1 Introduction↩︎

The automated synthesis of correct-by-construction controllers for stochastic dynamical systems is crucial for their deployment in safety-critical scenarios. Synthesizing such controllers is challenging due to continuous and stochastic dynamics and the complexity of control tasks [1]. One solution is to abstract the system into a finite-state (also called symbolic) model [2]–[4]. Under an appropriate behavioral relation (e.g., a feedback refinement relation [5]), trajectories of the abstraction are related to those of the dynamical system. Thus, a controller (i.e., policy) in the abstraction can, by construction, be refined to a controller for the original system.

Conventional abstraction methods, however, rely on a precise mathematical model of the system. In relaxing this assumption, data-driven abstractions have recently gained momentum [6]–[13]. These methods take a black-box (or sometimes a gray-box, e.g., [10]) perspective and construct abstractions from sampled system trajectories. Several papers provide probably approximately correct (PAC) guarantees [7], [12], whereas others return controllers with hard (non-statistical) guarantees [6], [8], [11]. However, except from [13], none of these methods can handle stochastic systems.

In this paper, we take a middle route between these model-based and data-driven abstraction methods. Specifically, we consider control problems for linear systems with known deterministic dynamics but stochastic noise of an unknown distribution. This hybrid setting is similar to [14], [15], which develop a method to construct abstractions with PAC guarantees by sampling of the noise. However, due to their exhaustive discretization of the state space, the application to large-scale, industrial and realistic systems remains elusive.

A promising way to improve scalability is to exploit classical system properties, such as stability [16]. For example, [17] shows that for any stable discrete-time linear system with input constraints, there exists an approximately bismilar finite abstraction of any desired precision. Similar results hold for incrementally stable continuous-time switched [18] and nonlinear systems [19], [20]. A related notion is that of incremental forward completeness, which enables the abstraction of nonlinear discrete-time systems [21]. We observe that these results guarantee the existence of a certain type of abstraction if the system is stable. However, we postulate that stability may also be beneficial to construct finite-state abstractions with smaller underlying graphs.

= [draw, rectangle, minimum height=2em, minimum width=8em, text centered] = [draw, circle, node distance=1.5cm] = [coordinate] = [coordinate] = [pin edge=to-,thin,black]

Thus, the question central to this paper is: “How can the stability of a stochastic dynamical system be exploited to synthesize controllers via finite-state abstractions with smaller underlying graphs?” Our approach builds upon the hybrid abstraction technique for discrete-time stochastic linear systems developed in [14]. We consider tasks as reach-avoid properties, i.e., reach a set of goal states while always avoiding unsafe states. The control objective is to design a feedback controller such that the closed-loop system satisfies the reach-avoid task with at least a desired threshold probability.

Inspired by [14], we create an abstraction for discrete-time stochastic linear systems into an interval Markov decision process (iMDP) with PAC intervals of transition probabilities, which we compute using data-driven techniques for scenario programs with discarded constraints [22], [23]. A defining characteristic of this abstraction is that each abstract action is associated with a fixed distribution over (continuous) successor states. By contrast, other abstractions typically associate each abstract action with a fixed control input, such that the distribution over successor states depends on the precise continuous state where the abstract action is chosen. With our approach, we avoid this issue at the cost of more restrictive assumptions on the dynamics (1).

Instead of abstracting the open-loop dynamics directly (as in [fig:1layer]), we propose the two-layer feedback control design framework in [fig:2layer]. In this framework, we first stabilize the system with a linear feedback gain and then abstract the stabilized dynamics. This approach delegates part of the control effort to the stabilizing controller, which allows us to further constrain the control input synthesized in the abstraction. Especially if the stabilizing controller contributes to satisfying the reach-avoid task, we can reduce the number of edges in the graph of the abstraction significantly (by up to 90%; see 5) with negligible performance loss.

Contributions↩︎

As our main contribution, we extend the abstraction method from [14] to the two-layer abstraction in [fig:2layer] and show that this new scheme can be used to construct abstractions with smaller underlying graphs. We show that the formal relation induced by the abstraction from [14] carries over to our setting. Our experiments exemplify the conditions necessary for a good trade-off between abstraction size and controller performance.

2 Preliminaries↩︎

