On-the-Fly Symbolic Synthesis With Memory Reduction Guarantees

• 成果类型: Article
• 署名作者: Macoveiciuc, Elisei; Reissig, Gunther
• 署名单位: Bundeswehr University Munich
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2022.3188483
• 发表日期: 2023
• 页码: 2576-2583
• 关键词: Optimal control; Behavioral sciences; STANDARDS; Memory management; Heuristic algorithms; COSTS; Continuous time systems; computational methods; formal verification; synthesis; reach-avoid problem; safety problem

摘要

We present novel on-the-fly abstraction-based controller synthesis algorithms for two fundamental specifications-invariance and optimal reachability. In contrast to existing methods, the algorithms we propose do not require precomputation or storage of any large abstraction parts. This translates to orders of magnitude of reduction in memory consumption compared to standard methods. Moreover, our algorithms fully apply to general nonlinear systems and provide controllers that do not posses any additional conservatism. We demonstrate the successful synthesis of controllers for a problem that was previously unsolvable due to excessive memory and time consumption.