Stochastic reachability of a target tube: Theory and computation

TL;DR

This paper develops a scalable, convex-optimization-based method for computing probabilistic safety guarantees in stochastic dynamical systems, specifically targeting the stochastic reachability problem within time-varying constraints.

Contribution

It introduces a novel, grid-free algorithm for underapproximating stochastic reach sets using convex optimization, improving scalability and performance over existing tools.

Findings

Algorithm outperforms existing software in verification tasks.

Provides conditions for properties of stochastic reach sets.

Demonstrates scalability on numerical examples.

Abstract

Probabilistic guarantees of safety and performance are important in constrained dynamical systems with stochastic uncertainty. We consider the stochastic reachability problem, which maximizes the probability that the state remains within time-varying state constraints (i.e., a ``target tube''), despite bounded control authority. This problem subsumes the stochastic viability and terminal hitting-time stochastic reach-avoid problems. Of special interest is the stochastic reach set, the set of all initial states from which it is possible to stay in the target tube with a probability above a desired threshold. We provide sufficient conditions under which the stochastic reach set is closed, compact, and convex, and provide an underapproximative interpolation technique for stochastic reach sets. Utilizing convex optimization, we propose a scalable and grid-free algorithm that computes a polytopic underapproximation of the stochastic reach set and synthesizes an open-loop controller. This algorithm is anytime, i.e., it produces a valid output even on early termination. We demonstrate the efficacy and scalability of our approach on several numerical examples, and show that our algorithm outperforms existing software tools for verification of linear systems.