LoomRV

Monitoring many properties, efficiently

A system may need to check dozens of requirements against the same execution trace: whether an event occurred within a timing window, or whether a condition has held throughout a period. Independent monitors repeat input processing and evaluation of common subformulas. Their execution and memory layout also matter, even when there is no work to share.

LoomRV addresses both costs. It extends compositional sequential-network monitoring to multiple past-time LTL and MTL properties, in both discrete and dense time. The framework combines a shared computation graph with a data-oriented C++ runtime.

Compile shared work once

The frontend builds one directed acyclic graph across the registered properties. A content-addressable node database checks structural signatures and reuses identical subformulas, so each shared result is computed once per update.

Make execution and state contiguous

Sharing is only half of the design. The compiler packs the graph into an immutable array of fixed-size node records in topological order. Integer child indices replace pointers between heap-allocated objects, and operands precede their users. The engine evaluates the schedule in one forward pass, without recursion.

Metric temporal operators maintain variable-size sets of time intervals. Instead of giving every node its own growing container, LoomRV stores this interval state in a preallocated, double-buffered arena:

1. Read a node’s previous state and the current results of its already-evaluated children.
2. Append its updated interval state to the current buffer at a write cursor.
3. At the timestep boundary, swap the buffers and reset the cursor.

Buffer capacity is computed from the compiled formulas’ temporal bounds and allocated once at monitor creation. Metric interval state needs no dynamic allocation during evaluation. The layout favors spatial locality and separates previous state from the current update.

My contribution

I am the first author of Multi-Property Temporal Logic Monitoring, published in the FMCAD 2026 proceedings by TU Wien Academic Press, with Doğan Ulus. I developed LoomRV, building on my senior project, DO-VERIFY. The work integrates shared monitor construction, the C++ execution engine, and arena-based temporal state with a reproducible experimental artifact. The repository includes the Docker environment, trace generation, experiment scripts, and result tables.

Measure runtime efficiency and shared execution

The paper first evaluates each of 30 Timescales properties independently. None contains repeated subexpressions, so these comparisons demonstrate runtime improvements without subformula deduplication. It then evaluates all 30 properties together, comparing independent LoomRV monitors with the full shared monitor.

The results below distinguish these experiments. The multi-property timings include input processing and evaluation over one million steps; the full gain combines the execution engine, one-pass trace processing, and structural sharing. Controlled high- and low-sharing formula sets further explore sensitivity to structural overlap. Representative real-world property collections remain an important next step for measuring how much sharing occurs naturally.