Incorporating Monitors in Reactive Synthesis without Paying the Price

TL;DR

This paper introduces a novel approach to reactive synthesis that incorporates monitors using automata triggers, enabling more expressive specifications with minimal state space reasoning, and provides a tool for controller construction.

Contribution

It presents a formal language with automata monitors as triggers, a compositional synthesis procedure, and a tool for constructing controllers, enhancing expressiveness and efficiency in reactive synthesis.

Findings

More expressive language than existing triggers.

Minimal reasoning about monitor state space.

Effective handling of counting and long sequence constraints.

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 specifications, and have found languages that combine modelling with declarative specifications 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 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 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. To show the advantages of our approach we apply it 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. We provide a tool to construct controllers (in the form of symbolic automata) for our language.