Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions

Abstract

Temporal task planning guarantees a robot will succeed in its task as long as certain explicit and implicit assumptions about the robot’s operating environment, sensors, and capabilities hold. A robot executing a plan can silently fail to fulfill the task if the assumptions are violated at runtime. Monitoring assumption violations at runtime can flag silent failures and also provide mitigation and remediation opportunities. However, this requires means for describing assumptions combining temporal and quantitative data, automatic construction of correct monitors and ensuring a correct interplay between the planning execution and monitors. In this paper we propose combining temporal planning with stream runtime verification, which offers a high-level language to describe monitors together with guarantees on execution time and memory usage. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.

Publication
Proc. of the IEEE Int’l Conf. on Robotics and Automation, (ICRA'21), pp6824-6830, IEEE, 2021
César Sánchez
César Sánchez
Research Professor

My research focuses on formal methods, in paricular logic, automata and game theory. Temporal logics for Hyperproperties. Applications to Blockchain.