一句话：提出 GenSys 不动点引擎，利用现成求解器为无限状态安全博弈计算最大获胜策略并合成紧凑控制器。
无限状态系统中最大许可控制器的合成具有广泛实际应用，这类控制器对应于逻辑规约的无限状态双人博弈中的最大获胜策略。本文提出工具 GenSys，它是一个不动点引擎，用于计算无限状态安全博弈中参与者的最大获胜策略。其关键特点是复用现成求解器的能力来实现不动点计算，而无需自行构造完整专用求解器。评估表明，GenSys 在该领域显著优于现有最先进工具，能够求解一些具有挑战性的问题，具备可扩展性，并且合成出的控制器较为紧凑、规模较小且更易理解。该工具已开源并免费提供使用。
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.
@inproceedings{paperbot6345,
title = {GenSys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces},
author = {Stanly Samuel and Deepak D'Souza and Raghavan Komondoor},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3473126}
}