Analysis of path planning algorithms : a formal verification-based approach

With the emergence of multi-robot systems in the field of robotics there is a need for new approaches for modeling and investigating the behavior of robotic systems. Formal verification is a well-known mathematical method which has been used for decades in order to expose potential design faults in industrial systems. In this paper we introduce the application of formal verification techniques in the context of multirobot systems. Applying verification techniques, we aim to prove that the collective behavior of a group of robots satisfies certain desired properties. We illustrate our approach using a simple path planning algorithm which conducts a set of robots from their initial positions to their destinations on a planar surface