Model checking is a formal method that decides whether a system satisfies a property formulated in temporal logic. While model checking is typically applied to hardware/software systems, it may be used to analyze any system that reaches only finitely many states; it is the number of these states that determines the time and memory requirements of the technique and thus limits its applicability.

This paper applies model checking to a system where a robot moves through an environment of obstacles. Whenever the robot senses an object blocking its path, it changes its direction; an algorithm inspired by the behavior of beetles is applied to learn an appropriate strategy for changing directions and avoiding collisions. The system is modeled in the language PROMELA of the model checker SPIN using embedded C code for the learning algorithm; it is then, for example, checked that after the initial learning phase, the robot stops colliding with obstacles.

Actually, the system is modeled twice: while an “explicit” model represents the positions of all objects in the environment, an “abstract” model only represents those objects that the robot may sense and collide with. When the robot moves, new objects may nondeterministically enter this model. The relationship between both models is formalized by a simulation relation. The authors prove that both models satisfy the same properties such that it suffices to check the smaller abstract model. The paper thus applies model checking to a novel problem and illustrates a general technique to extend the feasibility of model checking.