Design-while-Verify: Correct-by-Construction Control Learning with Verification in the Loop
TimeThursday, July 14th11:37am - 12pm PDT
Location3000, Level 3
Design of Cyber-physical Systems, Cloud Computing and IoT
DescriptionIn this paper, we propose a correct-by-construction control learning framework that integrates the verification into the control design process for safety-critical CPSs. Specifically, we leverage the verification results to construct feedback metrics, which measure how likely the current design of control parameters can meet the required reach-avoid property for safety and goal-reaching. We formulate an optimization problem based on such metrics for tuning the controller parameters and develop an approximated gradient descent algorithm. The learned controller is formally guaranteed to meet the required reach-avoid property. Our approach can significantly improve the chance of finding control design with formal guarantees.