Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
From MaRDI portal
Publication:2103672
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.
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
Cites work
- scientific article; zbMATH DE number 5353850 (Why is no real title available?)
- scientific article; zbMATH DE number 18895 (Why is no real title available?)
- scientific article; zbMATH DE number 2107836 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- A game-based abstraction-refinement framework for Markov decision processes
- A stochastic games framework for verification and control of discrete time stochastic hybrid systems
- Approximate model checking of stochastic hybrid systems
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Compositional (In)Finite Abstractions for Large-Scale Interconnected Stochastic Systems
- Compositional Abstraction for Networks of Control Systems: A Dissipativity Approach
- Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach
- Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems
- Compositional abstraction-based synthesis for networks of stochastic switched systems
- Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations
- Compositional construction of infinite abstractions for networks of stochastic control systems
- Compositional strategy synthesis for stochastic games with multiple objectives
- Control design for specifications on stochastic hybrid systems
- Control synthesis for stochastic systems given automata specifications defined by stochastic sets
- Dynamic Bayesian networks as formal abstractions of structured stochastic processes
- Game-Theoretic Methods for Robustness, Security, and Resilience of Cyberphysical Control Systems: Games-in-Games Principle for Optimal Cross-Layer Resilient Control Systems
- Hierarchical control system design using approximate simulation
- Infinite horizon linear-quadratic Stackelberg games for discrete-time stochastic systems
- Minimax Control of Discrete-Time Stochastic Systems
- Model checking and strategy synthesis for stochastic games: from theory to practice (invited talk)
- Model checking of safety properties
- Monomial strategies for concurrent reachability games and other stochastic games
- Observer design for systems with multivariable monotone nonlinearities
- Observer-based control of systems with slope-restricted nonlinearities
- Perfect-information stochastic games with generalized mean-payoff objectives
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- Qualitative analysis of concurrent mean-payoff games
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems
- SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
- Sequential Stackelberg equilibria in two-person games
- Stochastic games with lexicographic reachability-safety objectives
- Stochastic optimal control. The discrete time case
- Stochastic tube MPC with state estimation
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems
Cited in
(12)- Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
- Duality-based nested controller synthesis from STL specifications for stochastic linear systems
- Formal controller synthesis for Markov jump linear systems with uncertain dynamics
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- Compositional controller synthesis for stochastic games
- Permissive controller synthesis for probabilistic systems
- Control synthesis for stochastic systems given automata specifications defined by stochastic sets
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems
- 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
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)
