Real-Time Model Checking for Closed-Loop Robot Reactive Planning

• URL: http://arxiv.org/abs/2508.19186v1
• Date: Tue, 26 Aug 2025 16:49:30 GMT
• Title: Real-Time Model Checking for Closed-Loop Robot Reactive Planning
• Authors: Christopher Chandler, Bernd Porr, Giulia Lafratta, Alice Miller,
• Abstract summary: We present a new application of model checking which achieves real-time multi-step planning and obstacle avoidance on a real autonomous robot.<n>We have developed a small, purpose-built model checking algorithm which generates plans in situ based on "core" knowledge and attention as found in biological agents.<n>Our approach is based on chaining temporary control systems which are spawned to counteract disturbances in the local environment.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present a new application of model checking which achieves real-time multi-step planning and obstacle avoidance on a real autonomous robot. We have developed a small, purpose-built model checking algorithm which generates plans in situ based on "core" knowledge and attention as found in biological agents. This is achieved in real-time using no pre-computed data on a low-powered device. Our approach is based on chaining temporary control systems which are spawned to counteract disturbances in the local environment that disrupt an autonomous agent from its preferred action (or resting state). A novel discretization of 2D LiDAR data sensitive to bounded variations in the local environment is used. Multi-step planning using model checking by forward depth-first search is applied to cul-de-sac and playground scenarios. Both empirical results and informal proofs of two fundamental properties of our approach demonstrate that model checking can be used to create efficient multi-step plans for local obstacle avoidance, improving on the performance of a reactive agent which can only plan one step. Our approach is an instructional case study for the development of safe, reliable and explainable planning in the context of autonomous vehicles.

Related papers

• Action Flow Matching for Continual Robot Learning [57.698553219660376]
  Continual learning in robotics seeks systems that can constantly adapt to changing environments and tasks.<n>We introduce a generative framework leveraging flow matching for online robot dynamics model alignment.<n>We find that by transforming the actions themselves rather than exploring with a misaligned model, the robot collects informative data more efficiently.
  arXiv  Detail & Related papers  (2025-04-25T16:26:15Z)
• Centaur: Robust End-to-End Autonomous Driving with Test-Time Training [84.78837437133234]
  We propose Centaur, which updates a planner's behavior via test-time training without relying on hand-engineered rules or cost functions.<n>We develop a novel uncertainty measure, called Cluster Entropy, which is simple, interpretable, and compatible with state-of-the-art planning algorithms.
  arXiv  Detail & Related papers  (2025-03-14T17:59:41Z)
• EMPERROR: A Flexible Generative Perception Error Model for Probing Self-Driving Planners [27.813716878034374]
  We present EMPERROR, a novel transformer-based generative perception error model.<n>We show that it imitates modern detectors more faithfully than previous work.<n>It is able to produce realistic inputs that increase the planner's collision rate by up to 85%.
  arXiv  Detail & Related papers  (2024-11-12T11:24:18Z)
• Real-Time Anomaly Detection and Reactive Planning with Large Language Models [18.57162998677491]
  Foundation models, e.g., large language models (LLMs), trained on internet-scale data possess zero-shot capabilities. We present a two-stage reasoning framework that incorporates the judgement regarding potential anomalies into a safe control framework. This enables our monitor to improve the trustworthiness of dynamic robotic systems, such as quadrotors or autonomous vehicles.
  arXiv  Detail & Related papers  (2024-07-11T17:59:22Z)
• Planning with Adaptive World Models for Autonomous Driving [50.4439896514353]
  We present nuPlan, a real-world motion planning benchmark that captures multi-agent interactions.<n>We learn to model such unique behaviors with BehaviorNet, a graph convolutional neural network (GCNN)<n>We also present AdaptiveDriver, a model-predictive control (MPC) based planner that unrolls different world models conditioned on BehaviorNet's predictions.
  arXiv  Detail & Related papers  (2024-06-15T18:53:45Z)
• Model Checking for Closed-Loop Robot Reactive Planning [0.0]
  We show how model checking can be used to create multistep 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.
  arXiv  Detail & Related papers  (2023-11-16T11:02:29Z)
• AI planning in the imagination: High-level planning on learned abstract search spaces [68.75684174531962]
  We propose a new method, called PiZero, that gives an agent the ability to plan in an abstract search space that the agent learns during training. We evaluate our method on multiple domains, including the traveling salesman problem, Sokoban, 2048, the facility location problem, and Pacman.
  arXiv  Detail & Related papers  (2023-08-16T22:47:16Z)
• Active Uncertainty Reduction for Safe and Efficient Interaction Planning: A Shielding-Aware Dual Control Approach [9.07774184840379]
  We present a novel algorithmic approach to enable active uncertainty reduction for interactive motion planning based on the implicit dual control paradigm. Our approach relies on sampling-based approximation of dynamic programming, leading to a model predictive control problem that can be readily solved by real-time gradient-based optimization methods.
  arXiv  Detail & Related papers  (2023-02-01T01:34:48Z)
• SABER: Data-Driven Motion Planner for Autonomously Navigating Heterogeneous Robots [112.2491765424719]
  We present an end-to-end online motion planning framework that uses a data-driven approach to navigate a heterogeneous robot team towards a global goal. We use model predictive control (SMPC) to calculate control inputs that satisfy robot dynamics, and consider uncertainty during obstacle avoidance with chance constraints. recurrent neural networks are used to provide a quick estimate of future state uncertainty considered in the SMPC finite-time horizon solution. A Deep Q-learning agent is employed to serve as a high-level path planner, providing the SMPC with target positions that move the robots towards a desired global goal.
  arXiv  Detail & Related papers  (2021-08-03T02:56:21Z)
• Discovering Avoidable Planner Failures of Autonomous Vehicles using Counterfactual Analysis in Behaviorally Diverse Simulation [16.86782673205523]
  We introduce a planner testing framework that leverages recent progress in simulating behaviorally diverse traffic participants. We show that our method can indeed find a wide range of critical planner failures.
  arXiv  Detail & Related papers  (2020-11-24T09:44:23Z)
• Risk-Averse MPC via Visual-Inertial Input and Recurrent Networks for Online Collision Avoidance [95.86944752753564]
  We propose an online path planning architecture that extends the model predictive control (MPC) formulation to consider future location uncertainties. Our algorithm combines an object detection pipeline with a recurrent neural network (RNN) which infers the covariance of state estimates. The robustness of our methods is validated on complex quadruped robot dynamics and can be generally applied to most robotic platforms.
  arXiv  Detail & Related papers  (2020-07-28T07:34:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.