Abstraction-based Synthesis for Stochastic Systems with Omega-Regular Objectives
Maxence Dutreix, Jeongmin Huh, Samuel Coogan
备注：
A theoretical mistake has been identified in the first version of the manuscript (Fact 1, which states that minimizing policies are memoryless in the product BMDP) and has been corrected in the second version. Other content related to this mistake has been modified (e.g. removal of Algorithm 2 and 4)
This paper studies the synthesis of controllers for discrete-time, continuous state stochastic systems subject to omega-regular specifications using finite-state abstractions. We present a synthesis algorithm for minimizing or maximizing the probability that a discrete-time stochastic system with finite number of modes satisfies an omega-regular property. Our approach uses a finite-state abstraction of the underlying dynamics in the form of a Bounded-parameter Markov Decision Process (BMDP) arising from a finite partition of the system's domain. Such abstractions allow for a range of transition probabilities between states for each action. Our method analyzes the product between the abstraction and a Deterministic Rabin Automaton encoding the specification. Synthesis is decomposed into a qualitative problem, where the greatest permanent winning components of the product are created, and a quantitative problem, which requires maximizing the probability of reaching this component. We propose a metric for the quality of the controller with respect to the abstracted states and devise a domain partition refinement technique to reach a quality target. Next, we present a method for computing controllers for stochastic systems with a continuous input set. The system is assumed to be affine in input and disturbance, and we derive a technique for solving the qualitative and quantitative problems in the abstractions of such systems called Controlled Interval-valued Markov Chains. The greatest permanent component of such abstractions are found by partitioning the input space to generate a BMDP accounting for all possible qualitative transitions between states. Maximizing the probability of reaching this component is cast as an optimization problem. Quality of the synthesized controller and a refinement scheme are described for this framework.
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 introduce NNSynth, a new framework that uses machine learning techniques to guide the design of abstraction-based controllers with correctness guarantees. NNSynth utilizes neural networks (NNs) to guide the search over the space of controllers. The trained neural networks are "projected" and used for constructing a "local" abstraction of the system. An abstraction-based controller is then synthesized from such "local" abstractions. If a controller that satisfies the specifications is not found, then the best found controller is "lifted" to a neural network for additional trai…
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实验室）
We consider abstraction-based design of output-feedback controllers for non-linear dynamical systems against specifications over state-based predicates in linear-time temporal logic (LTL). In this context, our contribution is two-fold: (I) we generalize feedback-refinement relations for abstraction-based output-feedback control to systems with arbitrary predicate and observation maps, and (II) we introduce a new algorithm for the synthesis of abstract output-feedback controllers w.r.t. LTL specifications over unobservable state-based predicates. Our abstraction-based output-feedback controller…
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…
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 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…
This paper studies formal synthesis of controllers for continuous-space systems with unknown dynamics to satisfy requirements expressed as linear temporal logic formulas. Formal abstraction-based synthesis schemes rely on a precise mathematical model of the system to build a finite abstract model, which is then used to design a controller. The abstraction-based schemes are not applicable when the dynamics of the system are unknown. We propose a data-driven approach that computes the growth bound of the system using a finite number of trajectories. The growth bound together with the sampled tra…
This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of the original system and then synthesise a controller for the abstract system. For this approach, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers fo…
Air Force Research Laboratory（空军研究实验室）；University of Central Florida（中佛罗里达大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
Given a Markov decision process (MDP) and a linear-time ($ω$-regular or LTL) specification, the controller synthesis problem aims to compute the optimal policy that satisfies the specification. More recently, problems that reason over the asymptotic behavior of systems have been proposed through the lens of steady-state planning. This entails finding a control policy for an MDP such that the Markov chain induced by the solution policy satisfies a given set of constraints on its steady-state distribution. This paper studies a generalization of the controller synthesis problem for a linear-time …
Temporal logic has been widely used to express complex task specifications for cyber-physical systems (CPSs). One way to synthesize a controller for CPS under temporal logic constraints is to first abstract the CPS as a discrete transition system, and then apply formal methods. This approach, however, is computationally demanding and its scalability suffers due to the curse of dimensionality. In this paper, we propose a control barrier function (CBF) approach to abstraction-free control synthesis under a linear temporal logic (LTL) constraint. We first construct the deterministic Rabin automat…
We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented a…
We study the problem of synthesizing a controller to satisfy a complex task in the presence of sensor faults and attacks. We model the task using Gaussian distribution temporal logic (GDTL), and propose a solution approach that does not rely on computing any finite abstraction to model the system. We decompose the GDTL specification into a sequence of reach-avoid sub-tasks. We develop a class of fault-tolerant finite time convergence control barrier functions (CBFs) to guarantee that a dynamical system reaches a set within finite time almost surely in the presence of malicious attacks. We use …
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 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…
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…
We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofold: (I) We construct abstractions which model the impact of occasional high disturbance spikes on the system via so called disturbance edges. (II) We show that the application of resilient reactive syn…
This paper studies the controller synthesis problem for Linear Temporal Logic (LTL) specifications using (constrained) zonotope techniques. First, we implement (constrained) zonotope techniques to partition the state space and further to verify whether the LTL specification can be satisfied. Once the LTL specification can be satisfied, the next step is to design a controller to guarantee the satisfaction of the LTL specification for dynamic systems. Based on the verification of the LTL specification, an abstraction-based control design approach is proposed in this paper: a novel abstraction co…
Autonomous systems often have complex and possibly unknown dynamics due to, e.g., black-box components. This leads to unpredictable behaviors and makes control design with performance guarantees a major challenge. This paper presents a data-driven control synthesis framework for such systems subject to linear temporal logic on finite traces (LTLf) specifications. The framework combines a baseline (offline) controller with a novel online controller and refinement procedure that improves the baseline guarantees as new data is collected. The baseline controller is computed offline on an uncertain…
In this work, we propose an abstraction and refinement methodology for the controller synthesis of discrete-time stochastic systems to enforce complex logical properties expressed by deterministic finite automata (a.k.a. DFA). Our proposed scheme is based on a notion of so-called $(ε,δ)$-approximate probabilistic relations, allowing one to quantify the similarity between stochastic systems modeled by discrete-time stochastic games and their corresponding finite abstractions. Leveraging this type of relations, the lower bound for the probability of satisfying the desired specifications can be w…
We consider the policy synthesis problem for continuous-state controlled Markov processes evolving in discrete time, when the specification is given as a Büchi condition (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the Büchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the Büchi condition can be enforced with probability one. The second step is to find the maximal probability of reaching the already computed qualitative winning set. In contrast with finite-state models, we s…
We consider abstraction-based design of output-feedback controllers for dynamical systems with a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller design (ABCD) first constructs a finite-state abstraction of the underlying dynamical system, and second, uses reactive synthesis techniques to compute an abstract state-feedback controller on the abstraction. In this context, our contribution is two-fold: (I) we define a suitable relation between the original system and its abstraction which characterizes the …
We propose a hierarchical control framework for the synthesis of correct-by-construction controllers for nonlinear control-affine systems with respect to reach-avoid-stay specifications. We first create a low-dimensional continuous abstraction of the system and use Sum-of-Squares (SOS) programming to obtain a low-level controller ensuring a bounded error between the two models. We then create a discrete abstraction of the continuous abstraction and use formal methods to synthesize a controller satisfying the specifications shrunk by the obtained error bound. Combining both controllers finally …
We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertai…
