Time-Varying Reach-Avoid Control Certificates for Stochastic Systems
For control theorists and practitioners, this provides a convex optimization-based method to certify and synthesize controllers for stochastic systems with safety and reachability constraints.
This paper introduces a reach-avoid certificate framework for discrete-time, continuous-space stochastic systems, enabling verification and synthesis of controllers that maximize the probability of reaching a target while avoiding unsafe regions. The method uses sum-of-squares optimization and is demonstrated on benchmark problems.
Reach-avoid analysis is fundamental to reasoning about the safety and goal-reaching behavior of dynamical systems, and serves as a foundation for specifying and verifying more complex control objectives. This paper introduces a reach-avoid certificate framework for discrete-time, continuous-space stochastic systems over both finite- and infinite-horizon settings. We propose two formulations: time-varying and time-invariant certificates. We also show how these certificates can be synthesized using sum-of-squares (SOS) optimization, providing a convex formulation for verifying a given controller. Furthermore, we present an SOS-based method for the joint synthesis of an optimal feedback controller and its corresponding reach-avoid certificate, enabling the maximization of the probability of reaching the target set while avoiding unsafe regions. Case studies and benchmark results demonstrate the efficacy of the proposed framework in certifying and controlling stochastic systems with continuous state and action spaces.