Verifying Performance for Autonomous Robot Missions with Uncertainty

Establishing performance guarantees for robot missions is especially important for C-WMD applications. Software verification techniques, such as model checking (Clark 1999, Jhala & Majumdar 2009), can be applied to robotic applications but characteristics of this application area, including addition of a robot environment model and handling continuous spatial location well, exacerbate state explosion, a key weakness of these methods. We have proposed an approach to verifying robot missions that shifts the focus from state-based analysis onto the solution of a set of flow equations (Lyons et al. 2012). The key novelty introduced in this paper is a probabilistic spatial representation for flow equations. We show how this representation models the spatial situation for robot motion with environments or controllers that include discrete choice (constraints). A model such as we propose here is useful only if it can accurately predict robot motion. We conclude by presenting three validation results that show this approach has strong predictive power; that is, that the verifications it produces can be trusted