# Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

arXiv: https://arxiv.org/abs/2407.09348 · HTML: https://mlsanity.com/paper/2407.09348/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 41 references that are in the map.
- First posted on arXiv 12 Jul 2024.

## Builds on (most cited first, 17 of 17)

- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Shield Synthesis: Runtime Enforcement for Reactive Systems](https://mlsanity.com/paper/1501.02573/) (2015)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Boolean Abstractions for Realizability Modulo Theories (Extended version)](https://mlsanity.com/paper/2310.17292/) (2023)
- [Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)](https://mlsanity.com/paper/2204.13693/) (2022)
- [Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts](https://mlsanity.com/paper/1709.04986/) (2017)
- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces](https://mlsanity.com/paper/2107.08794/) (2021)
- [Reactive Synthesis Modulo Theories Using Abstraction Refinement](https://mlsanity.com/paper/2108.00090/) (2021)
- [Solving Infinite-State Games via Acceleration (Full Version)](https://mlsanity.com/paper/2305.16118/) (2023)
- [Full LTL Synthesis over Infinite-state Arenas](https://mlsanity.com/paper/2307.09776/) (2023)
- [Towards Realizability Checking of Contracts using Theories](https://mlsanity.com/paper/1502.03005/) (2015)
- [Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability](https://mlsanity.com/paper/1610.05867/) (2016)
- [Numerical LTL Synthesis for Cyber-Physical Systems](https://mlsanity.com/paper/1307.3722/) (2013)
- [Symbolic Automata: ω-Regularity Modulo Theories](https://mlsanity.com/paper/2310.02393/) (2023)
- [A General Automata Model for First-Order Temporal Logics (Extended Version)](https://mlsanity.com/paper/2405.20057/) (2024)

## Built on by (most cited first, 2 of 2)

- [Realizable Continuous-Space Shields for Safe Reinforcement Learning](https://mlsanity.com/paper/2410.02038/) (2024)
- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)

## Abstract (arXiv)

Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient).