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

TL;DR

This paper introduces a real-time model checking approach for autonomous robots that enables multi-step obstacle avoidance and planning on low-powered devices, inspired by biological agents.

Contribution

It presents a novel, purpose-built model checking algorithm that performs in situ multi-step planning for autonomous robots without pre-computed data.

Findings

Efficient multi-step plans improve obstacle avoidance performance.

Real-time planning achieved on low-powered hardware.

Model checking demonstrates safety and reliability in local planning.

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.