Compositional abstraction and safety synthesis using overlapping symbolic models
KTH Royal Institute of Technology（皇家理工学院）；Laboratoire des signaux et systèmes (L2S), CNRS, CentraleSupélec, Université Paris-Sud, Université Paris-Saclay（信号与系统实验室，法国国家科学研究中心，中央苏佩莱克高等学院，巴黎第十一大学，巴黎萨克雷大学）；Univ. Grenoble Alpes/CNRS, GIPSA-Lab（格勒诺布尔阿尔卑斯大学/法国国家科学研究中心，GIPSA实验室）
Pierre-Jean Meyer, Antoine Girard, Emmanuel Witrant
In this paper, we develop a compositional approach to abstraction and safety synthesis for a general class of discrete time nonlinear systems. Our approach makes it possible to define a symbolic abstraction by composing a set of symbolic subsystems that are overlapping in the sense that they can share some common state variables. We develop compositional safety synthesis techniques using such overlapping symbolic subsystems. Comparisons, in terms of conservativeness and of computational complexity, between abstractions and controllers obtained from different system decompositions are provided. Numerical experiments show that the proposed approach for symbolic control synthesis enables a significant complexity reduction with respect to the centralized approach, while reducing the conservatism with respect to compositional approaches using non-overlapping subsystems.
In this paper, we introduce a compositional method for the construction of finite abstractions of interconnected discrete-time switched systems. Particularly, we use a notion of so-called alternating simulation function as a relation between each switched subsystem and its finite abstraction. Based on some small-gain type conditions, we use those alternating simulation functions to construct compositionally an overall alternating simulation function as a relation between an interconnection of finite abstractions and that of switched subsystems. This overall alternating simulation function allo…
We propose a compositional approach for constructing abstractions of general Markov decision processes using approximate probabilistic relations. The abstraction framework is based on the notion of $δ$-lifted relations, using which one can quantify the distance in probability between the interconnected gMDPs and that of their abstractions. This new approximate relation unifies compositionality results in the literature by incorporating the dependencies between state transitions explicitly and by allowing abstract models to have either finite or infinite state spaces. Accordingly, one can lever…
In this paper, we focus on mitigating the computational complexity in abstraction-based controller synthesis for interconnected control systems. To do so, we provide a compositional framework for the construction of abstractions for interconnected systems and a bottom-up controller synthesis scheme. In particular, we propose a notion of approximate composition which makes it possible to compute an abstraction of the global interconnected system from the abstractions (possibly of different types) of its components. Finally, by leveraging our notion of approximate composition, we propose a botto…
In this paper, we propose a compositional approach to construct opacity-preserving finite abstractions (a.k.a symbolic models) for networks of discrete-time nonlinear control systems. Particularly, we introduce new notions of simulation functions that characterize the distance between control systems while preserving opacity properties across them. Instead of treating large-scale systems in a monolithic manner, we develop a compositional scheme to construct the interconnected finite abstractions together with the overall opacity-preserving simulation functions. For a network of incrementally i…
In this paper, we propose a compositional approach for the construction of finite abstractions (a.k.a. finite Markov decision processes (MDPs)) for networks of discrete-time stochastic control subsystems that are not necessarily stabilizable. The proposed approach leverages the interconnection topology and a notion of finite-step stochastic storage functions, that describes joint dissipativity-type properties of subsystems and their abstractions, and establishes a finite-step stochastic simulation function as a relation between the network and its abstraction. To this end, we first develop a n…
This paper provides a compositional scheme based on dissipativity approaches for constructing finite abstractions of continuous-time continuous-space stochastic control systems. The proposed framework enjoys the structure of the interconnection topology and employs a notion of stochastic storage functions, that describe joint dissipativity-type properties of subsystems and their abstractions. By utilizing those stochastic storage functions, one can establish a relation between continuous-time continuous-space stochastic systems and their finite counterparts while quantifying probabilistic dist…
Compositional Construction of Infinite Abstractions for Networks of Stochastic Control Systems
Technical University of Munich（慕尼黑工业大学）；Newcastle University（纽卡斯尔大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）；Ludwig Maximilian University of Munich（慕尼黑大学）
This paper formulates and studies the concepts of approximate (alternating) bisimulation relations characterizing equivalence relations between interconnected systems and their abstractions. These equivalence relations guarantee that the symbolic model conserves the original model's dynamics. We develop a compositional approach for abstraction-based controller synthesis by relying on the notions of approximate composition and incremental input-to-state stability. In particular, given a large-scale system consisting of interconnected components, we provide conditions under which the concept of …
In this paper, we provide a compositional approach for constructing finite abstractions (a.k.a. finite Markov decision processes (MDPs)) of interconnected discrete-time stochastic switched systems. The proposed framework is based on a notion of stochastic simulation functions, using which one can employ an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds on their output trajectories. To this end, we first provide probabilistic closeness guarantees between the interconnection of stochastic switched subsystems and that of their f…
In this paper, we develop a compositional scheme for the construction of continuous approximations for interconnections of infinitely many discrete-time switched systems. An approximation (also known as abstraction) is itself a continuous-space system, which can be used as a replacement of the original (also known as concrete) system in a controller design process. Having designed a controller for the abstract system, it is refined to a more detailed one for the concrete system. We use the notion of so-called simulation functions to quantify the mismatch between the original system and its app…
We construct compositional continuous approximations for an interconnection of infinitely many discrete-time switched systems. An approximation (known as abstraction) is itself a continuous-space system, which can be used as a replacement of the original (known as concrete) system in a controller design process. Having synthesized a controller for the abstract system, the controller is refined to a more detailed controller for the concrete system. To quantify the mismatch between the output trajectory of the approximation and of that the original system, we use the notion of so-called simulati…
In this work, we propose a compositional framework for the verification of approximate initial-state opacity for networks of discrete-time switched systems. The proposed approach is based on a notion of approximate initial-state opacity-preserving simulation functions (InitSOPSFs), which characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of approximate initial state opacity. We show that such InitSOPSFs can be obtained compositionally by assuming some small-gain type conditions and composing so-called local InitSOPSFs constructed for each su…
Algorithms for Synthesizing Priorities in Component-based Systems
Technische Universität München（慕尼黑工业大学）；Verimag Laboratory（Verimag实验室）；Institute of Information Science, Academia Sinica（中央研究院信息学研究所）；State Key Laboratory of Computer Science, ISCAS（中国科学院计算技术研究所）；fortiss GmbH（fortiss公司）
