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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
