Multi-Property Temporal Logic Monitoring

TL;DR

This paper introduces an efficient online multi-property runtime verification framework that shares computation across properties, significantly improving scalability and performance in monitoring multiple temporal logic specifications.

Contribution

It extends compositional monitoring to a shared setting, enabling reuse of intermediate results and reducing redundant computation for multiple temporal properties.

Findings

Achieved 2x to 4.5x throughput improvements per property

Achieved 6x to 12x throughput improvements in multi-property scenarios

Demonstrated scalability to large sets of specifications in resource-constrained systems

Abstract

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.