Counter Example Guided Reactive Synthesis for LTL Modulo Theories

Abstract

Reactive synthesis is the process of automatically generating a correct system from a given temporal specification. In this paper, we address the problem of reactive synthesis for LTL modulo theories ( ), which extends LTL with literals from a first-order theory and allows relating the values of data across time. This logic allows describing complex dynamics both for the system and for the environment—such as a numeric variable increasing monotonically over time. The logic also allows defining relations (and not only assignment) between variables, enabling permissive shielding. We propose a sound algorithm called Counter-Example Guided Reactive Synthesis modulo theories (CEGRES), whose core is the novel concept of reactive tautology, which are valid temporal formulas that preserve the semantics of the specification but make the algorithm conclusive. Although realizability for full is undecidable in general, we prove that CEGRES is terminating for some important theories and for arbitrary theories when specifications do not fetch data across time. We include an empirical evaluation that shows that CEGRES can solve many reactive synthesis problems of practical interest.