Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Computer Engineering
Establishing Performance Guarantees For Behavior-Based Robot Missions Using An Smt Solver, Feng Tang, Damian M. Lyons, Ronald Arkin
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 …
Performance Verification For Behavior-Based Robot Missions, Damian M. Lyons, Ron Arkin, Shu Jiang, Tsungming Liu, Paramesh Nirmal
Performance Verification For Behavior-Based Robot Missions, Damian M. Lyons, Ron Arkin, Shu Jiang, Tsungming Liu, Paramesh Nirmal
Faculty Publications
Certain robot missions need to perform predictably in a physical environment that may have significant uncertainty. One approach is to leverage automatic software verification techniques to establish a performance guarantee. The addition of an environment model and uncertainty in both program and environment, however, means the state-space of a model-checking solution to the problem can be prohibitively large. An approach based on behavior-based controllers in a process-algebra framework that avoids state-space combinatorics is presented here. In this approach, verification of the robot program in the uncertain environment is reduced to a filtering problem for a Bayesian Network. Validation results are …