Document Type



Mobile Robots, Performance Guarantees, Formal Methods, Design Tools


Computer Engineering | Robotics


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.

Article Number


Publication Date



IFAC Intelligent Vehicle Symposium, Gold Coast Australia, June 26-28, 2013

This research was conducted at the Fordham University Robotics and Computer Vision Lab. For more information about graduate programs in Computer Science, see, and the Fordham University Graduate School of Arts and Sciences, see

Included in

Robotics Commons