# Multi-Property Temporal Logic Monitoring

arXiv: https://arxiv.org/abs/2605.13668 · HTML: https://mlsanity.com/paper/2605.13668/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 May 2026.

## Built on by (most cited first, 1 of 1)

- [Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications](https://mlsanity.com/paper/2609.33461/) (2026)

## Abstract (arXiv)

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.