# Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Jan 2019.

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

- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Certification of Iterative Predictions in Bayesian Neural Networks](https://mlsanity.com/paper/2105.10134/) (2021)
- [Verified Probabilistic Policies for Deep Reinforcement Learning](https://mlsanity.com/paper/2201.03698/) (2022)
- [Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2201.00655/) (2021)
- [Probabilistic Reach-Avoid for Bayesian Neural Networks](https://mlsanity.com/paper/2310.01951/) (2023)
- [Promises of Deep Kernel Learning for Control Synthesis](https://mlsanity.com/paper/2309.06569/) (2023)
- [Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics](https://mlsanity.com/paper/2212.00679/) (2022)
- [Verification of Unknown Dynamical Systems via Autoencoder Latent Space](https://mlsanity.com/paper/2512.13593/) (2025)
- [Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions](https://mlsanity.com/paper/2311.09786/) (2023)

## Abstract (arXiv)

This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both finite- and infinite-horizon specifications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables.