Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and learning. This paper focuses on the unified construction of sequential networks from MTL specifications over discrete and dense time behaviors to provide an efficient and scalable online monitoring framework. Our core technique, future temporal marking, utilizes interval-based symbolic representations of future discrete and dense timelines. Building upon this, we develop efficient update and output functions for sequential network nodes for timed temporal operations. Finally, we extensively test and compare our proposed technique with existing approaches and runtime verification tools. Results highlight the performance and scalability advantages of our monitoring approach and sequential networks.

翻译：度量时序逻辑（MTL）是一种流行的形式化方法，用于描述具有时序约束的时序模式，可应用于基于属性的测试、机器人学、优化和学习等领域，以规范信息物理系统的行为。本文聚焦于从离散与稠密时间行为上的MTL规约统一构建序列网络，以提供一个高效且可扩展的在线监测框架。我们的核心技术——未来时序标记——利用基于区间的符号表示方法来刻画未来离散与稠密时间线。在此基础上，我们为序列网络节点开发了高效的更新函数与输出函数，以处理带时序的时序运算。最后，我们通过大量测试，将所提技术与现有方法及运行时验证工具进行了比较。结果凸显了我们的监测方法及序列网络在性能与可扩展性方面的优势。