Runtime Monitoring of Time Window Temporal Logic

Abstract

Temporal logic is becoming increasingly popular for its application in the analysis and control of dynamic systems. Time window temporal logic (TWTL) is a rich expressive language for specifying time-bounded serial tasks in a compact manner that is common in many control applications, such as robotics. Typically, TWTL specifications are verified using an automata-based model checking algorithm. However, verification of important properties of a given system using model checking in design time does not guarantee that the system will behave as expected during the runtime operation which falls under the scope of runtime verification. In this letter, we present a rewriting-based algorithm for runtime monitoring of safety requirements expressed in TWTL. The feasibility and efficiency of our proposed approach is demonstrated using two case studies related to unmanned aerial vehicle (UAV) surveillance and industrial robotics for manufacturing.