Synthesizing nonanomalous event-based controllers for liveness goals

Abstract

We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behaviour 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 modelled carefully in order to avoid synthesising anomalous behaviour models. We characterise non-anomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.