Minimal Assumptions Refinement for Realizable Specifications
Davide G. Cavezza, Dalal Alrajeh, András György
Abstract
A challenge that has gathered much attention in recent years is automated synthesis of correct-by-construction software systems from declarative specifications. The specification language is typically a subset of linear temporal logic called generalized reactivity of rank 1, for which there exists an efficient synthesis algorithm. Specifications in this language model the system as the interaction between an environment and a controller, the former satisfying a set of assumptions and the latter a set of guarantees. In order for a solution to exist, a sufficient set of assumptions implying the guarantees must be provided. The assumptions must be as general as possible and small enough to be intelligible by engineers that need to assess their consistency with the true environment where the synthesized controller will operate.