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.

翻译：运行时验证能够检查单条执行轨迹上的时态逻辑规范，并提供了穷举形式化验证的可扩展替代方案。实践中，系统必须同时满足数十到数百个时态属性；然而，现有方法对每个属性进行独立监控，导致计算冗余和可扩展性受限。本文提出一种在线多属性监控框架，将过去时间线性时态逻辑和度量时态逻辑规范编译为子公式共享的有向无环图，每个属性对应一个输出。与独立构建监控器的先前方法不同，我们的方法将基于组合序贯网络的时态逻辑监控器构建扩展到共享环境，允许跨属性复用中间结果，同时保持其个体结构。该方法的核心是基于竞技场分配的双缓冲布局的数据导向执行模型，将每个子公式的中间结果存储在紧凑、连续的内存中。这种设计有利于空间局部性，并能以最小开销实现增量更新。实验结果表明，与传统单属性监控相比，多属性配置下每个属性的吞吐量提升了2到4.5倍和6到12倍，从而可扩展到大型规范集，并适用于高性能和资源受限系统。