On-the-fly reactive synthesis modulo theories

Abstract

The Boolean abstraction technique translates (i.e., Booleanizes) an LTL modulo theories specification into an equi-realizable LTL specification. This solves the realizability modulo theories problem. However, synthesis modulo theories is a different problem: the system has to receive valuations in a first-order theory T and output valuations in T . In this work in progress, we address how to meet this need without a pure synthesis method, but solving ”synthesis” on-the-fly by synthetising a Boolean controller from the Booleanized LTL specification and shipping it with a method that provides models in satisfiable instances of existential formulae (e.g., an SMT solver).