# Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis (Full Version)

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Nov 2024.

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

- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)
- [Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications](https://mlsanity.com/paper/2603.06710/) (2026)

## Abstract (arXiv)

Infinite-state reactive synthesis has attracted significant attention in recent years, which has led to the emergence of novel symbolic techniques for solving infinite-state games. Temporal logics featuring variables over infinite domains offer an expressive high-level specification language for infinite-state reactive systems. Currently, the only way to translate these temporal logics into symbolic games is by naively encoding the specification to use techniques designed for the Boolean case. An inherent limitation of this approach is that it results in games in which the semantic structure of the temporal and first-order constraints present in the formula is lost. There is a clear need for techniques that leverage this information in the translation process to speed up solving the generated games. In this work, we propose the first approach that addresses this gap. Our technique constructs a monitor incorporating first-order and temporal reasoning at the formula level, enriching the constructed game with semantic information that leads to more efficient solving. We demonstrate that thanks to this, our method outperforms the state-of-the-art techniques across a range of benchmarks.