Verifying Plans and Scripts for Robotics Tasks Using Performance Level Profiles

Authors

  • Alexander Kovalchuk Ben-Gurion University
  • Shashank Shekhar Ben-Gurion University
  • Ronen I. Brafman Ben-Gurion University

DOI:

https://doi.org/10.1609/icaps.v31i1.16016

Keywords:

Planning and Scheduling

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.

Downloads

Published

2021-05-17

How to Cite

Kovalchuk, A., Shekhar, S., & Brafman, R. I. (2021). Verifying Plans and Scripts for Robotics Tasks Using Performance Level Profiles. Proceedings of the International Conference on Automated Planning and Scheduling, 31(1), 673-681. https://doi.org/10.1609/icaps.v31i1.16016