Maximizing Reach-Avoid Probabilities for Linear Stochastic Systems via Control Architectures

TL;DR

The work addresses safety-critical control for linear stochastic systems by maximizing reach-avoid probabilities using a hierarchical scheme that couples Model Predictive Control with a Dynamic Programming–based reference generator. By modeling the closed-loop as an MDP and solving a DP on a finite abstraction, the method achieves scalable reach-avoid optimization while providing formal guarantees; robustifications ensure bounds under gridding and modeling errors. The approach is validated on a linear perturbed quadcopter in cluttered environments, demonstrating both flexibility and scalability, with a demonstrated underapproximation guarantee $\tilde{V}_0(c_0) \le V_0(x_0)$. These contributions offer a practical pathway to safety-certified performance in higher-dimensional stochastic systems, balancing tractability and theoretical guarantees in real-world settings.

Abstract

The maximization of reach-avoid probabilities for stochastic systems is a central topic in the control literature. Yet, the available methods are either restricted to low-dimensional systems or suffer from conservative approximations. To address these limitations, we propose control architectures that combine the flexibility of Markov Decision Processes with the scalability of Model Predictive Controllers. The Model Predictive Controller tracks reference signals while remaining agnostic to the stochasticity and reach-avoid objective. Instead, the reach-avoid probability is maximized by optimally updating the controller's reference online. To achieve this, the closed-loop system, consisting of the system and Model Predictive Controller, is abstracted as a Markov Decision Process in which a new reference can be chosen at every time-step. A feedback policy generating optimal references is then computed via Dynamic Programming. If the state space of the system is continuous, the Dynamic Programming algorithm must be executed on a finite system approximation. Modifications to the Model Predictive Controller enable a computationally efficient robustification of the Dynamic Programming algorithm to approximation errors, preserving bounds on the achieved reach-avoid probability. The approach is validated on a perturbed 12D quadcopter model in cluttered reach-avoid environments proving its flexibility and scalability.

Figures (7)

• Figure 1: X-Y-trajectory of a perturbed quadcopter. The goal is to reach the gray sets while avoiding the red walls of the labyrinth. A control architecture is used to maximize the reach-avoid probability, achieving a success rate of $40%$. Successful trajectories are green, unsuccessful red. The initial position is $(-0.5,-0.5)$. Details are provided in Section \ref{['sec_numerical_example']}.
• Figure 2: The MPC receives commands $a$, which contain a reference trajectory, and computes inputs $u$ based on the system state $x$. It ensures that ${x}(t)\in{\mathcal{G}}$ and $u(t)\in\mathcal{U}$ for all $t\geq 0$. The DP policy generates commands $a$ at time intervals of $\Delta_t$ based on $x(k\Delta_t)$, $k\in\mathbb{N}$. The command $a$ influences the behavior of the MPC, and it is chosen such that the closed-loop system achieves a maximum reach-avoid probability.
• Figure 3: The constraint $x_{k,j}\in\hat{\mathcal{G}}=\mathcal{G}\ominus B_{\eta}$ ensures that $x(t)\in\mathcal{G}$, for all $t\in[k\Delta_t+j\delta_t,k\Delta_t + (j+1)\delta_t]$, $k\in[N]$, $j\in[J]$. The constraint $x_{k,j}\in\Tilde{\mathcal{G}}=\hat{\mathcal{G}}\ominus B_{r}$ ensures that $x_{k,j}\in\hat{\mathcal{G}}$ even when the initial state $x_{k,0}$ is uncertain within a set $\mathcal{H}$. The red circles indicate the balls $B_{\eta}$ and $B_r$, the gray boxes indicate the tube $\mathcal{E}$.
• Figure 4: X-Y-trajectories of a quadcopter under our proposed control architecture in different scenarios. The control architecture maximizes the reach-avoid probability. Top-left: simple, Top-right: eth+mit, Bottom-Left: zigzag, Bottom-Right: balls, and Fig. \ref{['fig_num_lab']}: labyrinth. The unsafe set $\mathcal{S}^c$ is red, the target set $\mathcal{T}$ gray. Green trajectories satisfy the reach-avoid objective, red trajectories do not. The initial x- and y-position are always chosen as $(0.5,0.5)$.
• Figure 5: Commands (blue) and quadcopter trajectory (red) of a simulation run in the simple environment.

Theorems & Definitions (8)

• Lemma 3.1: Proof in Appendix \ref{['app_proof_lem_cont_time_constraint_satisfaction']}
• Proposition 3.2: Proof in Appendix \ref{['app_proof_prop_recursive_feasibility_of_MPC']}
• Lemma 4.1: Proof in Appendix \ref{['proof_lem_B_bounds_Epsilon']}
• Corollary 4.2
• Proposition 4.3: Proof in Appendix \ref{['proof_prop_RMPC_guarantees']}
• Theorem 4.4: Proof in Appendix \ref{['app_proof_thm_value_function_underapproximation']}
• Lemma A.1
• proof