Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies

ABSTRACT. In the last decade, thanks to the ability of analyzing probabilistic models given specifications in temporal logics, Probabilistic Model Checking (PMC) has become a widely used methodology in several application domains, e.g., communication protocols, planning and scheduling, and robotics. Moreover, the availability of effective PMC tools enables automated analysis in such complex real-world scenarios.

In this paper we evaluate PMC tools to investigate safety of robots whose control policies are learned by reinforcement, i.e., considering feedback signals received upon acting in unknown environments. Introduced in previous contributions of ours, a new challenging application domain for PMC tools is represented by their usage as back-engines of an automated methodology aimed to verify and repair control policies. We present an evaluation of the current state-of-the-art PMC tools and assess their potential on various case studies, including both real and simulated robots accomplishing navigation, manipulation and reaching tasks.