We present a novel technique for synthesising behaviour models that works for an expressive subset of liveness properties and conforms
to the foundational requirements engineering World/Machine model, dealing explicitly with
assumptions on environment behaviour and distinguishing
controlled and monitored actions.
This is the first technique that conforms to what is considered best practice in requirements
specifications: distinguishing prescriptive and descriptive assertions.
Most previous attempts at using synthesis of behavioural models were
restricted to handling only safety properties.
Those that did support liveness were inadequate for synthesis of
operational event based models as they did not include the bespoke
distinction between system goals and environment assumptions.