Formally verifying navigation safety for ground robots

Abstract

Robots' continuous physical behaviors are controlled by discrete instructions generated using complicated control algorithms. In such a robotic hybrid system, guaranteeing robot's navigation safety can be more challenging than those discrete controls alone or only the continuous robot motions. For a robotic system operating in the real world, navigation safety is critical in order to avoid potential harm for robots or their surrounding environment. We present safety guarantee and obstacle avoidance control algorithms for mobile ground robots modeled by hybrid programs. Using the verification tool KeYmaera, we formally verify that our algorithms satisfy passive or passive friendly safety properties in an environment consisting of stationary/dynamic obstacles. These algorithms allow us to check the navigation safety at the design stage of a robotic system.