  In the current control design of safety-critical autonomous systems, formal
verification techniques are typically applied after the controller is designed
to evaluate whether the required properties (e.g., safety) are satisfied.
However, due to the increasing system complexity and the fundamental hardness
of designing a controller with formal guarantees, such an open-loop process of
design-then-verify often results in many iterations and fails to provide the
necessary guarantees. In this paper, we propose a correct-by-construction
control learning framework that integrates the verification into the control
design process in a closed-loop manner, i.e., design-while-verify.
Specifically, we leverage the verification results (computed reachable set of
the system state) to construct feedback metrics for control learning, 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 with a
difference method to solve the optimization problem and learn the controller.
The learned controller is formally guaranteed to meet the required reach-avoid
property. By treating verifiability as a first-class objective and effectively
leveraging the verification results during the control learning process, our
approach can significantly improve the chance of finding a control design with
formal property guarantees. This is demonstrated via a set of experiments on
both linear and non-linear systems that use model-based or neural network based
controllers.
