From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach
Abstract
Reactive synthesis is the process of using temporal logic specifications in LTL to generate correct controllers, but its use has been restricted to Boolean specifications. Recently, a Boolean abstraction technique allows to translate LTL T specifications that contain literals in theories into equi-realizable LTL specifications. However, no synthesis procedure exists yet. In synthesis modulo theories, the system to synthesize receives valuations of environment variables in a first-order theory T and outputs valuations of system variables from T . In this paper, we address how to syntheize a full controller using a combination of the static Boolean controller obtained from the Booleanized LTL specification together with dynamic queries to a solver that produces models of a satisfiable existential formulae from T . This is the first method that realizes reactive synthesis modulo theories.
Keywords
Cite
@article{arxiv.2310.07904,
title = {From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach},
author = {Andoni Rodríguez and Cesar Sanchez},
journal= {arXiv preprint arXiv:2310.07904},
year = {2023}
}