Scalable control synthesis for stochastic systems via structural IMDP abstractions

TL;DR

A novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs).

Abstract

This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. The focus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a class of robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form. We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systems that, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memory complexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of our methods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results.

Figures (6)

• Figure 1: An example of an where, given a source-action pair $(s, a)$ (the green state), the ambiguity set for the transition probability can be decomposed into the product between two independent interval ambiguity sets, ${ \Gamma}^1_{s,a}, { \Gamma}^2_{s,a}$. In this example, it is only necessary to store 9 transitions (per source-action pair) in contrast to 20 transitions for a traditional .
• Figure 2: On the left, for the green state, we report two marginal interval ambiguity sets, i.e. an interval ambiguity set for each marginal of a product ambiguity set, with outgoing transitions to all other states. On the right, an is constructed by multiplying the interval bounds of the marginal ambiguity sets. By this multiplication of bounds, joint distributions are introduced that cannot be represented as a product of distributions from the marginal ambiguity sets.
• Figure 3: An example of the recursive structure for the proposed algorithm for value iteration over . The example is for an with two marginals of three states each. Notice going right-to-left that we optimize over ${ \gamma}^2_{s,a}$ three times, as for each subproblem, we assume $t^1$ is given.
• Figure 4: Comparing $\varepsilon$ for a varying number of regions on the abstraction (assuming a uniform partition of the state space) and time horizons for both SySCoRe van2023syscore and .
• Figure 5: Mean error and 95$\%$ confidence interval, with respect to a uniform distribution of initial conditions, for various sizes of partitions for the car parking and building automation system benchmarks.

Theorems & Definitions (10)

• Remark 1
• definition 1: Probabilistic reach-avoid
• definition 2
• definition 3
• theorem 3
• Remark 4
• definition 4
• theorem 5
• proposition 1
• theorem 6