Automated verification and synthesis of stochastic hybrid systems: a survey
From MaRDI portal
Publication:2097770
(in)finite abstractionsautomated verification and synthesiscompositionality techniquescontrol barrier certificatesMarkov decision processesmodel-order reductionsstochastic hybrid systemsstochastic similarity relations
Markov and semi-Markov decision processes (90C40) Research exposition (monographs, survey articles) pertaining to systems and control theory (93-02) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Discrete-time control/observation systems (93C55) Identification in stochastic control theory (93E12)
Abstract: Stochastic hybrid systems have received significant attentions as a relevant modelling framework describing many systems, from engineering to the life sciences: they enable the study of numerous applications, including transportation networks, biological systems and chemical reaction networks, smart energy and power grids, and beyond. Automated verification and policy synthesis for stochastic hybrid systems can be inherently challenging: this is due to the heterogeneity of their dynamics (presence of continuous and discrete components), the presence of uncertainty, and in some applications the large dimension of state and input sets. Over the past few years, a few hundred articles have investigated these models, and developed diverse and powerful approaches to mitigate difficulties encountered in the analysis and synthesis of such complex stochastic systems. In this survey, we overview the most recent results in the literature and discuss different approaches, including (in)finite abstractions, verification and synthesis for temporal logic specifications, stochastic similarity relations, (control) barrier certificates, compositional techniques, and a selection of results on continuous-time stochastic systems; we finally survey recently developed software tools that implement the discussed approaches. Throughout the manuscript we discuss a few open topics to be considered as potential future research directions: we hope that this survey will guide younger researchers through a comprehensive understanding of the various challenges, tools, and solutions in this enticing and rich scientific area.
Recommendations
- A compositional modelling and verification framework for stochastic hybrid systems
- Stochastic hybrid systems: a powerful framework for complex, large scale applications
- Quantitative automata model checking of autonomous stochastic hybrid systems
- Verification and control of probabilistic rectangular hybrid automata
- Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
Cites work
- p-Safe Analysis of Stochastic Hybrid Processes
- \( \mathcal{H}_2\) model reduction for diffusively coupled second-order networks by convex-optimization
- -complete decision procedures for satisfiability over the reals
- \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems
- A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
- A stochastic games framework for verification and control of discrete time stochastic hybrid systems
- ABC(SMC)\textsuperscript{2}: simultaneous inference and model checking of chemical reaction networks
- Abstraction-based synthesis for stochastic systems with omega-regular objectives
- Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes
- Adaptive control-based barrier Lyapunov functions for a class of stochastic nonlinear systems with full state constraints
- Approximate Abstractions of Stochastic Hybrid Systems
- Approximate model checking of stochastic hybrid systems
- Approximate Moment Dynamics for Chemically Reacting Systems
- Approximate Safety Verification and Control of Partially Observable Stochastic Hybrid Systems
- Approximately bisimilar symbolic models for randomly switched stochastic systems
- Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey
- Approximation of Large-Scale Dynamical Systems
- Approximations of Stochastic Hybrid Systems
- Approximations of Stochastic Hybrid Systems: A Compositional Approach
- Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
- Bisimilar symbolic models for stochastic control systems without state-space discretization
- Bisimulation through probabilistic testing
- Characterization and computation of infinite-horizon specifications over Markov processes
- Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
- 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 construction of infinite abstractions for networks of stochastic control systems
- Compositional probabilistic verification through multi-objective model checking
- Computer Aided Verification
- Computing probabilistic bisimilarity distances for probabilistic automata
- Confidence bounds for statistical model checking of probabilistic hybrid systems
- Control barrier functions for stochastic systems
- Control design for specifications on stochastic hybrid systems
- Converse Barrier Certificate Theorems
- Data-driven verification of stochastic linear systems with signal temporal logic constraints
- Deep reinforcement learning with temporal logics
- Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey
- Dynamic Bayesian networks for formal verification of structured stochastic processes
- Efficiency through uncertainty
- Efficient finite abstraction of mixed monotone systems
- Finite state approximation for verification of partially observable stochastic hybrid systems
- Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes
- Formal methods for discrete-time dynamical systems
- Formal Modeling and Analysis of Timed Systems
- Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
- Formal Synthesis of Stochastic Systems via Control Barrier Certificates
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Formal Verification and Synthesis for Discrete-Time Stochastic Systems
- Forward stochastic reachability analysis for uncontrolled linear systems using Fourier transforms
- Foundations of Modern Probability
- From Dissipativity Theory to Compositional Abstractions of Interconnected Stochastic Hybrid Systems
- From dissipativity theory to compositional construction of finite Markov decision processes
- From Dissipativity Theory to Compositional Synthesis of Large-Scale Stochastic Switched Systems
- From Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems
- Global stability for mixed monotone systems
- Higher-order approximations for verification of stochastic hybrid systems
- scientific article; zbMATH DE number 425394 (Why is no real title available?)
- scientific article; zbMATH DE number 1956626 (Why is no real title available?)
- scientific article; zbMATH DE number 4120082 (Why is no real title available?)
- scientific article; zbMATH DE number 2087806 (Why is no real title available?)
- scientific article; zbMATH DE number 794262 (Why is no real title available?)
- scientific article; zbMATH DE number 1444349 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 6936882 (Why is no real title available?)
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Introduction to the Scenario Approach
- Labelled Markov processes.
- Lagrangian approximations for stochastic reachability of a target tube
- Learning probabilistic termination proofs
- Markov chains and stochastic stability
- Measurability and safety verification for stochastic hybrid systems
- Metrics for labelled Markov processes
- Model checking of safety properties
- Moment-based analysis of stochastic hybrid systems with renewal transitions
- Motion Planning for Continuous-Time Stochastic Processes: A Dynamic Programming Approach
- Multi-layered abstraction-based controller synthesis for continuous-time systems
- Multilevel Monte Carlo method for statistical model checking of hybrid systems
- Networks of dissipative systems. Compositional certification of stability, performance, and safety
- Nonlinear Moment Matching-Based Model Order Reduction
- On Abstraction of Probabilistic Systems
- On the connections between PCTL and dynamic programming
- On the relationship between bisimulation and trace equivalence in an approximate probabilistic context
- pFaces
- Probabilistic CEGAR
- Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects
- Probabilistic invariance of mixed deterministic-stochastic dynamical systems
- Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
- Probabilistic Reach-Avoid Computation for Partially Degenerate Stochastic Processes
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems
- Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- Quantitative model-checking of controlled discrete-time Markov processes
- Reachability computation for switching diffusions, finite abstractions with certifiable and tuneable precision
- Reachability for partially observable discrete time stochastic hybrid systems
- Reduction of Second-Order Network Systems With Structure Preservation
- Regularization of Bellman equations for infinite-horizon probabilistic properties
- Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems
- Robust PCTL model checking
- Scalable semidefinite programming
- Scalable underapproximative verification of stochastic LTI systems using convexity and compactness
- SCOTS: a tool for the synthesis of symbolic controllers
- Semidefinite programming relaxations for semialgebraic problems
- Shrinking Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances
- Small gain theorems for large scale systems and construction of ISS Lyapunov functions
- Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems
- SReachTools
- Stability analysis for stochastic hybrid systems: a survey
- Stochastic hybrid systems for studying biochemical processes
- Stochastic hybrid systems. Theory and safety critical applications.
- Stochastic Model Predictive Control: An Overview and Perspectives for Future Research
- Stochastic models for chemically reacting systems using polynomial stochastic hybrid systems
- Stochastic reachability analysis of hybrid systems.
- Stochastic reachability of a target tube: theory and computation
- Stochastic stability and control
- Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions
- Symbolic controller synthesis for Büchi specifications on stochastic systems
- Symbolic models for stochastic switched systems: A discretization and a discretization-free approach
- Temporal logic model predictive control
- Temporal logic verification of stochastic systems using barrier certificates
- The linear programming approach to reach-avoid problems for Markov decision processes
- The MathSAT5 SMT solver
- The Scenario Approach to Robust Control Design
- The stochastic reach-avoid problem and set characterization for diffusions
- Towards scalable synthesis of stochastic control systems
- Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
- Validation of Stochastic Systems
- Verification and Control of Hybrid Systems
- Verification and refutation of probabilistic specifications via games
- Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Verification of Markov decision processes using learning algorithms
- Verification of partial-information probabilistic systems using counterexample-guided refinements
Cited in
(32)- Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
- Automatic verification of competitive stochastic systems
- Performance assessment and design of abstracted models for stochastic hybrid systems through a randomized approach
- Efficiency through uncertainty
- Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems
- Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes
- Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
- Poster Abstract: Controller Synthesis for Nonlinear Stochastic Games via Approximate Probabilistic Relations
- Symbolic control for stochastic systems via finite parity games
- Certified reinforcement learning with logic guidance
- Event-triggered polynomial input-to-state stability in mean square for pantograph stochastic systems
- Interval Markov Decision Processes with Continuous Action-Spaces
- SySCoRe: Synthesis via Stochastic Coupling Relations
- Poster Abstract: Data-Driven Correct-by-Design Control of Parametric Stochastic Systems✱
- Stochastic hybrid systems: a powerful framework for complex, large scale applications
- Time minimization and online synchronization for multi-agent systems under collaborative temporal logic tasks
- Formal controller synthesis for Markov jump linear systems with uncertain dynamics
- Verification of quantum systems using barrier certificates
- Data-driven abstraction-based control synthesis
- A probabilistic safety-aware strategy in stochastic multi-agent reach-avoid games
- A new framework for bounding reachability probabilities of continuous-time stochastic systems
- Certified model order reduction from data
- Scalable control synthesis for stochastic systems via structural imdp abstractions
- Memory-dependent abstractions of stochastic systems through the Lens of transfer operators
- SySCcoRe 2.0: toolset for formal control synthesis of continuous-state stochastic systems and temporal logic specifications
- Context-triggered games for reactive synthesis over stochastic systems via control barrier certificates
- Abstraction-based synthesis of stochastic hybrid systems
- Model predictive control of stochastic hybrid systems with signal temporal logic constraints
- Quantitative verification with neural networks
- Average reward reinforcement learning for omega-regular and mean-payoff objectives
- Kernel-based learning of safety barriers
- On the construction of barrier certificates: a dynamic programming perspective
Describes a project that uses
Uses Software
This page was built for publication: Automated verification and synthesis of stochastic hybrid systems: a survey
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2097770)
