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.

使用模型检验创建差分驱动轮式机器人的多步计划，以避免即时危险，并以近实时的方式改善局部障碍物避免的效果。