Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories
DOI:
https://doi.org/10.1609/aaai.v38i9.28939Keywords:
KRR: Geometric, Spatial, and Temporal Reasoning, KRR: Automated Reasoning and Theorem ProvingAbstract
Reactive synthesis is the process of generate correct con- trollers from temporal logic specifications. Typically, synthesis is restricted to Boolean specifications in LTL. Recently, a Boolean abstraction technique allows to translate LTLT specifications that contain literals in theories into equi-realizable LTL specifications, but no full synthesis procedure exists yet. In synthesis modulo theories, the system receives valuations of environment variables (from 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 on-the-fly queries to a solver that produces models of satisfiable existential T formulae. This is the first synthesis method for LTL modulo theories. Additionally, our method can produce adaptive responses which increases explainability and can improve runtime properties like performance. Our approach is applicable to both LTL modulo theories and LTLf modulo theories.Downloads
Published
2024-03-24
How to Cite
Rodríguez, A., & Sánchez, C. (2024). Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories. Proceedings of the AAAI Conference on Artificial Intelligence, 38(9), 10679-10686. https://doi.org/10.1609/aaai.v38i9.28939
Issue
Section
AAAI Technical Track on Knowledge Representation and Reasoning