Reelay: Online Temporal Logic Monitoring Framework

Abstract

We present Reelay, a unified online temporal logic monitoring framework designed for the rigorous analysis and runtime verification of cyber-physical systems. Reelay addresses the fragmentation of existing logical formalisms and tools by providing a single computational model and interface that supports a broad class of temporal logics. These include Linear Temporal Logic (LTL), Metric Temporal Logic (MTL), and Signal Temporal Logic (STL), along with their extensions for robustness semantics and first-order quantification over unbounded categorical data domains. At its core, Reelay translates temporal logic specifications into executable computation graphs operating as synchronous dataflow systems. This architecture ensures an efficient execution mechanism, making the framework ideal for high-frequency data streams regardless of behavior length. Uniquely, the framework supports both discrete and dense-time semantics, as well as delta-encoded temporal behaviors to minimize bandwidth usage in bandwidth-constrained environments. Reelay is implemented as a header-only C++ library with a high-level Python interface, facilitating integration across a wide range of deployment contexts, from resource-constrained embedded systems to autonomous robotic platforms. We demonstrate the practical applicability of the framework through a representative case study and performance experiments, illustrating how Reelay bridges the gap between expressive formal specifications and efficient runtime verification.