Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions

DOI10.1109/TAC.2014.2351652MaRDI QIDQ2982915zbMATH OpenOpenAlexFDO

Authors Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros

Publication date 16 May 2017

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1302.3868

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Synthesis problems (93B50) Discrete event control/observation systems (93C65) Stochastic systems in control theory (general) (93E03)

Abstract: Symbolic approaches to the control design over complex systems employ the construction of finite-state models that are related to the original control systems, then use techniques from finite-state synthesis to compute controllers satisfying specifications given in a temporal logic, and finally translate the synthesized schemes back as controllers for the concrete complex systems. Such approaches have been successfully developed and implemented for the synthesis of controllers over non-probabilistic control systems. In this paper, we extend the technique to probabilistic control systems modeled by controlled stochastic differential equations. We show that for every stochastic control system satisfying a probabilistic variant of incremental input-to-state stability, and for every given precision $varepsilon>0$, a finite-state transition system can be constructed, which is $varepsilon$-approximately bisimilar (in the sense of moments) to the original stochastic control system. Moreover, we provide results relating stochastic control systems to their corresponding finite-state transition systems in terms of probabilistic bisimulation relations known in the literature. We demonstrate the effectiveness of the construction by synthesizing controllers for stochastic control systems over rich specifications expressed in linear temporal logic. The discussed technique enables a new, automated, correct-by-construction controller synthesis approach for stochastic control systems, which are common mathematical models employed in many safety critical systems subject to structured uncertainty and are thus relevant for cyber-physical applications.

Cited in

(31)

• Symbolic models for stochastic switched systems: A discretization and a discretization-free approach
• Towards scalable synthesis of stochastic control systems
• Optimal multirate sampling in symbolic models for incrementally stable switched systems
• On distributed symbolic control of interconnected systems under persistency specifications
• Verification of approximate opacity for switched systems: a compositional approach
• Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations
• Symbolic models for infinite networks of control systems: a compositional approach
• Robust approximate symbolic models for a class of continuous-time uncertain nonlinear systems via a control interface
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Approximately bisimilar symbolic model for switched systems with unstable subsystems
• Similarity quantification for linear stochastic systems: a coupling compensator approach
• Compositional abstraction-based synthesis for networks of stochastic switched systems
• Probabilistic reachability and control synthesis for stochastic switched systems using the tamed Euler method
• Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach
• Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems
• Compositional construction of infinite abstractions for networks of stochastic control systems
• Compositional synthesis of finite abstractions for networks of systems: a small-gain approach
• Symbolic models for retarded jump-diffusion systems
• Approximately bisimilar symbolic models for randomly switched stochastic systems
• Abstraction-based control synthesis using partial information
• Verification of general Markov decision processes by approximate similarity relations and policy refinement
• Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
• Estimating infinitesimal generators of stochastic systems with formal error bounds
• Abstractions of networks of stochastic hybrid systems under randomly switched topologies: a compositional approach
• Data-driven verification and synthesis of stochastic systems via barrier certificates
• Inverse optimal incremental control of nonlinear jump-diffusion systems
• Incremental finite-step input-to-state stability for network of discrete-time switched systems
• Context-triggered games for reactive synthesis over stochastic systems via control barrier certificates
• Abstraction-based synthesis of stochastic hybrid systems
• Moment exponential input-to-state stability of non-linear switched stochastic systems with Lévy noise
• Compositional abstraction synthesis for interconnected switched systems with incrementally non-passive modes

This page was built for publication: Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2982915)