Reelay：在线 temporal logic 监控框架

我们提出Reelay，一个统一的在线 temporal logic 监控框架，旨在为网络-物理系统提供严谨的分析和运行时验证。Reelay通过提供单一的计算模型和接口来解决现有逻辑形式化和工具的碎片化问题，支持广泛的 temporal logic 类别，包括线性时序逻辑（LTL）、度量时序逻辑（MTL）和信号时序逻辑（STL），以及它们的鲁棒性语义和对无限范畴数据域的 first-order 量化。在核心层面，Reelay将 temporal logic 规范翻译为作为同步数据流系统的可执行计算图。这种体系结构确保了高效的执行机制，使该框架适用于各种行为长度的高频数据流。独特的是，该框架支持离散和稠密时间语义，以及delta编码的时序行为，以最小化受限带宽环境中的带宽使用。Reelay实现为一个仅头文件的 C++ 库，附带高级 Python 接口，便于在从资源受限的嵌入式系统到自主机器人平台的广泛部署情境中进行集成。我们通过一个代表性案例研究和性能实验，展示了该框架的实际适用性，说明了Reelay如何在表达性强的形式规范与高效运行时验证之间架起桥梁。