Analysis of Path Planning Algorithms : a Formal Verification-based Approach

Abstract

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 verifi-cation 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 applica-tion of formal verification techniques in the context of multi-robot systems. Applying verification techniques, we aim to prove that the collective behavior of a group of robots sat-isfies 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.