Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
From MaRDI portal
Publication:2103672
DOI10.1016/J.AUTOMATICA.2022.110696zbMATH Open1505.93257arXiv2104.11803OpenAlexW4308984347MaRDI QIDQ2103672FDOQ2103672
Authors: Bingzhuo Zhong, Abolfazl Lavaei, Majid Zamani, Marco Caccamo 
Publication date: 9 December 2022
Published in: Automatica (Search for Journal in Brave)
Abstract: 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 well ensured by refining controllers synthesized over abstract systems to the original games. Moreover, we propose an algorithmic procedure to construct such a relation for a particular class of nonlinear stochastic systems with slope restrictions on the nonlinearity. The proposed methods are demonstrated on a quadrotor example, and the results indicate that the desired lower bound for the probability of satisfaction is guaranteed.
Full work available at URL: https://arxiv.org/abs/2104.11803
Recommendations
- Compositional controller synthesis for stochastic games
- Control synthesis for stochastic systems given automata specifications defined by stochastic sets
- scientific article; zbMATH DE number 2163041
- Controllability of stochastic game-based control systems
- scientific article; zbMATH DE number 19131
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Synthesis of robust controllers: a game-theoretic approach
- scientific article; zbMATH DE number 3860975
- Stochastic system controller synthesis for reachability specifications encoded by random sets
- A stochastic games framework for verification and control of discrete time stochastic hybrid systems
stochastic gamespolicy refinementapproximate probabilistic relationautomata-based controller synthesisfinite abstraction
Formal languages and automata (68Q45) Stochastic games, stochastic differential games (91A15) Synthesis problems (93B50) Discrete-time control/observation systems (93C55) Stochastic systems in control theory (general) (93E03)
Cites Work
- SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
- \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems
- Title not available (Why is that?)
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- Stochastic optimal control. The discrete time case
- Title not available (Why is that?)
- Observer-based control of systems with slope-restricted nonlinearities
- Minimax Control of Discrete-Time Stochastic Systems
- Stochastic tube MPC with state estimation
- Model checking of safety properties
- Title not available (Why is that?)
- Approximate model checking of stochastic hybrid systems
- Hierarchical control system design using approximate simulation
- Observer design for systems with multivariable monotone nonlinearities
- A stochastic games framework for verification and control of discrete time stochastic hybrid systems
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Sequential Stackelberg equilibria in two-person games
- Control design for specifications on stochastic hybrid systems
- Control synthesis for stochastic systems given automata specifications defined by stochastic sets
- Infinite horizon linear-quadratic Stackelberg games for discrete-time stochastic systems
- Game-Theoretic Methods for Robustness, Security, and Resilience of Cyberphysical Control Systems: Games-in-Games Principle for Optimal Cross-Layer Resilient Control Systems
- Dynamic Bayesian networks as formal abstractions of structured stochastic processes
- Automated verification and synthesis of stochastic hybrid systems: a survey
- A game-based abstraction-refinement framework for Markov decision processes
- Monomial strategies for concurrent reachability games and other stochastic games
- Qualitative analysis of concurrent mean-payoff games
- Perfect-information stochastic games with generalized mean-payoff objectives
- Compositional (In)Finite Abstractions for Large-Scale Interconnected Stochastic Systems
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- Compositional strategy synthesis for stochastic games with multiple objectives
- Model checking and strategy synthesis for stochastic games: from theory to practice (invited talk)
- Title not available (Why is that?)
- Stochastic games with lexicographic reachability-safety objectives
- Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations
- Compositional abstraction-based synthesis for networks of stochastic switched systems
- Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach
- Compositional construction of infinite abstractions for networks of stochastic control systems
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Compositional Abstraction for Networks of Control Systems: A Dissipativity Approach
- Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems
- Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems
Cited In (12)
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Duality-based nested controller synthesis from STL specifications for stochastic linear systems
- Permissive controller synthesis for probabilistic systems
- Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
- Control synthesis for stochastic systems given automata specifications defined by stochastic sets
- Compositional controller synthesis for stochastic games
- Poster Abstract: Controller Synthesis for Nonlinear Stochastic Games via Approximate Probabilistic Relations
- Compositional synthesis of control barrier certificates for networks of stochastic systems against \(\omega\)-regular specifications
- Formal controller synthesis for Markov jump linear systems with uncertain dynamics
Uses Software
This page was built for publication: Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2103672)
