November 3, 2021
Gerardo Schneider
This talk is concerned with the combination of monitoring techniques and reactive synthesis based on temporal logic (LTL). We explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language (Monitor-Triggered Temporal Logic) with automata monitors as non-repeating and repeating 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 synthesis procedure for this language, where reasoning about the monitor state space is minimal. We show its applicability to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. This is a joint work with Shaun Azzopardi and Nir Piterman, based on the paper “Incorporating Monitors in Reactive Synthesis without Paying the Price” recently presented at ATVA'21.