English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In the current control design of safety-critical autonomous systems, formalverification techniques are typically applied after the controller is designedto evaluate whether the required properties (e.g., safety) are satisfied.However, due to the increasing system complexity and the fundamental hardnessof designing a controller with formal guarantees, such an open-loop process ofdesign-then-verify often results in many iterations and fails to provide thenecessary guarantees. In this paper, we propose a correct-by-constructioncontrol learning framework that integrates the verification into the controldesign process in a closed-loop manner, i.e., design-while-verify.Specifically, we leverage the verification results (computed reachable set ofthe system state) to construct feedback metrics for control learning, whichmeasure how likely the current design of control parameters can meet therequired reach-avoid property for safety and goal-reaching. We formulate anoptimization problem based on such metrics for tuning the controllerparameters, and develop an approximated gradient descent algorithm with adifference method to solve the optimization problem and learn the controller.The learned controller is formally guaranteed to meet the required reach-avoidproperty. By treating verifiability as a first-class objective and effectivelyleveraging the verification results during the control learning process, ourapproach can significantly improve the chance of finding a control design withformal property guarantees. This is demonstrated via a set of experiments onboth linear and non-linear systems that use model-based or neural network basedcontrollers.

Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees