# Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey

arXiv: https://arxiv.org/abs/2101.07491 · HTML: https://mlsanity.com/paper/2101.07491/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Jan 2021.

## Built on by (most cited first, 20 of 20)

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise](https://mlsanity.com/paper/2110.12662/) (2021)
- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Decision-Making Under Uncertainty: Beyond Probabilities](https://mlsanity.com/paper/2303.05848/) (2023)
- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Correct-by-construction reach-avoid control of partially observable linear stochastic systems](https://mlsanity.com/paper/2103.02398/) (2021)
- [Interval Markov Decision Processes with Continuous Action-Spaces](https://mlsanity.com/paper/2211.01231/) (2022)
- [A Survey on Event Prediction Methods from a Systems Perspective: Bringing Together Disparate Research Areas](https://mlsanity.com/paper/2302.04018/) (2023)
- [Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics](https://mlsanity.com/paper/2212.00679/) (2022)
- [Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)](https://mlsanity.com/paper/2506.16971/) (2025)
- [Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions](https://mlsanity.com/paper/2311.09786/) (2023)
- [Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives](https://mlsanity.com/paper/2505.15693/) (2025)
- [Control Synthesis in Partially Observable Environments for Complex Perception-Related Objectives](https://mlsanity.com/paper/2507.02942/) (2025)
- [Comparing Labeled Markov Chains: A Cantor-Kantorovich Approach](https://mlsanity.com/paper/2511.18103/) (2025)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [Interval POMDP Shielding for Imperfect-Perception Agents](https://mlsanity.com/paper/2604.20728/) (2026)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)
- [Sound Probabilistic Safety Bounds for Large Language Models](https://mlsanity.com/paper/2607.20286/) (2026)

## Abstract (arXiv)

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.