# FAUST2: Formal Abstractions of Uncountable-STate STochastic processes

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Mar 2014.

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

- [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)
- [Shielding Atari Games with Bounded Prescience](https://mlsanity.com/paper/2101.08153/) (2021)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/2209.10341/) (2022)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2201.00655/) (2021)
- [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)
- [SOCKS: A Stochastic Optimal Control and Reachability Toolbox Using Kernel Methods](https://mlsanity.com/paper/2203.06290/) (2022)
- [Learning Stabilizing Policies in Stochastic Control Systems](https://mlsanity.com/paper/2205.11991/) (2022)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)

## Abstract (arXiv)

FAUST2 is a software tool that generates formal abstractions of (possibly non-deterministic) discrete-time Markov processes (dtMP) defined over uncountable (continuous) state spaces. A dtMP model is specified in MATLAB and abstracted as a finite-state Markov chain or Markov decision processes. The abstraction procedure runs in MATLAB and employs parallel computations and fast manipulations based on vector calculus. The abstract model is formally put in relationship with the concrete dtMP via a user-defined maximum threshold on the approximation error introduced by the abstraction procedure. FAUST2 allows exporting the abstract model to well-known probabilistic model checkers, such as PRISM or MRMC. Alternatively, it can handle internally the computation of PCTL properties (e.g. safety or reach-avoid) over the abstract model, and refine the outcomes over the concrete dtMP via a quantified error that depends on the abstraction procedure and the given formula. The toolbox is available at http://sourceforge.net/projects/faust2/