Incorporating Monitors in Reactive Synthesis without Paying the Price

Abstract

Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative speci cations, and have found languages that combine modelling with declarative speci - cations more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative speci cations in the presence of an existing behaviour model as a monitor, with the bene t of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeat- ing triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional syn- thesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we ap- ply it to speci cations requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametri- sation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.