Software Engineering Institute

Robots are increasingly used to perform a wide variety of tasks, especially those involving dangerous or inaccessible locations. As the complexity of such tasks grow, robots are being deployed in teams, with complex coordination schemes aimed at maximizing the chance of mission success. Such teams operate under inherently uncertain conditions—the robots themselves fail, and have to continuously adapt to changing environmental conditions. A key challenge facing robotic mission designers is therefore to construct a mission—i.e., specify number and type of robots, number and size of teams, coordination and planning mechanisms etc.—so as to maximize some overall utility, such as probability of mission success. In this paper, we advocate, formalize, and empirically justify an approach to compute quantitative utility of robotic missions using probabilistic model checking. We show how to express a robotic demining mission as a restricted type of discrete time Markov chain (called PA), and its utility as either a linear temporal logic formula or a reward. We prove a set of compositionality theorems that enable us to compute the utility a system composed of several PAs by combining the utilities of each PA in isolation. This ameliorates the statespace explosion problem, even when the system being verified is composed of a larger number of robots. We validate our approach empirically, using the probabilistic model checker prism. This paper first appears in the Proceedings of the 20th International SPIN Symposium of Model Checking (SPIN 2013).