Reactive Synthesis Modulo Theories using Abstraction Refinement

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


Reactive synthesis builds a system from a specification given as a temporal logic formula. Traditionally, reactive synthesis is defined for systems with Boolean input and output variables. Recently, new techniques have been proposed to extend reactive synthesis to data domains, which are required for more sophisticated programs. In particular, Temporal stream logic (TSL) extends LTL with state variables, updates, and uninterpreted functions and was created for use in synthesis. We present a new synthesis procedure for TSL(T), an extension of TSL with theories. Our approach is also able to find predicates, not present in the specification, that are required to synthesize some programs. Synthesis is performed using two nested counterexample guided synthesis loops and an LTL synthesis procedure.
Our method translates TSL(T) specifications to LTL and extracts a system if synthesis is successful. Otherwise, it analyzes the counterstrategy for inconsistencies with the theory, these are then ruled out by adding temporal assumptions, and the next iteration of the loop is started. If no inconsistencies are found the outer refinement loop tries to identify new predicates and reruns the inner loop. A system can be extracted if the LTL synthesis returns
realizable at any point, if no more predicates can be added the problem is unrealizable. The general synthesis problem for TSL is known to be undecidable. We identify a new decidable fragment and demonstrate that our method can successfully synthesize or show unrealizability of several non-Boolean examples.
Original languageEnglish
Title of host publicationProceedings of the 22nd Formal Methods in Computer-Aided Design, FMCAD 2022
PublisherTU Wien Academic Press
ISBN (Electronic)978-3-85448-053-2
Publication statusPublished - 2022
Event22nd Formal Methods in Computer-Aided Design: FMCAD 2022 - Trento, Italy
Duration: 19 Oct 202221 Oct 2022

Publication series

NameConference Series: Formal Methods in Computer-Aided Design


Conference22nd Formal Methods in Computer-Aided Design
Abbreviated titleFMCAD 2022

Cite this