A probability space \(( \Omega, \mathcal{F}, \amsmathbb{P} )\) consists of an uncertainty space \(\Omega\), a \(\sigma\)-algebra \(\mathcal{F}\), and a probability measure \(\amsmathbb{P}\colon \mathcal{F} \to [0,1]\). A random variable \(x\) is a measurable function \(x \colon \Omega \to \amsmathbb{R}^n\) for some \(n \in \amsmathbb{N}\), which takes value \(x(\omega) \in \amsmathbb{R}^n\) for \(\omega \in \Omega\). We denote the set of all distributions for both a continuous and discrete set \(X\) by \(\mathcal{P}(X)\). The convex hull of a set of points \(\{v_1, \ldots, v_m\}\) in \(\amsmathbb{R}^n\) is \(\mathrm{conv}(v_1,\ldots,v_n)\). We denote the interior of \(V \subset \amsmathbb{R}^n\) by \(\mathrm{int(V)}\) and the pseudoinverse of matrix \(B\) by \(B^\dagger\). The indicator function \(\mathbb{1}_V(x)\) for a set \(V \subset \amsmathbb{R}^n\) is one if \(x \in V\) and zero otherwise. The Cartesian product of an interval is written as \([a,b]^n\), for \(a \leq b\), \(n \in \amsmathbb{N}\).

2.1 Stochastic dynamical systems↩︎

Consider a discrete-time, stochastic linear dynamical system \(\mathcal{S}\) where the state space variable \(x_k \in \amsmathbb{R}^n\) evolves as \[\label{eq:linear95system} \mathcal{S}: \,\, x_{k+1} = A{x}_k + B{u}_k + {\eta}_k, \quad x_0 = \bar{x},\tag{1}\] where \(\bar{x} \in \amsmathbb{R}^n\) is the initial condition, \({u}_k \in \amsmathbb{R}^p\) is the control input, and \({\eta}_k \in \amsmathbb{R}^n\) is a stochastic noise. Matrices \(A\) and \(B\) have the appropriate dimensions. The control input is constrained to a convex polytope \(U= \{ u \in \amsmathbb{R}^p : Gu \leq g\} \subset \amsmathbb{R}^p\) called the admissible control input, where \(G \in \amsmathbb{R}^{q \times p}\) and \(g \in \amsmathbb{R}^q\). Moreover, \(({\eta}_k)_{k \in \amsmathbb{N}_0}\) is a discrete-time stochastic process defined on a probability space \((\Omega,\mathcal{F},\amsmathbb{P})\), with its natural filtration (see [24] for details). Thus, \(({x}_k)_{k \in \amsmathbb{N}_0}\) is also a stochastic process in the same probability space.

2 requires process \(({\eta}_k)_{k \in \amsmathbb{N}}\) to be i.i.d. and to possess a well-defined probability density. However, we do not assume knowledge of its density. Under 2, system 1 can be equivalently expressed using the stochastic kernel (see [26] for details) \(T \colon \amsmathbb{R}^n \times U\to \mathcal{P}(\amsmathbb{R}^n)\), which maps each state-input pair to a distribution over states: \[\label{eq:linear95system95kernel} x_{k+1} \sim T(\cdot \mid x_k,u_k), \quad x_0 = \bar{x}.\tag{2}\] For example, if \({\eta}_k \sim \mathcal{N}(\mu , \Sigma), \, k \in \amsmathbb{N}\) is Gaussian, the stochastic kernel is given by \(T(\cdot \mid x_k,u_k) = \mathcal{N}(Ax_k + Bu_k + \mu , \Sigma)\). A time-varying feedback controller chooses the inputs \({u}_k \in U\) by measuring the current state.

2.2 Problem statement↩︎

Given a system as in 1 , our goal is to find a time-varying controller \(c\) such that the closed-loop system with \(u_k = c(x_k,k)\), for all \(k \in \amsmathbb{N}\), satisfies some objective. Specifically, we consider the objective of reaching a desired region \(X_G\) of the state space while always avoiding unsafe states \(X_U\).

