Synthesizing nonanomalous event-based controllers for liveness goals

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 prop...