Incorporating Monitors in Reactive Synthesis without Paying the Price

Reactive synthesis has a high complexity, 2EXPTIME, which can make the synthesis of real systems with large complex specifications difficult. However parts of a system may already exist or may be produced manually (e. g. when parts of the specification may be out of the scope for synthesis). Synthesis can then instead be applied on the remaining part of the specification. An interesting problem to consider in this context is what level of knowledge of the other components is required for the new component’s synthesis. We consider pre-existing components in the form of rich symbolic automata environment monitors (a lower-level specification language common in the runtime verification community). The choice of symbolic automata allows parametrised specifications and an exponentially succinct representation. We consider their combination with LTL formulas in a sequential fashion (a monitor triggers the component corresponding to the formula), and/or with repetition (when the synthesised component finishes the monitoring starts again). We introduce the notions of tight realisability and tight controllers for co-safety LTL formulas, allowing the controllers to signal immediately when a formula has been fulfilled for any given trace, to allow for regular repetition. We show that realisable LTL formulas can be synthesised and plugged-in without any knowledge of the monitor, while knowledge of the monitor increases the space of realisable specifications. This work illustrates how LTL synthesis can be used in richer and more imperative contexts, increasing its scope. This work was carried out with Nir Piterman and Gerardo Schneider, and based on work to appear in ATVA 2021.

Authors

• Shaun Azzopardi

Keywords

No keywords are indexed for this paper.