Proceedings:
Book One
Volume
Issue:
Proceedings of the International Conference on Automated Planning and Scheduling, 31
Track:
Special Track on Robotics
Downloads:
Abstract:
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 addresses two issues that PLPs raise: (1) Their formal semantics. (2) How to verify a script or a plan that schedule the use of components that have been documented by PLPs. We provide a formal semantics for PLPs by mapping 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. This PTA can be used to verify the system’s properties and answers queries about its behavior. Finally, we empirically evaluate an implemented system based on these ideas, demonstrating its scalability. The result is a pragmatic approach for verifying component-based robotic systems.
DOI:
10.1609/icaps.v31i1.16016
ICAPS
Proceedings of the International Conference on Automated Planning and Scheduling, 31