Classification of simulation relations for symbolic control

TL;DR

This work develops a unified framework for classifying simulation relations in symbolic control by introducing an augmented system and a universal interface that realize plug-and-play concretization. It shows that the existence of a relation of type $\mathrm{T}$ between a concrete system $\mathcal{S}_1$ and an abstract system $\mathcal{S}_2$ is equivalent to a feedback refinement relation on the augmented pair, enabling seamless concretization of any abstract controller. Five key relations (ASR, FRR, PSR, FAR, MCR) are placed into a single framework, with explicit interface constructions and comparative insights into their concretization architectures, complexity, and memory requirements. The results yield a practical, constructive pathway to design and connect abstract controllers to real systems, highlighting trade-offs between corrective/predictive strategies and memoryless versus memoryful implementations. The framework lays groundwork for extending to other relation types and output-feedback settings, strengthening the applicability of abstraction-based control in safety-critical CPS.

Abstract

Abstraction-based control design is a promising approach for ensuring safety-critical control of complex cyber-physical systems. A key aspect of this methodology is the relation between the original and abstract systems, which ensures that the abstract controller can be transformed into a valid controller for the original system through a concretization procedure. In this paper, we provide a comprehensive and systematic framework that characterizes various simulation relations, through their associated concretization procedures. We introduce the concept of augmented system, which universally enables a feedback refinement relation with the abstract system. This augmented system encapsulates the specific characteristics of each simulation relation within an interface, enabling a plug-and-play control architecture. Our results demonstrate that the existence of a particular simulation relation between the concrete and abstract systems is equivalent to the implementability of a specific control architecture, which depends on the considered simulation relation. This allows us to introduce new types of relations, and to establish the advantages and drawbacks of different relations, which we exhibit through detailed examples.

Figures (6)

• Figure 1: The three steps of abstraction-based control. Our work focuses on the connection between the type of relation between $\mathcal{S}_1$ and $\mathcal{S}_2$ (step 1) and the concretization procedure (step 3). We show that one can taylor the abstraction relation depending on the required properties of the concretization step and of the finally obtained concrete controller, independently of the abstract controller synthesis step (step 2).
• Figure 2: Closed-loop system resulting from the abstraction and concretization approach. Left: Based on the feedback refinement relation. Right: Based on the interface proposed in this paper.
• Figure 3: Feedback composition $\mathcal{S}_1\times \mathcal{S}_2$ of systems $\mathcal{S}_1$ and $\mathcal{S}_2$ in \ref{['eq:sys']} where $H_2'(x) = \{y_2\mid \exists u_2\in\mathcal{U}_2:\ (y_2,u_2)\in H_2(x_2,u_2)\}$ (see Definition \ref{['def:feedback_composition']}). The blue blocks are delay blocks which represent memory elements that store and provide the previous value of a signal, e.g., $D(x_2(k)) = x_2(k-1)$.
• Figure 4: Concretization of an abstract controller $\mathcal{C}_2$ into a concrete controller $\mathcal{C}_1^{\mathop{\mathrm{T}}\nolimits}$ for the relation $\mathcal{S}_1 \preceq_R^{\mathop{\mathrm{T}}\nolimits} \mathcal{S}_2$ using the interface $(\mathcal{Z}_1, h_1^{\mathop{\mathrm{T}}\nolimits}, h_2^{\mathop{\mathrm{T}}\nolimits}, \widetilde{R})$. (a) Depicts the augmented system $\widetilde{\mathcal{S}}_1^{\mathop{\mathrm{T}}\nolimits}$, where $\widetilde{\mathcal{S}}_1 \preceq_{\widetilde{R}}^{\mathop{\mathrm{FRR}}\nolimits} \mathcal{S}_2$, with controller $\widetilde{\mathcal{C}}_1 = \mathcal{C}_2 \circ \widetilde{R}$\ref{['eq:concrete_controller_FRR_def']}. Dotted lines show the relations between systems. The remaining subfigures illustrate specific implementations (Definition \ref{['def:interface_relations_specific_augmented']}) for $\mathop{\mathrm{T}}\nolimits \in \{\mathop{\mathrm{ASR}}\nolimits, \mathop{\mathrm{PSR}}\nolimits, \mathop{\mathrm{FAR}}\nolimits, \mathop{\mathrm{MCR}}\nolimits, \mathop{\mathrm{FRR}}\nolimits\}$.
• Figure 5: Illustration of $(x_2,u_2,x_1,u_1)\in R_e^{\mathop{\mathrm{ASR}}\nolimits}$ and $R_e^{\mathop{\mathrm{MCR}}\nolimits}$ for Example \ref{['example:2D']}. The cell $R^{-1}(x_2) = \mathcal{S}(x_2, \epsilon)$ and its image under the dynamic $F_1$ are represented in blue. The grey circle $\mathcal{A}\coloneqq \mathcal{S}(f(x_2, u_2), \rho \epsilon)$ is the over-approximation of the reachable set of $R^{-1}(x_2)$. The set $F_2^{\mathop{\mathrm{ASR}}\nolimits}(x_2, u_2)$ just needs to contain enough cells so that their union covers the set $\mathcal{A}$, for example, only the red cells. While the set $F_2^{\mathop{\mathrm{MCR}}\nolimits}(x_2, u_2)$ must at least contain all the cells intersecting $\mathcal{A}$, which are shown in red and green. Therefore, in this example, we have $|F_2^{\mathop{\mathrm{ASR}}\nolimits}(x_2,u_2)| = 4$ while $|F_2^{\mathop{\mathrm{MCR}}\nolimits}(x_2,u_2)| = 15$.

Theorems & Definitions (36)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Definition 6
• Definition 7
• Theorem 1: tabuada2009verification
• Definition 8
• Theorem 2: reissig2016feedback