Dogan Ulus

Dogan Ulus

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.

Arınç Demir, Dogan Ulus

Runtime verification enables checking temporal logic specifications over individual execution traces and offers a scalable alternative to exhaustive formal verification. In practice, systems must satisfy dozens to hundreds of temporal properties simultaneously; however, existing approaches monitor each property in isolation, resulting in redundant computation and limited scalability. In this work, we present an online multi-property monitoring framework that compiles past-time LTL and MTL specifications into a shared directed acyclic graph of subformulas with one output per property. Unlike prior approaches that construct monitors independently, our method extends compositional sequential network-based temporal logic monitor construction to a shared setting, enabling reuse of intermediate results across properties while preserving their individual structure. Central to our approach is a data-oriented execution model based on an arena-allocated, double-buffered layout that stores intermediate results for each subformula in compact, contiguous memory. This design favors spatial locality and enables incremental updates with minimal overhead. Experimental results demonstrate per-property throughput improvements of 2x to 4.5x and 6x to 12x in multi-property configurations compared to conventional single-property monitoring, enabling scalability to large specification sets and deployment in high-performance and resource-constrained systems.

Dogan Ulus, Calin Belta

This paper presents an application of specification based runtime verification techniques to control mobile robots in a reactive manner. In our case study, we develop a layered control architecture where runtime monitors constructed from formal specifications are embedded into the navigation stack. We use temporal logic and regular expressions to describe safety requirements and mission specifications, respectively. An immediate benefit of our approach is that it leverages simple requirements and objectives of traditional control applications to more complex specifications in a non-intrusive and compositional way. Finally, we demonstrate a simulation of robots controlled by the proposed architecture and we discuss further extensions of our approach.

Dogan Ulus

We present Montre, a monitoring tool to search patterns specified by timed regular expressions over real-time behaviors. We use timed regular expressions as a compact, natural, and highly-expressive pattern specification language for monitoring applications involving quantitative timing constraints. Our tool essentially incorporates online and offline timed pattern matching algorithms so it is capable of finding all occurrences of a given pattern over both logged and streaming behaviors. Furthermore, Montre is designed to work with other tools via standard interfaces to perform more complex and versatile tasks for analyzing and reasoning about cyber-physical systems. As the first of its kind, we believe Montre will enable a new line of inquiries and techniques in these fields.