Abstraction Refinement for Attractivity Controllers Using Quantitative Synthesis

• 成果类型: Article
• 署名作者: Apaza-Perez, W. Alejandro; Girard, Antoine
• 署名单位: Universite Paris Saclay; Centre National de la Recherche Scientifique (CNRS); Universidad Mayor de San Andres
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2022.3227371
• 发表日期: 2023
• 页码: 5745-5751
• 关键词: Attractivity specification; formal methods; sym-bolic control

摘要

Attractivity specifications consist in driving the state of a system to a target region and to keep it in that region afterward. In this article, we develop an approach to controller synthesis for attractivity specifications based on iterative refinements of symbolic abstractions. We compute iteratively sequences of least-violating attractivity controllers and of associated attractors. The current controller is used to restrict possible control actions at the next iteration where a new abstraction is used following a local refinement applied inside the current attractor. The approach results in a nested sequence of attractors that are closer to the target region at each iteration. To illustrate the effectiveness of our approach, we show an application to a marine vessel system.