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

TL;DR

GenSys is an open-source fixed-point engine that efficiently synthesizes compact, maximally-permissive controllers for infinite-state safety games by leveraging existing solvers, outperforming current tools in scalability and problem-solving.

Contribution

Introduces GenSys, a scalable fixed-point engine that uses existing solvers to synthesize small, understandable controllers for infinite-state systems, advancing the state-of-the-art.

Findings

GenSys outperforms existing tools significantly.

Successfully solves challenging infinite-state problems.

Produces smaller, more comprehensible controllers.

Abstract

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.