Performance verification for robot missions in uncertain environments

This paper addresses the challenges involved in building a software tool for verifying the behavior of a multi-robot waypoint mission that includes uncertainly located obstacles and uncertain environment geometry as well as uncertainty in robot motion. An approach is presented to the problem of a-priori specification of uncertain environments for robot program verification. Two approaches to modeling probabilistic localization for verification are presented: a high-level approach and an approach that allows run-time localization code to be embedded in verification. Verification and experimental validation results are presented for several autonomous robot missions, demonstrating the accuracy of verification and the mission-specific benefit of localization