GenSys:一种用于无限状态空间上极大控制器综合的可扩展不动点引擎
计算机科学中的逻辑
2021-08-18 v2 系统与控制
系统与控制
摘要
在无限状态系统中综合最大许可控制器具有许多实际应用。此类控制器直接对应于逻辑指定的无限状态双人博弈中的极大获胜策略。本文介绍一种称为 GenSys 的工具,它是一个用于计算无限状态安全博弈中玩家极大获胜策略的不动点引擎。GenSys 的一个关键特性是借助现有现成求解器的能力来实现其不动点引擎。GenSys 在此领域显著优于最先进的工具。我们的工具已解决该领域一些具有挑战性的问题,具有可扩展性,并能综合出紧凑的控制器。这些控制器规模相对较小且更易于理解。GenSys 可免费使用,并基于开源许可提供。
引用
@article{arxiv.2107.08794,
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},
journal= {arXiv preprint arXiv:2107.08794},
year = {2021}
}