For system \(\mathcal{S}\) in 1 , we consider \(X_G, X_U\subset \amsmathbb{R}^n\) as compact subsets of \(\amsmathbb{R}^n\) and use the notation \(\varphi= (X_G,X_U, H)\) for this reach-avoid property. A trajectory \({x}_0, {x}_1, \ldots, x_H\) of length \(H\) for system \(\mathcal{S}\) satisfies \(\varphi\) if there exists a \(k \in \{0,\ldots,H\}\) such that \(x_k \in X_G\) and \(x_{k'} \notin X_U\) for all \(k' \in \{0,\ldots,k\}\). Under a fixed controller, system \(\mathcal{S}\) induces a stochastic process \((x_k)_{k \in \amsmathbb{N}_0}\) for which we can reason over the probability of satisfying a reach-avoid property [26].

We are now able to describe our control objective.

2.3 Markov decision processes↩︎

Our approach for solving 1 is to create a discrete abstraction of system \(\mathcal{S}\) into an MDP with imprecise transition probabilities. To distinguish from system \(\mathcal{S}\), we call abstract states locations and a controller for the abstraction a policy.

For any iMDP, we require that \(\check{P}_{s'}(s,a) \leq \hat{P}_{s'}(s,a)\) for all \(s, s' \in S, a \in \mathcal{A}(s)\), and that \(\sum_{s' \in S} \check{P}_{s'}(s,a) \leq 1 \leq \sum_{s' \in S} \hat{P}_{s'}(s,a)\) for all \(s \in S, a \in \mathcal{A}(s)\); otherwise, the set ?? may be empty. An adversary fixes a probability \(P'(s,a)(s') \in P(s,a)\) for all pairs \((s,a) \in S\times \mathcal{A}\). Importantly, a different \(P'\) can be chosen every time the same pair \((s,a)\) is encountered. For brevity, we overload notation and use \(P' \in P\) to denote choosing an adversary in the set of all adversaries.

Actions are chosen by a time-varying policy \(\pi\colon S \times \amsmathbb{N}_0 \to \mathcal{P}(\mathcal{A})\), which maps every location \(s \in S\) and time \(k \in \amsmathbb{N}_0\) to an action \(a \in \mathcal{A}\).² The set of all admissible policies³ is \[\Pi= \big\{ \pi\colon S \times \amsmathbb{N}_0 \to \mathcal{P}(\mathcal{A}) \, \mid \, \pi(s,k)(a) > 0 \implies a \in \mathcal{A}(s) \big\}.\]Thus, any policy \(\pi\in \Pi\) requires that for all \(k \in \amsmathbb{N}\) and \(s\in S\), the support of the distribution \(\pi(s,k)\) is contained in \(\mathcal{A}(s)\).

For an iMDP, a reach-avoid property \(\varphi' = (S_G, S_U, H)\) (cf. 2) is defined over the locations, i.e., \(S_G, S_U \subseteq S\). The semantics over trajectories \(s_0, s_1,\ldots, s_{H}\) are the same as for system \(\mathcal{S}\). Similar to 3, for any policy \(\pi\in \Pi\) and transition function \(P' \in P\), we denote the probability of satisfying \(\varphi'\) by \(\mathrm{Pr}_{P'}^\pi(\bar{s} \models \varphi')\).⁴ An optimal (robust) policy \(\pi^\star \in \Pi\) optimizes the next min-max problem: \[\label{eq:optimal95policy} \pi^* \in \mathop{\mathrm{arg\,max}}_{\pi\in \Pi} \, \min_{P' \in P} \mathrm{Pr}_{P'}^\pi( \bar{s} \models \varphi').\tag{3}\]

3 Abstraction-Based Controller Synthesis↩︎

We formally relate the dynamics in 1 to a finite iMDP, using a probabilistic variant of a feedback refinement relation [5]. Then, we establish that the abstraction proposed by [14] induces this relation. A measurable set \(R \subseteq \amsmathbb{R}^n \times S\) is called a binary relation, for which we use notations \(R(x) = \{ s \in S: (x,s) \in R \}\) and \(R^{-1}(s) = \{ x \in \amsmathbb{R}^n : (x,s) \in R \}\).

Similar to [5], we denote a probabilistic feedback refinement relation \(R\) from \(\mathcal{I}\) to \(\mathcal{S}\) by \(\mathcal{I}\preceq_R \mathcal{S}\). Moreover, we also use the relation \(R\) in 5 to relate reach-avoid properties between system \(\mathcal{S}\) and an iMDP.

Intuitively, given an iMDP path \(s_0, s_1, \ldots, s_H\) that satisfies \(\varphi'\), the relation \(\varphi' \preceq_R \varphi\) implies that all related trajectories \(x_0, x_1, \ldots, x_H\), i.e., trajectories for which \((x_i, s_i) \in R \,\) for all \(i = 0,\ldots,H\), must satisfy \(\varphi\). The following result, which is proven in [15], shows that 5 6 can be used to synthesize correct-by-construction controllers for system \(\mathcal{S}\).

The proof of 1 uses that, for MDPs, the relation \(R\) preserves the satisfaction of probabilistic computation tree logic (PCTL), in which the reach-avoid property in 2 can be expressed [29]. For iMDPs, this preservation of probabilistic satisfaction leads to the inequality in ?? . In fact, 1 can be extended to any PCTL formula; see, e.g., [30]. However, since our contributions are unrelated to the property, we focus on reach-avoid properties for simplicity.

3.1 Abstraction procedure↩︎

We revisit the abstraction developed in [14], [15], which first uses a model-based approach to compute the abstract locations and actions. Second, a data-driven approach is used to capture the stochastic uncertainty into intervals of transition probabilities. The resulting abstraction is an iMDP that creates a relation as in 6 with a pre-defined confidence level.

3.1.1 Model-based locations and actions↩︎

The locations of the abstraction are given by a polyhedral partition of a bounded portion \(\mathcal{X}\subset \amsmathbb{R}^n\) of the state space of system \(\mathcal{S}\):

Adding the final element \(\amsmathbb{R}^n \setminus \mathcal{X}\) ensures that the partition covers \(\amsmathbb{R}^n\). A partition creates an equivalence relation [31].

The locations of the abstraction are the equivalence classes of the partition, i.e., \(S \mathrel{\vcenter{:}}= \amsmathbb{R}^n /{\mathord{\sim}}\). Next, the set of actions is \(\mathcal{A}\mathrel{\vcenter{:}}= \{a_1, \ldots, a_q\}\), \(q \in \amsmathbb{N}\), where each \(a \in \mathcal{A}\) is associated with a target point \({d}_a \in \amsmathbb{R}^n\) in the state space of \(\mathcal{S}\). For each point \({d}_a\), for \(a \in \mathcal{A}\), we define the backward reachable set as \[\begin{align} \label{eq:backward95reachable95set} \mathcal{R}^{-1}(d_a) &= \{ x \in \amsmathbb{R}^n : d_a = Ax + Bu, \, u \in U\} \\ &= \mathrm{conv}\big( A^{-1}({d}_a - B v^i) \,:\, i = 1,\ldots,q \big), \end{align}\tag{4}\] where the second equality follows from 1. The set \(\mathcal{A}(s) \subseteq \mathcal{A}\) of actions enabled in location \(s \in S\) is \[\label{eq:enabled95actions} \mathcal{A}(s) = \big\{ a \in \mathcal{A}\mid s \subseteq \mathcal{R}^{-1}({d}_a) \big\}.\tag{5}\] Thus, action \(a \in \mathcal{A}\) is enabled in location \(s \in S\) only if the equivalence class \(s\) is contained in the backward reachable set \(\mathcal{R}^{-1}({d}_a)\). Choosing abstract action \(a \in \mathcal{A}\) is defined such that \({d}_a = Ax + Bu\), which implies that \(u = B^\dagger({d}_a - Ax)\).⁵ Since the noise is additive, the successor state is \({d}_a + {\eta}\), which is a random variable with distribution \(T(\cdot \mid x, B^\dagger({d}_a - Ax) )\).

3.1.2 Data-driven transition probabilities↩︎

As the distribution of the noise is unknown, we use a finite set of samples of \({\eta}_k\) to compute an interval on the probability of reaching each location \(s \in S\). Formally, let \(\{\delta_1,\ldots,\delta_N\} \in \Omega^N\), where \(N \in \amsmathbb{N}\) is the number of samples⁶ of \({\eta}_k\). For each pair \(s, s' \in S\) and enabled action \(a \in \mathcal{A}(s)\), the interval \([\check{P}_{s'}(s,a), \hat{P}_{s'}(s,a)]\) is computed such that the exact probability is contained with at least a desired probability of \(1-\beta\), with \(\beta \in (0,1)\): \[\begin{align} \nonumber \amsmathbb{P}^N \Big\{ \,\, \check{P}_{s'}(s,a) &\leq \int_{\amsmathbb{R}^n} \mathbb{1}_{s'}(\xi) T( d\xi \mid x, \, [B^\dagger(d_a-Ax)] ) \\ &\leq \hat{P}_{s'}(s,a) \,\, \Big\} \geq 1-\beta, \label{eq:iMDP95intervals} \end{align}\tag{6}\] where \(x\) is such that \([x] = s\), state \(s' \in S= \amsmathbb{R}^n /{\mathord{\sim}}\) is interpreted as a subset of \(\amsmathbb{R}^n\), and the outer probability is taken w.r.t. the upper bound \(\hat{P}_{s'}(s,a)\) and lower bound \(\check{P}_{s'}(s,a)\) of the interval, which are random variables in the space \(\Omega^N\).

In practice, we compute these intervals using the method from [15], which leverages the scenario approach [22]. This method implicitly solves a set of \(2N\) convex scenario programs with discarded constraints [32] and uses [23] to compute tight bounds on the probability of constraint violation for each of these programs. By construction, one of these \(2N\) probabilities of constraint violations lower bounds the transition probability in 6 , and another one is an upper bound. By choosing the confidence level on the probability of constraint violation for each scenario program as \(1-\frac{\beta}{2N}\), we obtain a probability interval such that 6 holds. It is shown in [15] that these scenario programs can be solved analytically based on its geometry, making the approach highly efficient. Due to space restrictions, we refer to [15] for formal details.

3.1.3 Complete abstraction↩︎

Putting all elements together, we define the iMDP abstraction \((S, \bar{s}, \mathcal{A}, \check{P}, \hat{P})\), with

• Set of locations \(S = \amsmathbb{R}^n /{\mathord{\sim}}\), with \(\bar{s} = [\bar{x}]\);

• Actions \(\mathcal{A}= \{a_1,\ldots,a_q\}\), for \(q \in \amsmathbb{N}\), with the enabled actions \(\mathcal{A}(s)\) defined by 5 for all \(s \in S\);

• For each \(s,s' \in S\) and \(a \in \mathcal{A}(s)\), the lower and upper bound probabilities \(\check{P}_{s'}(s,a)\) and \(\hat{P}_{s'}(s,a)\) are such that 6 holds for a desired value of \(\beta \in (0,1)\).

3.2 Controller synthesis↩︎

We show that the equivalence relation \({\sim} \subset \amsmathbb{R}^n \times S\) created by the partition (cf. 2) is (with a certain probability) a probabilistic feedback refinement relation \(R\) from iMDP \(\mathcal{I}\) to system \(\mathcal{S}\), as defined by the conditions in 5.

The iMDP has at most \(|\mathcal{A}| \cdot |S|\) unique probability intervals (see [15] for details). We have that \(\mathcal{I}\preceq_\sim \mathcal{S}\) if all of these intervals contain the exact probability, which (by applying the union bound) is satisfied with a probability of at least \(1 - \beta \cdot |\mathcal{A}| \cdot |S|\). Thus, the claim follows.

Under 1, we can refine any policy for the abstract iMDP into a controller of the form in 1.

Finally, we obtain the following key result for the iMDP abstraction and the refined controller defined above.

Thus, the satisfaction probability on the iMDP is a lower bound on the satisfaction probability for system \(\mathcal{S}\) under the refined controller, with probability at least \(1-\beta \cdot |\mathcal{A}| \cdot |S|\).

4 Exploiting Stability in Abstraction↩︎

The size of the iMDP abstraction (which can be expressed by the number of edges, or transitions, in the underlying graph) from 3 grows exponentially with the dimension of the state space. In this section, we develop an extension to the method from [14] to create smaller abstractions. As our key contribution, we leverage the two-layer control design framework in [fig:2layer], which first stabilizes the dynamics and then creates an abstraction of the closed-loop dynamics. Specifically, we use the feedback control law given by \[{u}_k = -K x_k + {u}'_k, \label{eq:two-layer-control-law}\tag{7}\] where the gain matrix \(K \in \amsmathbb{R}^{m \times n}\) represents a stabilizing control law, and \(u'\) is the control input captured by the abstraction. In this paper, we obtain the feedback gain matrix by solving an instance of a linear quadratic regulator (LQR) [16] control problem. Applying the feedback control law in 7 to system 1 yields the closed-loop dynamics given by \[\label{eq:dynamics95double95input} {x}_{k+1} = A_\mathrm{cl} {x}_k + B {u}'_k + {\eta}_k,\tag{8}\] where \(A_\mathrm{cl} = A-BK\). We assume that the feedback gain \(K\) satisfies the input constraints in the following way.

4.1 Backward reachable set for stabilized dynamics↩︎

We show how the iMDP abstraction described in 3 can be employed together with the two-layer feedback control law in 7 . The key step is that we modify the backward reachable set computation in 4 , replacing it by \[\begin{align} \label{eq:backward95reachable95set95stable} \mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U') = \big\{ {x}\in \amsmathbb{R}^n : \,\, &{d}_a = A_\mathrm{cl} {x}+ B{u}', \\ &-K{x}+ {u}' \in U, \, {u}' \in U' \big\}, \nonumber \end{align}\tag{9}\] where the constraint \(-K {x}+ {u}' \in U= \{ u \in \amsmathbb{R}^m : Gu \leq h\}\) enforces that the total input \(u\) is admissible, and the constraint \({u}' \in U' = \{ u \in \amsmathbb{R}^m : G'u \leq h'\}\) controls the size of the abstraction. Matrices \(G\) and \(G'\) and vectors \(h\) and \(h'\) define the admissible control inputs; their sizes are omitted for brevity.

Observe that 9 is of the same form as 4 (despite imposing additional constraints) and can thus be computed similarly, as shown by the following lemma.

Item \(i)\): We will show that the point \(\tilde{x} = A_{\mathrm{cl}}^{-1}d_a \in \mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U')\). Note that this point \(\tilde{x}\) is obtained for \({u}' = 0\) in 9 , which is an admissible input due to 4. Moreover, due to 3, we have that \(-K x \in U\), and thus, it holds that \(\tilde{x} \in \mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U')\), which concludes the proof of item \(i)\). Item \(ii)\): Solving the equality constraint in 9 for \(x\) yields \(x = A_\mathrm{cl}^{-1}({d}_a - Bu)\), so the input constraint \(-Kx + u' \in U\) can be written as \[\label{eq:lemma1:proof1} -K A_\mathrm{cl}^{-1}{d}_a + (I + K A_\mathrm{cl}^{-1}B) u' = \alpha + \beta u' \in U.\tag{10}\] Thus, we have two convex polyhedral constraints on \(u\), given by \(\alpha + \beta u' \in U= \{ u \in \amsmathbb{R}^m : Gu \leq h\}\) and \(u' \in U' = \{ u \in \amsmathbb{R}^m : G'u \leq h'\}\). The intersection of the feasible sets for \(u\) is the set \(\tilde{U}\) in ?? , concluding the proof of item \(ii)\).

Observe that, while we can compute \(\mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U')\) similarly as in 3, the number of vertices to consider is generally higher due to the additional input constraint \(u' \in U'\).

4.2 Constructing smaller abstractions↩︎

We can use the modified backward reachable set in 9 to construct abstractions with fewer enabled actions, as illustrated by the following lemma.

Letting \(U' = \amsmathbb{R}^p\) and \(A_\mathrm{cl} = A-BK\) in 9 gives \[\begin{align} {2} \mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U') &= \big\{ {x}\in \amsmathbb{R}^n : \,\, &&{d}_a = A{x}+ B(-K{x}+ {u}'), \,\, \\ & &&-K{x}+ {u}' \in U \big\} \\ &= \big\{ {x}\in \amsmathbb{R}^n : \,\, &&{d}_a = A{x}+ Bu, \,\, u \in U \big\} \\ &= \mathcal{R}^{-1}({d}_a), && \end{align}\] thus proving the first claim. For \(U'' \subset U'\), observe from 9 that \(u' \in U'' \subset U'\). Thus, we obtain that \(\mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U'') \subseteq \mathcal{R}^{-1}_{\mathrm{cl}}({d}_a, U')\), which proves the second claim.

Recall from 3 that an action \(a \in \mathcal{A}\) is enabled in location \(s \in S\) if and only if the corresponding partition element is contained in the backward reachable set \(\mathcal{R}^{-1}({d}_a)\). In the modified backward reachability set in 9 , we can control the size of \(\mathcal{R}^{-1}_{\mathrm{cl}}({d}_a)\) through \(U'\). In fact, 2 shows that by shrinking the set \(U'\), we may reduce the number of enabled actions at each state and, consequently, the size of the graph of the iMDP. In the next section, we show how suitable choices for the feedback gain \(K\) and input constraint \(U'\) may lead to significantly smaller iMDP abstractions.

5 Numerical Experiments↩︎

We implement our method in a Python tool, which is available at https://github.com/LAVA-LAB/DynAbs. We use the model checker PRISM [33] to compute optimal policies as per 3 for iMDPs. In all experiments, we apply 3 with an overall confidence of \(1-\beta \cdot |\mathcal{A}| \cdot |S| = 0.99\). For simplicity, we use partitions into rectangular regions.

5.1 Double integrator↩︎

Consider a stochastic system with dynamics given as \[{x}_{k+1} = \begin{bmatrix} \frac{1}{\rho^2} & \frac{1 + \rho}{+} 1 \\ 0 & 1 \end{bmatrix} {x}_k + \begin{bmatrix} \frac{0.5 + \rho}{\rho} & 0.5 \\ 1 & 1 \end{bmatrix} (-K{x}_k + {u}_k') + {\eta}_k, \label{eq:ExperimentDynamics:FullyActuated}\tag{11}\] where we apply the control law given in 7 , and the noise \(\eta_k \sim \mathcal{N}(0 , I_2)\) has a standard normal distribution and satisfies the conditions in Assumption 2. We select \(\rho = 2\) to render the system unstable when a trivial control of \(-Kx_k + u'_k = 0\) is applied. The reach-avoid task is to reach a state \(x \in [-3, 3]^2\) while avoiding states \(x \notin [-41,41]^2\) within \(H= 16\) steps.⁸ We partition the set \(\mathcal{X}= [-41,41]^2\) into \(41\) by \(41\) rectangular regions of width two. The input constraint is \(U= [-60,60]^2\).

Baseline↩︎

As a baseline, we set \(K=0\) and construct the single-layer iMDP abstraction (as outlined in 3) with input constraint \(U= [-60,60]^2\). The resulting iMDP has 39.8 million transitions, and the lower bounds on the satisfaction probabilities (obtained from 3) are shown in 2 for a range of initial states \(\bar{x} = (x_1, 0)\) for \(x_1 \in [-41, 41]\).

Stabilizing controller↩︎

We now use our two-layer abstraction scheme, where we compute the gain \(K\) with an LQR with cost matrices \(Q = R = I_2\), yielding \((A-BK)\) having eigenvalues of \(\lambda = 0.178 \pm 0.136i\). We construct the iMDP for the different sets \(U\) and \(U'\) shown in 1, presenting the lower bound satisfaction probabilities for two cases in 2. With our method, we construct significantly smaller abstractions with little loss in probabilistic guarantee. For example, with \(|U| = 60\), \(|U'| = 20\), the number of iMDP transitions is reduced from 39.8 to 15.8 million at negligible loss in probabilistic guarantee. Shrinking the set \(U'\) further reduces the iMDP size; however, at the cost of a considerable reduction in probabilistic guarantee, as shown in [fig:integrator95baseline].

Aligned property.

Disaligned property.

5.2 Spacecraft docking↩︎

We consider the spacecraft docking problem from [34], with \(x \in \amsmathbb{R}^4\) modeling the position and velocity in two dimensions (see [34] for the full model). We illustrate that our method generally works well if the stabilizing feedback controller is aligned with the reach-avoid property. That is, the stabilizing controller should steer the state \(x\) towards the goal region \(X_G\subset \amsmathbb{R}^4\), while steering clear from the unsafe states \(X_U\subset \amsmathbb{R}^4\). We consider the two reach-avoid problems shown in 3 (only the position state variables are shown). As a baseline, we construct the abstraction with a partition into \(3\,200\) elements and an input constraint \(U= [-0.1, 0.1]^2\). For the reach-avoid problem in 3 (a), the resulting iMDP has 1.6 million transitions and leads to a lower bound satisfaction probability of \(0.80\) in 3. Similarly, for the problem in 3 (b), the iMDP has 2.1 million transitions and leads to a lower bound satisfaction probability of \(0.86\).

Now, we apply our method with \(U' = [-0.08, 0.08]^2\), resulting in iMDPs with 280 and 330 thousand transitions (reductions of 79% and 85% respectively). For the problem in 3 (a), the lower bound on the satisfaction probability is \(0.79\) (only \(0.01\) below the baseline). However, for 3 (b), the bound drops to \(0.0072\), i.e., almost zero. To explain this severe performance loss, we show simulated trajectories under the refined controller (as per 8) in 3. Moreover, the arrows show the vector field under the stabilized dynamics, i.e., \((A-BK)x\) for different \(x \in \amsmathbb{R}^n\). In 3 (a), the vector field points to the goal region and away from unsafe states, and is thus aligned with the property. By contrast, the vector field in 3 (b) is not aligned since it steers the system into unsafe states, causing a performance loss of the controller.

6 Conclusion↩︎

In this paper, we have developed a novel formal abstraction method for stochastic linear dynamical systems that exploits stability to generate smaller abstract models. By stabilizing the dynamics with a linear feedback gain first, we have shown that we can reduce the size of abstractions (in terms of the number of edges in the underlying graph) significantly. Our experiments have shown that, when the feedback gain steers the system toward the goal states (and away from the unsafe states), we can reduce the number of transitions by up to \(90\%\) with negligible performance loss.

However, if the stabilizing controller is not aligned with the control task (as in 3 (b)), the controller performance degrades significantly. One possible solution is to use a piece-wise affine trajectory-tracking controller, which selects different gains in different regions of the state space. Exploring this latter approach will be the next step of our research.

References↩︎

---

1. This research has been partially funded by an NWO grant NWA.1160.18.238 (PrimaVera), ERC Starting Grant 101077178 (DEUCE), and a JPMC faculty research award. T. Badings and N. Jansen are with the Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands; {thom.badings, nils.jansen}@ru.nl. N. Jansen is also with the Faculty of Computer Science, Ruhr-Universität Bochum, Germany. L. Romao and A. Abate are with the Department of Computer Science, Oxford University; {licio.romao, alessandro.abate}@cs.ox.ac.uk.↩︎

2. Time-varying policies are needed to attain optimal values for the time-bounded properties we consider [27]. An equivalent approach is to encode the time step explicitly in the iMDP by defining the set of locations \(S' = S \times \{0,\ldots,H\}\) and using memoryless policies \(\pi\colon S' \to \mathcal{A}\) instead.↩︎

3. The policy class \(\Pi\) suffices to obtain optimal policies for iMDP [28].↩︎

4. Fixing a policy \(\pi\in \Pi\) and an adversary with \(P' \in P\) induces a Markov chain with probability measure \(\mathrm{Pr}_{P'}^\pi\); see [27] for details.↩︎

5. Action \(a\) is only enabled in equivalence classes that are a subset of the backward reachable set \(\mathcal{R}^{-1}({d}_a)\). Thus, we have \(u = B^\dagger(d_a-Ax) \in U\) by construction for any state \(x \in \bigcup \big\{ s \in S \mid a \in \mathcal{A}(s) \big\} \subset \amsmathbb{R}^n\).↩︎

6. Since 1 is time-invariant and has additive noise, we can obtain these samples from a single trajectory of length \(N\) starting at an arbitrary state \(\bar{x}\).↩︎

7. If \(x \in \amsmathbb{R}^n\) is on the boundary of multiple partition elements, the refined controller can select any location \(s = [x]_\sim \in S\).↩︎

8. The correctness of our iMDP abstraction is independent of the horizon. For numerical experiments with an infinite time horizon, we refer to [15].↩︎