A Stability-Based Abstraction Framework for Reach-Avoid Control of Stochastic Dynamical Systems with Unknown Noise Distributions

TL;DR

This work tackles the scalability of abstraction-based controller synthesis for stochastic linear systems with unknown noise distributions by introducing a two-layer, stability-aware framework. A linear stabilizing feedback is used first to create a closed-loop, better-conditioned dynamics, after which an iMDP with interval transition probabilities is constructed to capture residual stochasticity via data-driven PAC guarantees. The main contributions include extending prior two-layer abstractions to achieve dramatically smaller graphs, establishing a probabilistic refinement relation that preserves reach-avoid guarantees, and demonstrating substantial size reductions (up to $90\%$) in practice with minimal performance loss when the stabilizing controller is aligned with the task. Numerical experiments on a double integrator and a spacecraft docking model illustrate the method’s effectiveness and highlight the critical role of alignment between the stabilizing controller and the reach-avoid objective for preserving performance. This approach enables more scalable, correct-by-construction control for safety-critical stochastic systems.

Abstract

Finite-state abstractions are widely studied for the automated synthesis of correct-by-construction controllers for stochastic dynamical systems. However, existing abstraction methods often lead to prohibitively large finite-state models. To address this issue, we propose a novel abstraction scheme for stochastic linear systems that exploits the system's stability to obtain significantly smaller abstract models. As a unique feature, we first stabilize the open-loop dynamics using a linear feedback gain. We then use a model-based approach to abstract a known part of the stabilized dynamics while using a data-driven method to account for the stochastic uncertainty. We formalize abstractions as Markov decision processes (MDPs) with intervals of transition probabilities. By stabilizing the dynamics, we can further constrain the control input modeled in the abstraction, which leads to smaller abstract models while retaining the correctness of controllers. Moreover, when the stabilizing feedback controller is aligned with the property of interest, then a good trade-off is achieved between the reduction in the abstraction size and the performance loss. The experiments show that our approach can reduce the size of the graph of abstractions by up to 90% with negligible performance loss.

Figures (3)

• Figure 1: A single-layer abstraction (a), versus our two-layer feedback design framework, which combines a stabilizing controller (linear feedback gain) with a symbolic controller (obtained from the abstraction). We impose constraints on both the total input $-Kx+u' \in U$ and on the input $u' \in U'$.
• Figure 2: Lower bound satisfaction probabilities (obtained from \ref{['thm:pac_control_design']}) for the integrator experiment with initial conditions $\bar{{x}} = (x_1, 0)$ for all $-41 \leq x_1 \leq 41$.
• Figure 3: Simulated trajectories and stabilized vector fields $(A-BK)x$ for both reach-avoid properties considered in the spacecraft problem (goal states in green; unsafe states in red). Case (a) is aligned, while case (b) is not.

Theorems & Definitions (19)

• Definition 1
• Definition 2: Reach-avoid property
• Definition 3: Satisfaction of $\varphi$
• Definition 4
• Remark 1
• Definition 5: DBLP:journals/jair/BadingsRAPPSJ23
• Definition 6
• Theorem 1: DBLP:journals/jair/BadingsRAPPSJ23
• Definition 7
• Remark 2: Equivalence relation