רונן ברפמן

Performance-Level Profiles (PLPs) were introduced as a type of action representation language suitable for capturing the behavior of functional code for robotics. This paper considers two issues that PLPs raise: (1) Their formal semantics. (2) How to verify a script or plans that schedule the use of components that have been documented by PLPs. We discuss formal semantics for PLPs that maps them to probabilistic timed automata (PTAs). We also show how, given a script that refers to components specified using PLPs, we derive a PTA specification of the entire system. Using a model checker, we can now verify various properties of the system and answers queries about its behavior. Finally, we empirically evaluate an implemented system based on these ideas that use the UPPAAL-SMC model checker and demonstrate its scalability. The result is a pragmatic approach for verifying various properties of component-based robotic systems.