Synthesizing nonanomalous event-based controllers for liveness goals
Nicolás D’Ippolito, Victor A. Braberman, Nir Piterman, Sebastián Uchitel · ACM Transactions on Software Engineering and Methodology · 2013
We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behavior models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modeled carefully in order to avoid synthesizing anomalous behavior models. We characterize nonanomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.