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

TL;DR

Issy is a versatile tool that simplifies the specification, realizability checking, and synthesis of infinite-state reactive systems, integrating multiple formalisms and offering efficient algorithms and user-friendly tooling.

Contribution

It introduces Issy, a comprehensive tool with an expressive specification language and advanced synthesis algorithms, facilitating broader adoption and comparison in infinite-state reactive system synthesis.

Findings

Demonstrates competitiveness with state-of-the-art tools on benchmarks.

Provides a high-level specification format to ease user effort.

Includes a compiler for interoperability with other tools.

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 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.