Time-Varying Reach-Avoid Control Certificates for Stochastic Systems

TL;DR

This paper develops a framework for certifying and synthesizing controllers for stochastic systems to ensure safety and goal-reaching, using sum-of-squares optimization for both finite and infinite horizons.

Contribution

It introduces time-varying and time-invariant reach-avoid certificates for stochastic systems and provides SOS-based methods for their synthesis and controller design.

Findings

Effective certification of stochastic systems demonstrated through case studies.

SOS-based synthesis maximizes probability of reaching targets while avoiding unsafe regions.

Framework applicable to systems with continuous state and action spaces.

Abstract

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.