Robotics Commons^™

Establishing Performance Guarantees For Behavior-Based Robot Missions Using An Smt Solver, Feng Tang, Damian M. Lyons, Ronald Arkin

Faculty Publications

In prior work we developed an approach to formally representing behavior-based multi-robot programs, and the uncertain environments in which they operate, as process networks. We automatically extract a set of probabilistic equations governing program execution in that environment using a static analysis module called VIPARS, and solve these using a Dynamic Bayesian Network (DBN) to establish whether stated performance guarantees hold for the program in that environment. In this paper we address the challenge of expanding the range of performance guarantees that are possible by using an SMT-solver instead of a DBN. We translate flow functions, which are recursive probabilistic …