2026 / Research engineering
LoomRV: Multi-Property Temporal Logic Monitoring
A high-performance C++ runtime verification framework for evaluating many temporal logic properties together through shared subformula execution.
LoomRV is the artifact for the paper Multi-Property Temporal Logic Monitoring. It extends my senior project work on DO-VERIFY from single-property runtime verification toward simultaneous monitoring of many past-time LTL and MTL specifications.
The core idea is to compile related formulas into a shared directed acyclic graph, so repeated subformulas are computed once and reused across property outputs. The runtime uses a zero-allocation, double-buffered arena layout for monitor state, with a linearized execution schedule designed for cache locality and predictable updates.
What I Built
- A C++ monitoring runtime for past-time temporal logic specifications over trace streams.
- A shared subformula representation that preserves each property’s output while removing redundant work.
- Benchmark and artifact infrastructure with Docker, CMake, generated traces, result tables, and reproducible experiment scripts.
- Performance comparisons against the object-oriented
reelayimplementation and single-property monitoring baselines.
Why It Matters
Runtime verification is often used when exhaustive formal verification is too expensive, but real systems rarely have just one property to check. Monitoring dozens or hundreds of formulas independently wastes computation on repeated structure. LoomRV treats the property set as one compiled workload, which makes multi-property monitoring more practical for high-throughput and resource-constrained environments.