Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Forward Reachability for Discrete-Time Nonlinear Stochastic Systems via Mixed-Monotonicity and Stochastic Order

Vignesh Sivaramakrishnan, Rosalyn A. Devonport, Murat Arcak, Meeko M. K. Oishi

TL;DR

This work develops a framework to compute forward stochastic reach sets for discrete-time nonlinear systems by extending mixed-monotone dynamics to operate under stochastic orders. By introducing a decomposition-based stochastic-monotone representation and a concentration inequality, the authors obtain interval over-approximations $X_k=[\underline{x}_k,\overline{x}_k]$ along with probabilities $1-\delta_k$ that the state lies inside. An algorithm leverages independence and the monotone structure to propagate these intervals over a finite horizon, yielding tractable, simulation-based reachability guarantees. Applied to aerospace problems, the method demonstrates effective interval containment in a linear example and exposes conservatism in nonlinear regimes, motivating future refinements to tighten bounds while preserving computational efficiency.

Abstract

We present a method to overapproximate forward stochastic reach sets of discrete-time, stochastic nonlinear systems with interval geometry. This is made possible by extending the theory of mixed-monotone systems to incorporate stochastic orders, and a concentration inequality result that lower-bounds the probability the state resides within an interval through a monotone mapping. Then, we present an algorithm to compute the overapproximations of forward reachable set and the probability the state resides within it. We present our approach on two aerospace examples to show its efficacy.

Forward Reachability for Discrete-Time Nonlinear Stochastic Systems via Mixed-Monotonicity and Stochastic Order

TL;DR

This work develops a framework to compute forward stochastic reach sets for discrete-time nonlinear systems by extending mixed-monotone dynamics to operate under stochastic orders. By introducing a decomposition-based stochastic-monotone representation and a concentration inequality, the authors obtain interval over-approximations along with probabilities that the state lies inside. An algorithm leverages independence and the monotone structure to propagate these intervals over a finite horizon, yielding tractable, simulation-based reachability guarantees. Applied to aerospace problems, the method demonstrates effective interval containment in a linear example and exposes conservatism in nonlinear regimes, motivating future refinements to tighten bounds while preserving computational efficiency.

Abstract

We present a method to overapproximate forward stochastic reach sets of discrete-time, stochastic nonlinear systems with interval geometry. This is made possible by extending the theory of mixed-monotone systems to incorporate stochastic orders, and a concentration inequality result that lower-bounds the probability the state resides within an interval through a monotone mapping. Then, we present an algorithm to compute the overapproximations of forward reachable set and the probability the state resides within it. We present our approach on two aerospace examples to show its efficacy.
Paper Structure (12 sections, 11 theorems, 26 equations, 3 figures, 1 algorithm)

This paper contains 12 sections, 11 theorems, 26 equations, 3 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and problem formulation
  3. Probabilistic Forward Reachability
  4. Mixed Monotone Systems
  5. Stochastic Orders
  6. Towards a Stochastic-order Theory of Monotone Dynamics
  7. From Stochastic Order to Concentration Inequality
  8. Algorithms for computing forward reachable set of a desired probability via stochastic order
  9. Examples
  10. CWH dynamics
  11. Line-of-sight of a 7 dimensional spacecraft
  12. Conclusion and Future Directions

Key Result

Lemma 1

Suppose we have a system eq:nonlinearSys with decomposition function, $g$. If $[\underline{x},\overline{x}]\subseteq \mathbb{R}^{n_x}$ and $[\underline{w},\overline{w}]\subseteq \mathbb{R}^{n_w}$ where $\underline{x},\overline{x}\in\mathbb{R}^{n_x}$ and $\underline{w},\overline{w}\in\mathbb{R}^{n_w} $\forall x\in[\underline{x},\overline{x}]$ and $\forall w\in[\underline{w},\overline{w}]$.

Figures (3)

  • Figure 1: Our approach combines the benefits of mixed monotonicity via the concentration inequalities we derive by establishing partial order of mixed-monotone decomposition of discrete-time stochastic systems via stochastic order. This allows us to determine the probability (denoted in red) the states of the system lie within the overapproximation of forward reachable sets in the form of intervals (denoted in blue).
  • Figure 2: Resulting spacecraft trajectory subjected to random initial condition and random disturbances starting with $95\%$ probability (i.e. $1-\delta_0 = 0.95$) of the state and disturbance lying within their intervals, , \ref{['eq:intervalProbAlg']}. Note that while the theoretical bound we recursively update in line \ref{['algLine:xIntervalProb']} of Algorithm \ref{['alg:prop']} drops to zero past 80 seconds, a majority of the simulated trajectories still reside within the interval reach set.
  • Figure 3: Resulting spacecraft trajectory subjected to random initial condition and random disturbances which reside in their initial intervals with $90\%$ probability (i.e. $1-\delta_0 = 0.9$), \ref{['eq:intervalProbAlg']}. In contrast to the linear example, the nonlinear system is highly sensitive to the underlying noise and results in stochastic interval reach sets to blow up to cover all possible values of \ref{['eq:angle_sensor']}.

Theorems & Definitions (26)

  • Definition 1: Mixed-Monotonicity in Discrete Time coogan2020mixedmeyer2021interval
  • Lemma 1: Discrete time forward interval reach sets coogan2015efficient
  • Definition 2: Upper set dolecki2016convergence
  • Definition 3: Stochastic Order of random vectors stocOrderShakedShantikumar
  • Lemma 2: Stochastic order through a monotone function stocOrderShakedShantikumar
  • Corollary 1
  • proof
  • Definition 4: Standard construction of a random vector stocOrderShakedShantikumar
  • Lemma 3: Natural construction of stochastic order
  • Definition 5
  • ...and 16 more