# Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Feb 2025.

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

- [Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications](https://mlsanity.com/paper/2603.06710/) (2026)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)

## Abstract (arXiv)

The synthesis of infinite-state reactive systems from temporal logic specifications or infinite-state games has attracted significant attention in recent years, leading to the emergence of novel solving techniques. Most approaches are accompanied by an implementation showcasing their viability on an increasingly larger collection of benchmarks. Those implementations are -- often simple -- prototypes. Furthermore, differences in specification formalisms and formats make comparisons difficult, and writing specifications is a tedious and error-prone task. To address this, we present Issy, a tool for specification, realizability, and synthesis of infinite-state reactive systems. Issy comes with an expressive specification language that allows for combining infinite-state games and temporal formulas, thus encompassing the current formalisms. The realizability checking and synthesis methods implemented in Issy build upon recently developed approaches and extend them with newly engineered efficient techniques, offering a portfolio of solving algorithms. We evaluate Issy on an extensive set of benchmarks, demonstrating its competitiveness with the state of the art. Furthermore, Issy provides tooling for a general high-level format designed to make specification easier for users. It also includes a compiler to a more machine-readable format that other tool developers can easily use, which we hope will lead to a broader adoption and advances in infinite-state reactive synthesis.