# StocHy: automated verification and synthesis of stochastic processes

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

## Key facts

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

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

- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [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)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (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)
- [Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems](https://mlsanity.com/paper/2210.05304/) (2022)
- [Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties](https://mlsanity.com/paper/2405.04015/) (2024)
- [Learning Stabilizing Policies in Stochastic Control Systems](https://mlsanity.com/paper/2205.11991/) (2022)
- [Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions](https://mlsanity.com/paper/2311.09786/) (2023)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)

## Abstract (arXiv)

StocHy is a software tool for the quantitative analysis of discrete-time stochastic hybrid systems (SHS). StocHy accepts a high-level description of stochastic models and constructs an equivalent SHS model. The tool allows to (i) simulate the SHS evolution over a given time horizon; and to automatically construct formal abstractions of the SHS. Abstractions are then employed for (ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy allows for modular modelling, and has separate simulation, verification and synthesis engines, which are implemented as independent libraries. This allows for libraries to be easily used and for extensions to be easily built. The tool is implemented in C++ and employs manipulations based on vector calculus, the use of sparse matrices, the symbolic construction of probabilistic kernels, and multi-threading. Experiments show StocHy's markedly improved performance when compared to existing abstraction-based approaches: in particular, StocHy beats state-of-the-art tools in terms of precision (abstraction error) and computational effort, and finally attains scalability to large-sized models (12 continuous dimensions). StocHy is available at www.gitlab.com/natchi92/StocHy.