# Correct-by-construction reach-avoid control of partially observable linear stochastic systems

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 81 references that are in the map.
- First posted on arXiv 3 Mar 2021.

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

- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [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)
- [FaSTrack: a Modular Framework for Fast and Guaranteed Safe Motion Planning](https://mlsanity.com/paper/1703.07373/) (2017)
- [Formal Synthesis of Stochastic Systems via Control Barrier Certificates](https://mlsanity.com/paper/1905.04585/) (2019)
- [Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey](https://mlsanity.com/paper/2101.07491/) (2021)
- [Control Barrier Functions for Stochastic Systems](https://mlsanity.com/paper/2003.03498/) (2020)
- [Unified Multi-Rate Control: from Low Level Actuation to High Level Planning](https://mlsanity.com/paper/2012.06558/) (2020)
- [Planning, Fast and Slow: A Framework for Adaptive Real-Time Safe Trajectory Planning](https://mlsanity.com/paper/1710.04731/) (2017)
- [Feedback Refinement Relations for the Synthesis of Symbolic Controllers](https://mlsanity.com/paper/1503.03715/) (2015)
- [Verification of general Markov decision processes by approximate similarity relations and policy refinement](https://mlsanity.com/paper/1605.09557/) (2016)
- [Control Theory Meets POMDPs: A Hybrid Systems Approach](https://mlsanity.com/paper/1905.08095/) (2019)
- [Stochastic Motion Planning under Partial Observability for Mobile Robots with Continuous Range Measurements](https://mlsanity.com/paper/2011.11836/) (2020)
- [Approximate Safety Verification and Control of Partially Observable Stochastic Hybrid Systems](https://mlsanity.com/paper/1410.8054/) (2014)
- [Temporal Logic Verification of Stochastic Systems Using Barrier Certificates](https://mlsanity.com/paper/1807.00064/) (2018)

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

- [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)
- [Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions](https://mlsanity.com/paper/2311.09786/) (2023)

## Abstract (arXiv)

We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at least some required probability, the system reaches a desired goal state in finite time while avoiding unsafe states. Due to stochasticity and nonconvexity, this problem does not admit exact algorithmic or closed-form solutions in general. Our key contribution is a correct-by-construction controller synthesis scheme based on a finite-state abstraction of a Gaussian belief over the unmeasured state, obtained using a Kalman filter. We formalize this abstraction as a Markov decision process (MDP). To be robust against numerical imprecision in approximating transition probabilities, we use MDPs with intervals of transition probabilities. By construction, any policy on the abstraction can be refined into a piecewise linear feedback controller for the LTI system. We prove that the closed-loop LTI system under this controller satisfies the reach-avoid problem with at least the required probability. The numerical experiments show that our method is able to solve reach-avoid problems for systems with up to 6D state spaces, and with control input constraints that cannot be handled by methods such as the rapidly-exploring random belief trees (RRBT).