# Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 40 references that are in the map.
- First posted on arXiv 16 Nov 2023.

## Builds on (most cited first, 15 of 15)

- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [A Survey of Motion Planning and Control Techniques for Self-driving Urban Vehicles](https://mlsanity.com/paper/1604.07446/) (2016)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints](https://mlsanity.com/paper/1410.6445/) (2014)
- [Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey](https://mlsanity.com/paper/2101.07491/) (2021)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [On the exact feasibility of convex scenario programs with discarded constraints](https://mlsanity.com/paper/2003.13433/) (2020)
- [StocHy: automated verification and synthesis of stochastic processes](https://mlsanity.com/paper/1901.10287/) (2019)
- [Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise](https://mlsanity.com/paper/2110.12662/) (2021)
- [Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems](https://mlsanity.com/paper/1901.01576/) (2019)
- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems](https://mlsanity.com/paper/1410.8060/) (2014)
- [Correct-by-construction reach-avoid control of partially observable linear stochastic systems](https://mlsanity.com/paper/2103.02398/) (2021)
- [Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics](https://mlsanity.com/paper/2212.00679/) (2022)

## Abstract (arXiv)

Automated synthesis of correct-by-construction controllers for autonomous systems is crucial for their deployment in safety-critical scenarios. Such autonomous systems are naturally modeled as stochastic dynamical models. The general problem is to compute a controller that provably satisfies a given task, represented as a probabilistic temporal logic specification. However, factors such as stochastic uncertainty, imprecisely known parameters, and hybrid features make this problem challenging. We have developed an abstraction framework that can be used to solve this problem under various modeling assumptions. Our approach is based on a robust finite-state abstraction of the stochastic dynamical model in the form of a Markov decision process with intervals of probabilities (iMDP). We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model. In this short paper, we survey our recent research in this area and highlight two challenges (related to scalability and dealing with nonlinear dynamics) that we aim to address with our ongoing research.