Reelay: Online Temporal Logic Monitoring Framework

TL;DR

Reelay is a versatile online temporal logic monitoring framework that unifies multiple logics and semantics, enabling efficient runtime verification for cyber-physical systems across diverse deployment scenarios.

Contribution

It introduces a unified computational model for various temporal logics, supporting both discrete and dense semantics with efficient execution for high-frequency data streams.

Findings

Supports multiple temporal logics including LTL, MTL, and STL.

Efficient execution on high-frequency data streams.

Demonstrated practical applicability through case studies and performance tests.

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.