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

Abstract

Abstract 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 , a tool for specification, realizability, and synthesis of infinite-state reactive systems. 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 build upon recently developed approaches and extend them with newly engineered efficient techniques, offering a portfolio of solving algorithms. We evaluate on an extensive set of benchmarks, demonstrating its competitiveness with the state of the art. Furthermore, 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.