Memoryless concretization relation

TL;DR

Any abstraction of a system that alternatingly simulates a system can be completed to satisfy <Formula format="inline"><TexMath><?TeX $\operatorname{MCR}$?></TexMath><AltText>Math 7</AltText> at the expense of increasing the non-determinism in the abstraction.

Abstract

We introduce the concept of memoryless concretization relation (MCR) to describe abstraction within the context of controller synthesis. This relation is a specific instance of alternating simulation relation (ASR), where it is possible to simplify the controller architecture. In the case of ASR, the concretized controller needs to simulate the concurrent evolution of two systems, the original and abstract systems, while for MCR, the designed controllers only need knowledge of the current concrete state. We demonstrate that the distinction between ASR and MCR becomes significant only when a non-deterministic quantizer is involved, such as in cases where the state space discretization consists of overlapping cells. We also show that any abstraction of a system that alternatingly simulates a system can be completed to satisfy MCR at the expense of increasing the non-determinism in the abstraction. We clarify the difference between the MCR and the feedback refinement relation (FRR), showing in particular that the former allows for non-constant controllers within cells. This provides greater flexibility in constructing a practical abstraction, for instance, by reducing non-determinism in the abstraction. Finally, we prove that this relation is not only sufficient, but also necessary, for ensuring the above properties.

Figures (9)

• Figure 1: The three steps of abstraction-based control. Our work focuses on the algorithmic burden necessary for the third step, and characterizes the relation between the systems allowing for a memoryless algorithm at step three.
• Figure 2: Types of discretization of the concrete state space. Let $\mathcal{S}_{1} = (\mathcal{X}_1,\mathcal{U}_1,F_1)$ with $\mathcal{X}_1 = [0,1]^2$, $\mathcal{S}_{2} = (\mathcal{X}_2,\mathcal{U}_2,F_2)$ with $\mathcal{X}_2 = \{q_1,q_2,q_3,q_4\}$, $R_1 \subseteq \mathcal{X}_1\times \mathcal{X}_2$ and $R_2 \subseteq \mathcal{X}_1\times \mathcal{X}_2$ are explicit from the figure. Left: $R_1$ is a strict single-valued map, i.e., it induces a full partition of $\mathcal{X}_1$. Right: $R_2$ is a non-strict set-valued map, i.e., it induces a partial cover of $\mathcal{X}_1$.
• Figure 3: Local conditions between related states to satisfy the relation. Note that here, the relation is fixed (i.e., here a cover of the state space since $|R(x_1')|>1$) as well as the transition map of the concrete system and that we are simply changing the transition map of the abstract system. Left: The relation $R$ is a $\operatorname{ASR}$ but not a $\operatorname{MCR}$. Right: The relation $R$ is a $\operatorname{MCR}$.
• Figure 4: Dynamic controller architecture $\mathcal{C}_1$ such that $(\mathcal{S}_1,\mathcal{S}_2,\mathcal{C}_1,\mathcal{C}_2,R)$ satisfies the controlled simulability property if $\mathcal{S}_1\preceq_R^{\operatorname{ASR}} \mathcal{S}_2$. The red block is the interface$I_R^{\operatorname{ASR}}$. The yellow block contains the abstract system and the quantizer. The green block is the abstract controller. The blue blocks are delay blocks which represent memory elements that store and provide a past value of a signal, e.g., $D(x_2(k)) = x_2(k-1)$.
• Figure 5: Three transition systems $\mathcal{S}_1= (\mathcal{X}_1, \mathcal{U}_1 , F_1)$, $\mathcal{S}_2= (\mathcal{X}_2, \mathcal{U}_2 , F_2)$ and $\mathcal{S}_{2}'= (\mathcal{X}_2, \mathcal{U}_2, F_{2}')$ and a relation $R\subseteq \mathcal{X}_1\times\mathcal{X}_2$. Specifically, $\mathcal{X}_1 = (1,2,3,4,5)$, $\mathcal{U}_1 = \{0,1\}$, $\mathcal{X}_2 = (a,b,c,d,e,f)$, $\mathcal{U}_2 = \{\alpha, \beta, \gamma\}$, the transition maps $F_1$, $F_2$ and $F_{2}'$ and the available inputs maps $\mathcal{U}_1(.)$, $\mathcal{U}_{2}(.)$ and $\mathcal{U}_{2}'(.)$ are clear from the illustration, and $R = \{(1,a), (2,b),(2,c),(3,d),(4,e),(5,f)\}$. The colors of the node indicate the related states. Inputs labeled orange simply indicate that their values are not relevant to the current discussion. We consider the concrete specification $\Sigma_1^{\text{Reach}} =[\{1\}, \{5\}, \{3\}]$ and the associated abstract specification $\Sigma_2^{\text{Reach}} = \Sigma_{2}^{\text{Reach}'} =[\{a\}, \{f\}, \{d\}]$, where the initial, target and obstacle states are respectively in green, red and black.

Theorems & Definitions (25)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5: $\operatorname{ASR}$
• Definition 6: Interface
• Theorem 1
• proof
• Theorem 2
• proof