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.

翻译：本文展示了如何利用模型检测为差动驱动轮式机器人创建多步规划，使其能够规避即时危险。通过使用专用的小型模型检测算法进行原位计算，我们实时生成规划，其方式反映了简单生物体的自我中心反应式响应。我们的方法基于链接临时控制系统，这些系统被触发以消除局部环境中干扰自主智能体偏离其偏好行为（或静止状态）的扰动。该方法涉及一种新颖的二维激光雷达数据离散化技术，该技术对即时环境中的有界随机波动具有敏感性。我们通过正向深度优先搜索的不变性检验实现多步规划操作化，并以死胡同场景作为首个测试案例。结果表明，模型检测能够规划出高效的局部避障轨迹，其性能优于仅能执行单步规划的反应式智能体。我们在无需任何预计算数据的情况下，以近实时方式实现了这一目标。尽管我们的方法存在局限性，但我们相信这一方向为开发自动驾驶背景下安全、可靠且透明的轨迹规划提供了有前景的途径。