Online-Monitoring Autonomous Transport Robots with an R-valued Temporal Logic

In this paper, we introduce real-valued temporal logic (RVTL) for online monitoring of reactive and cyber-physical systems. Our approach is based on classical metric temporal logic (MTL) with a real-valued semantics, where the truth value of a formula with respect to a finite trace depends on the distance between the end of the trace and the bound of the temporal operators in the formula. The assumed time model is dense and pointwise, i.e., the basic propositions refer to events reported by the system at specific times. We show that our logic is applicable for collaborating cyber-physical systems by giving example formulae from a case study of autonomous transport robots in a factory. We sketch an algorithm for monitoring RVTL formulae at runtime, and report on experiences with this algorithm in an actual industrial deployment of the case study.