Model Checking for Closed-Loop Robot Reactive Planning

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.

在本文中，我们展示了如何利用模型检查为差速驱动轮式机器人创建多步规划，使其能够避开即时危险。通过在原地使用一种小型的、专门构建的模型检查算法，我们以一种反映简单生物个体以自我为中心的反应式响应的方式实时生成规划。我们的方法基于链接临时控制系统，这些系统被生成用于消除局部环境中干扰自主个体执行其首选动作（或静止状态）的干扰。该方法涉及一种对紧邻环境中有界随机变化敏感的二维激光雷达数据的新型离散化。我们通过正向深度优先搜索利用不变性检查实现多步规划的操作化，并将死胡同场景作为第一个测试案例。我们的结果表明，模型检查可用于为局部避障规划高效轨迹，改进了只能规划一步的反应式个体的性能。我们在不使用预计算数据的情况下近乎实时地实现了这一点。虽然我们的方法存在局限性，但我们相信我们的方法在自动驾驶车辆背景下作为开发安全、可靠和透明轨迹规划的一种途径是有前景的。