# Model Checking for Closed-Loop Robot Reactive Planning

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 32 references that are in the map.
- First posted on arXiv 16 Nov 2023.

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

- [Practical Verification of Decision-Making in Agent-Based Autonomous Systems](https://mlsanity.com/paper/1310.2431/) (2013)
- [Comparative Analysis of Control Barrier Functions and Artificial Potential Fields for Obstacle Avoidance](https://mlsanity.com/paper/2010.09819/) (2020)
- [Probabilistic Model Checking and Autonomy](https://mlsanity.com/paper/2111.10630/) (2021)
- [Towards Adaptive Planning of Assistive-care Robot Tasks](https://mlsanity.com/paper/2209.14041/) (2022)
- [Simulation and Model Checking for Close to Realtime Overtaking Planning](https://mlsanity.com/paper/2110.12577/) (2021)
- [Online Strategy Synthesis for Safe and Optimized Control of Steerable Needles](https://mlsanity.com/paper/2110.12590/) (2021)
- [Proceedings Third Workshop on Formal Methods for Autonomous Systems](https://mlsanity.com/paper/2110.11527/) (2021)
- [Generating Safe Autonomous Decision-Making in ROS](https://mlsanity.com/paper/2209.14042/) (2022)

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

- [Real-Time Model Checking for Closed-Loop Robot Reactive Planning](https://mlsanity.com/paper/2508.19186/) (2025)

## Abstract (arXiv)

In this paper, we show how model checking can be used to create multi-step plans for a differential drive wheeled robot so that it can avoid immediate danger. Using a small, purpose built model checking algorithm in situ we generate plans in real-time in a way that reflects the egocentric reactive response of simple biological agents. Our approach is based on chaining temporary control systems which are spawned to eliminate disturbances in the local environment that disrupt an autonomous agent from its preferred action (or resting state). The method involves a novel discretization of 2D LiDAR data which is sensitive to bounded stochastic variations in the immediate environment. We operationalise multi-step planning using invariant checking by forward depth-first search, using a cul-de-sac scenario as a first test case. Our results demonstrate that model checking can be used to plan efficient trajectories for local obstacle avoidance, improving on the performance of a reactive agent which can only plan one step. We achieve this in near real-time using no pre-computed data. While our method has limitations, we believe our approach shows promise as an avenue for the development of safe, reliable and transparent trajectory planning in the context of autonomous vehicles.