Lazy Synthesis of Symbolic Output-Feedback Controllers for State-Based Safety Specifications

Lazy Synthesis of Symbolic Output-Feedback Controllers for State-Based Safety Specifications

연구 분야: Verification

학회: HSCC '23: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control

This short paper presents a lazy symbolic output-feedback controller synthesis algorithm for state-based safety specifications over large transition systems. The novel idea of our approach is to integrate an iterative algorithm for observer design with an online adaptable safety controller synthesis algorithm. This allows us to iteratively update the safety controller to observer refinements and to guide these refinements by the existing controller. This results in efficient lazy synthesis of a safety controller whose domain increases with the time spent in synthesis. We present simulation results for a synthetic robot motion planning example showing the benefits of our algorithm compared to the standard approach.