GenSys: A Scalable Fixed-Point Engine for Maximal Controller Synthesis over Infinite State Spaces
Fri 27 Aug 2021 23:25 - 23:30 - Architectures & Design—Model-Driven Software Engineering Chair(s): Davide Di Ruscio
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.
Fri 27 AugDisplayed time zone: Athens change
11:00 - 12:00 | Architectures & Design—Model-Driven Software EngineeringResearch Papers / Demonstrations +12h Chair(s): Luciano Baresi Politecnico di Milano, Davide Di Ruscio University of L'Aquila | ||
11:00 10mPaper | AlloyMax: Bringing Maximum Satisfaction to Relational SpecificationsDistinguished Paper Award Research Papers Changjian Zhang Carnegie Mellon University, Ryan Wagner Carnegie Mellon University, Pedro Orvalho INESC-ID; Universidade de Lisboa, David Garlan Carnegie Mellon University, Vasco Manquinho INESC-ID; Universidade de Lisboa, Ruben Martins Carnegie Mellon University, Eunsuk Kang Carnegie Mellon University DOI | ||
11:10 10mPaper | Timely and Accurate Detection of Model Deviation in Self-Adaptive Software-Intensive Systems Research Papers Yanxiang Tong Nanjing University, Yi Qin Nanjing University, Yanyan Jiang Nanjing University, Chang Xu Nanjing University, Chun Cao Nanjing University, Xiaoxing Ma Nanjing University DOI | ||
11:20 5mPaper | Sangrahaka: A Tool for Annotating and Querying Knowledge Graphs Demonstrations DOI | ||
11:25 5mPaper | GenSys: A Scalable Fixed-Point Engine for Maximal Controller Synthesis over Infinite State Spaces Demonstrations Stanly Samuel Indian Institute of Science, India, Deepak D'Souza IISc Bangalore, Raghavan Komondoor IISc Bengaluru DOI Pre-print | ||
11:30 30mLive Q&A | Q&A (Architectures & Design—Model-Driven Software Engineering) Research Papers | ||