# GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Jul 2021.

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

- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)
- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)
- [Automated Approach for Solving Infinite-state Polynomial Reachability Games](https://mlsanity.com/paper/2605.10169/) (2026)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)

## Abstract (arXiv)

The synthesis of maximally-permissive controllers in infinite-state systems has many practical applications. Such controllers directly correspond to maximal winning strategies in logically specified infinite-state two-player games. In this paper, we introduce a tool called GenSys which is a fixed-point engine for computing maximal winning strategies for players in infinite-state safety games. A key feature of GenSys is that it leverages the capabilities of existing off-the-shelf solvers to implement its fixed point engine. GenSys outperforms state-of-the-art tools in this space by a significant margin. Our tool has solved some of the challenging problems in this space, is scalable, and also synthesizes compact controllers. These controllers are comparatively small in size and easier to comprehend. GenSys is freely available for use and is available under an open-source license.