Source-linked AI summary
A Barrier Function Approach to Finite-Time Stochastic System Verification and Control
Cesar Santoyo, Maxence Dutreix, Samuel Coogan
TL;DR
The paper addresses finite-time safety verification and control for stochastic systems, where deterministic analyses do not capture random disturbances. It develops state-dependent stochastic barrier certificates solved through SOS optimization for continuous- and discrete-time systems, and synthesizes polynomial feedback controllers for affine-in-control dynamics. The framework provides probability bounds and demonstrates verification and control across three case studies.
Problem
Finite-time safety verification and feedback synthesis must address stochastic disturbances in safety-critical systems across continuous- and discrete-time settings.
Method
The paper uses stochastic control barrier functions with state-dependent expectation bounds, recasts the conditions as SOS optimization, and searches for polynomial feedback controllers.
Results
The framework provides finite-time probability bounds for both continuous- and discrete-time systems and demonstrates verification and control through three stochastic case studies.
Takeaways & Limitations
Affine-in-control stochastic systems can be paired with polynomial state feedback to meet a specified failure-probability criterion.
Takeaways & Limitations
Discrete-time controller synthesis becomes nonconvex when evaluating the expected barrier unless the barrier function is affine.
Abstract
from arXiv · showhide
This paper studies the problem of enforcing safety of a stochastic dynamical system over a finite-time horizon. We use stochastic control barrier functions as a means to quantify the probability that a system exits a given safe region of the state space in finite time. A barrier certificate condition that bounds the expected value of the barrier function over the time horizon is recast as a sum-of-squares optimization problem for efficient numerical computation. Unlike prior works, the proposed certificate condition includes a state-dependent upper bound on the evolution of the expectation. We present formulations for both continuous-time and discrete-time systems. Moreover, for systems for which the drift dynamics are affine-in-control, we propose a method for synthesizing polynomial state feedback controllers that achieve a specified probability of safety. Several case studies are presented which benchmark and illustrate the performance of our verification and control method in the continuous-time and discrete-time domains.
1 Introduction
The paper targets finite-time safety verification for stochastic systems, extending barrier-function methods to state-dependent expectation bounds and controller synthesis. It formulates continuous- and discrete-time approaches using SOS optimization and polynomial feedback control.
- Motivation: Finite-time safety verification is needed because many safety-critical systems face stochastic disturbances that deterministic analyses do not capture.The motivating examples include human-autonomous environments, where safety verification supports requirements such as collision avoidance.
- Contributions: The paper proposes a state-dependent bound on barrier-expectation evolution for continuous- and discrete-time stochastic systems.The condition includes the c-martingale formulation as a special case while accounting for system dynamics in the expectation constraint.
- Contributions: The proposed expectation constraint yields probability bounds no worse than the c-martingale condition and often improves them, especially for high sigma.The approach allows the expected barrier value to increase while retaining a finite-time safety interpretation.
- Contributions: Barrier functions are computed with SOS optimization using polynomial barriers, providing a simpler finite-horizon failure-probability formulation than exponential barriers.The paper reports empirically tighter probability bounds than the exponential-barrier approach in prior work.
- Control synthesis: For affine-in-control systems, the method searches for polynomial state-feedback controllers that meet a predetermined failure-probability criterion.The paper extends the verification formulation to control synthesis and includes discrete-time settings beyond the authors’ earlier continuous-time work.
- Evaluation: Three numerical case studies illustrate the verification and control methods in continuous- and discrete-time stochastic domains.The paper uses case studies to demonstrate the proposed results and conclusions.
2 Preliminaries
The preliminaries define the continuous- and discrete-time stochastic models, stopped processes, infinitesimal generators, and SOS programs used by the verification framework. These ingredients connect stochastic evolution and polynomial nonnegativity to computational optimization.
- 2.1 Stochastic Differential Equations: Continuous-time systems are modeled by stochastic differential equations with drift and diffusion terms under Lipschitz-continuity assumptions.The state evolves on a compact state space, with F as drift and sigma as diffusion.
- 2.1 Stochastic Differential Equations: The infinitesimal generator extends ordinary differentiation by describing the expected evolution of a function of a stochastic process.For the considered stochastic differential equation, the generator acts on twice-differentiable functions such as barrier functions.
- 2.1 Stochastic Differential Equations: A stopped process freezes the trajectory at its first exit time from the interior of the state space while preserving the relevant Markov and generator properties.The stopped process equals the original process before exit and remains at the exit state afterward.
- 2.2 Stochastic Difference Equations: Discrete-time systems evolve through a state map plus a disturbance term, with the disturbance governed by a probability distribution at each step.The discrete-time stopped process is defined analogously to the continuous-time construction.
- 2.3 Sum-of-Squares: Sum-of-squares polynomials are globally nonnegative, making them useful for encoding polynomial nonnegativity constraints.The preliminaries define SOS polynomials as a class within the polynomial ring and state their nonnegativity property.
- 2.3 Sum-of-Squares: A sum-of-squares program searches for polynomial decision variables subject to SOS and polynomial constraints.SOS programs can be converted efficiently into semidefinite programs using tools such as SOSTOOLS.
3 Problem Formulation
The paper formulates finite-horizon verification as bounding unsafe-entry probability for continuous- and discrete-time stochastic systems, then extends the formulation to feedback synthesis. Stochastic control barrier functions impose state, unsafe-set, and expectation constraints that yield probability bounds.
- 3 Problem Formulation: The verification objective is to upper-bound the probability that a stochastic system reaches unsafe conditions within a fixed finite horizon.The synthesis objective is to construct feedback control achieving a desired maximum failure probability.
- 3.1 Continuous Time Systems: In continuous time, the controlled stochastic dynamics combine drift, affine control input, and diffusion driven by a Wiener process.The feedback law is state-dependent, and the total drift is defined as F(x)=f(x)+g(x)u(x).
- 3.1 Continuous Time Systems: The continuous-time theorem requires a twice-differentiable barrier that is bounded above on the initial set, at least one on the unsafe set, and nonnegative on the state space.These constraints support finite-time probability bounds for a fixed feedback policy.
- 3.1 Continuous Time Systems: Relaxing the infinitesimal-generator supermartingale condition produces three case-dependent finite-time probability bounds.The resulting barrier is called a stochastic control barrier function, and the c-martingale bound appears as one characterized special case.
- 3.1 Continuous Time Systems: For a known initial state, the continuous-time bounds can use B(x0) instead of the initial-set bound gamma.This yields a probability bound for one initial point rather than the entire initial set.
- 3.2 Discrete Time Systems: In discrete time, the controlled transition includes a polynomial feedback law and a random disturbance through F(x,xi).The discrete-time theorem applies analogous stochastic control-barrier conditions to the stopped process.
- 3.2 Discrete Time Systems: The discrete-time barrier conditions use parameters alpha-tilde, beta-tilde, and gamma, with alpha-tilde at least 1, beta-tilde below 1, and gamma in [0,1).A barrier satisfying these conditions is likewise called a stochastic control barrier function for the chosen policy.
4 SOS Formulations & Numerical Procedures
The paper formulates continuous- and discrete-time stochastic barrier verification as SOS programs, then develops iterative procedures for verification and polynomial feedback-controller synthesis.
- 4 SOS Formulations & Numerical Procedures: The approach converts continuous- and discrete-time stochastic control-barrier conditions into SOS constraints for constructing barrier functions and computing failure-probability bounds.The continuous-time and discrete-time formulations use polynomial barrier functions and SOS relaxations of set constraints.
- 4.3 Controller Synthesis Procedure: Discrete-time controller synthesis is generally nonlinear and nonconvex because of E[B(F(x, ξ)) | x], although a linear barrier keeps the optimization problem convex.This limitation arises because the discrete-time expected barrier term complicates the search for polynomial controllers.
- 4.2 Verification & Control Law Synthesis Algorithms: Because the formulations become nonconvex when barrier parameters and control laws are variables, the algorithms fix selected variables, search over α, and optimize γ + β heuristically.The verification procedure computes a barrier for fixed u(x), uses a line search on α, and trades higher polynomial degree for tighter bounds and longer computation.
- 4.2 Verification & Control Law Synthesis Algorithms: The discrete-time procedure follows the continuous-time workflow but uses the discrete-time constraints and computes unsafe-probability bounds from the corresponding discrete-time formulas.The notation in Algorithm 1 simplifies the presentation by using α and β for the discrete-time parameters.
- 4.3 Controller Synthesis Procedure: Controller synthesis searches for a polynomial feedback law of order no greater than the barrier and targets a designer-specified upper bound on failure probability.The controller is represented in quadratic form using a monomial vector and coefficient matrix.
- 4.3 Controller Synthesis Procedure: The controller objective minimizes a coefficient bound that serves as a proxy for control effort while enforcing element-wise bounds on the polynomial coefficients.The scalar c bounds the entries of Q, and minimizing c encourages lower control effort.
- 4.3 Controller Synthesis Procedure: The controller-search algorithms interleave barrier verification with feedback updates, beginning from a fixed or zero control policy and adjusting β until the target probability is approached.Algorithm 3 combines the verification procedure with the controller search and iteratively updates β relative to the probability goal.
5 Case Studies
The case studies evaluate finite-horizon stochastic safety verification and control across continuous- and discrete-time systems using polynomial barrier functions, Monte Carlo comparisons, and SOS-based computation. Results show improved probability bounds, control synthesis to specified targets, and trade-offs between barrier complexity, control effort, and computational limitations.
- 5.1 1-D Stochastic System: The polynomial probability bound outperforms the prior c-martingale bound, especially at higher noise levels where the exponential bound becomes trivial.The comparison uses a 16th-degree polynomial barrier and 5000-draw Monte Carlo simulations as a reference.
- 5.1 1-D Stochastic System: Higher-degree barrier polynomials can reduce the required control gain, but the benefit saturates while computation time increases.The required gain no longer decreases after the polynomial degree reaches a saturation point.
- 5.2 Nonlinear Dynamics: The nonlinear continuous-time example bounds failure probability for 5000 Monte Carlo trajectories across constant σ values from 0.5 to 1.5.A 14th-degree polynomial barrier is used for the bound.
- 5.2 Nonlinear Dynamics: For the nonlinear system, a synthesized polynomial controller targets Pgoal = 0.10 using a 2nd-order controller and 10th-order barrier functions.The barrier degree is limited by SOSTOOLS computational constraints, and Table 1 compares controlled results with the uncontrolled upper bound.
- 5.3 Discrete-Time Population Model: The discrete-time population model combines 8th-order polynomial verification with Monte Carlo comparisons and 1st-order barrier control synthesis.The verification uses N = 2, while the control experiment uses N = 3 and Pgoal = 0.10.
- 5.3 Discrete-Time Population Model: Discrete-time synthesis is restricted to affine barrier functions because evaluating the expected barrier after one step otherwise creates a nonconvex constraint.The control experiment therefore uses a 1st-order barrier function over a restricted domain.
6 Conclusion
The paper develops stochastic control barrier functions for quantifying failure-probability bounds and synthesizing controllers that meet specified safety criteria.
- The methods quantify upper bounds on system failure probabilities using continuous-time and discrete-time stochastic control barrier functions.
- The proposed finite-time verification approach constrains the evolution of a non-negative barrier-function expectation and supports control synthesis.