Synthesizing Controller for Unsynthesizable Specification Based on Criticality Levels
Dong Yang, Hao Shi, Wei Dong, Yanqi Dong, Yong Zhang · 2024
Synthesizing a reactive system fulfilling given requirements is an interesting and challenging problem in the field of formal methods. By using temporal logic as specifications, related results have been well applied in the synthesis of Unmanned Autonomous System (UAS) controllers. But in practice, static and monolithic specifications are usually accompanied with the problem of being unsynthesizable in dynamic and complex environments. To improve the flexibility of controller synthesis, we propose specifications based on criticality levels and corresponding synthesis methods in this paper. When the complete specification is unsynthesizable, according to different synthesis algorithms of initial, transition and goal constraints, the controller that strictly fulfills the critical specifications will be synthesized. The non-critical specifications are used to guide the synthesis process and will be satisfied as much as possible. The proposed methods can improve the adaptability of UAS controller in complex and changeable running environments.