Symbolic models or abstractions are known to be powerful tools for the control design of cyber-physical systems (CPSs) with logic specifications. In this paper, we investigate a novel learning-based approach to the construction of symbolic models for nonlinear control systems. In particular, the symbolic model is constructed based on learning the un-modeled part of the dynamics from training data based on state-space exploration, and the concept of an alternating simulation relation that represents behavioral relationships with respect to the original control system. Moreover, we aim at achieving safe exploration, meaning that the trajectory of the system is guaranteed to be in a safe region for all times while collecting the training data. In addition, we provide some techniques to reduce the computational load, in terms of memory and computation time, of constructing the symbolic models and the safety controller synthesis, so as to make our approach practical. Finally, a numerical simulation illustrates the effectiveness of the proposed approach.
This paper studies the construction of dynamic symbolic abstractions for nonlinear control systems via dynamic quantization. Since computational complexity is a fundamental problem in the use of discrete abstractions, a dynamic quantizer with a time-varying quantization parameter is first applied to deal with this problem. Due to the dynamic quantizer, a dynamic approximation approach is proposed for the state and input sets. Based on the dynamic approximation, dynamic symbolic abstractions are constructed for nonlinear control systems, and an approximate bisimulation relation is guaranteed fo…
This paper studies symbolic abstractions for nonlinear control systems using logarithmic quantization. With a logarithmic quantizer, we approximate the state and input sets, and then construct a novel discrete abstraction for nonlinear control systems. A feedback refinement relation between the constructed discrete abstraction and the original system is established. Using the constructed discrete abstraction, the safety controller synthesis problem is studied. With the discrete abstraction and the abstract specification, the existence of a safety controller is investigated, and the algorithm i…
This paper studies the construction of symbolic abstractions for nonlinear control systems via feedback refinement relation. Both the delay-free and time-delay cases are addressed. For the delay-free case, to reduce the computational complexity, we propose a new approximation approach for the state and input sets based on a static quantizer, and then a novel symbolic model is constructed such that the original system and the symbolic model satisfy the feedback refinement relation. For the time-delay case, both static and dynamic quantizers are combined to approximate the state and input sets. …
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实验室）
Symbolic control techniques aim to satisfy complex logic specifications. A critical step in these techniques is the construction of a symbolic (discrete) abstraction, a finite-state system whose behaviour mimics that of a given continuous-state system. The methods used to compute symbolic abstractions, however, require knowledge of an accurate closed-form model. To generalize them to systems with unknown dynamics, we present a new data-driven approach that does not require closed-form dynamics, instead relying only the ability to evaluate successors of each state under given inputs. To provide…
In this work, we propose a data-driven approach for the construction of finite abstractions (a.k.a., symbolic models) for discrete-time deterministic control systems with unknown dynamics. We leverage notions of so-called alternating bisimulation functions (ABF), as a relation between each unknown system and its symbolic model, to quantify the mismatch between state behaviors of two systems. Accordingly, one can employ our proposed results to perform formal verification and synthesis over symbolic models and then carry the results back over unknown original systems. In our data-driven setting,…
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…
Discrete abstractions have become a standard approach to assist control synthesis under complex specifications. Most techniques for the construction of a discrete abstraction for a continuous-time system require time-space discretization of the concrete system, which constitutes property satisfaction for the continuous-time system non-trivial. In this work, we aim at relaxing this requirement by introducing a control interface. Firstly, we connect the continuous-time uncertain concrete system with its discrete deterministic state-space abstraction with a control interface. Then, a novel stabil…
In this manuscript, we investigate symbolic abstractions that capture the behavior of piecewise-affine systems under input constraints and bounded external noise. This is accomplished by considering local affine feedback controllers that are jointly designed with the symbolic model, which ensures that an alternating simulation relation between the system and the abstraction holds. The resulting symbolic system is called a state-feedback abstraction and we show that it can be deterministic even when the original piecewise-affine system is unstable and non-deterministic. One benefit of this appr…
Discrete abstractions have become a standard approach to assist control synthesis under complex specifications. Most techniques for the construction of discrete abstractions are based on sampling of both the state and time spaces, which may not be able to guarantee safety for continuous-time systems. In this work, we aim at addressing this problem by considering only state-space abstraction. Firstly, we connect the continuous-time concrete system with its discrete (state-space) abstraction with a control interface. Then, a novel stability notion called controlled globally asymptotic/practical …
Symbolic control is an abstraction-based controller synthesis approach that provides, algorithmically, certifiable-by-construction controllers for cyber-physical systems. Symbolic control approaches usually assume that full-state information is available which is not suitable for many real-world applications with partially-observable states or output information. This article introduces a framework for output-feedback symbolic control. We propose relations between original systems and their symbolic models based on outputs. They enable designing symbolic controllers and refining them to enforc…
We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almos…
In this paper, we provide for the first time an automated, correct-by-construction, controller synthesis scheme for a class of infinite dimensional stochastic systems, namely, retarded jump-diffusion systems. First, we construct finite abstractions approximately bisimilar to non-probabilistic retarded systems corresponding to the original systems having some stability property, namely, incremental input-to-state stability. Then, we provide a result on quantifying the distance between output trajectory of the obtained finite abstraction and that of the original retarded jump-diffusion system in…
In previous work, linear time-invariant event-triggered control (ETC) systems were abstracted to finite-state systems that capture the original systems' sampling behaviour. It was shown that these abstractions can be employed for scheduling of communication traffic in networks of ETC loops. In this paper, we extend this framework to the class of nonlinear homogeneous systems, however adopting a different approach in a number of steps. Finally, we discuss how the proposed methodology could be extended to general nonlinear systems.
A common technique to verify complex logic specifications for dynamical systems is the construction of symbolic abstractions: simpler, finite-state models whose behaviour mimics the one of the systems of interest. Typically, abstractions are constructed exploiting an accurate knowledge of the underlying model: in real-life applications, this may be a costly assumption. By sampling random $\ell$-step trajectories of an unknown system, we build an abstraction based on the notion of $\ell$-completeness. We newly define the notion of probabilistic behavioural inclusion, and provide probably approx…
Integrated Symbolic Design of Unstable Nonlinear Networked Control Systems
Istituto di Analisi dei Sistemi ed Informatica “A. Ruberti”, Consiglio Nazionale delle Ricerche（信息与系统分析研究所，意大利国家研究委员会）；Department of Information Engineering, Computer Science and Mathematics, Center of Excellence DEWS, University of L’Aquila（拉奎拉大学信息工程、计算机科学与数学系，DEWS卓越中心）
In this paper, we propose an incremental abstraction method for dynamically over-approximating nonlinear systems in a bounded domain by solving a sequence of linear programs, resulting in a sequence of affine upper and lower hyperplanes with expanding operating regions. Although the affine abstraction problem can be solved offline using a single linear program, existing approaches suffer from a computation space complexity that grows exponentially with the state dimension. Hence, the motivation for incremental abstraction is to reduce the space complexity for high-dimensional systems, but at t…
The essential step of abstraction-based control synthesis for nonlinear systems to satisfy a given specification is to obtain a finite-state abstraction of the original systems. The complexity of the abstraction is usually the dominating factor that determines the efficiency of the algorithm. For the control synthesis of discrete-time nonlinear stochastic systems modelled by nonlinear stochastic difference equations, recent literature has demonstrated the soundness of abstractions in preserving robust probabilistic satisfaction of ω-regular lineartime properties. However, unnecessary transitio…
This paper proposes an algorithmic method to heuristically solve the famous Travelling Salesman Problem (TSP) when the salesman's path evolves in continuous state space and discrete time but with otherwise arbitrary (nonlinear) dynamics. The presented method is based on the framework of Symbolic Control. In this way, our method returns a provably correct state-feedback controller for the underlying coverage specification, which is the TSP leaving out the requirement for optimality on the route. In addition, we utilize the Lin-Kernighan-Helsgaun TSP solver to heuristically optimize the cost for…
