去中心化 LTL 监控

想要监控分布式或基于组件的系统的用户通常将它们视为单体系统，从外部看，这些系统表现出统一的行为，而不是由许多组件展示许多共同构成系统全局行为的局部行为。这种抽象级别通常是合理的，向可能希望根据 LTL 公式指定系统全局行为的用户隐藏了实现细节。然而，由此产生的问题是，在没有中央数据收集点、所有组件的局部行为都可观测的分布式系统中，如何实际监控这样的规范。在这种情况下，LTL 规范需要被分解为子公式，进而需要将其分布到组件本地连接的监控器中，每个监控器只能看到全局行为的不同部分。本文的主要贡献是一种用于分布和监控 LTL 公式的算法，使得规范的满足或违反可以仅由本地监控器检测。我们提出了一个实现，并表明我们的算法在检测规范的满足/违反时仅引入最小的延迟。此外，我们的实际结果表明，本地监控器引入的通信开销远低于需要发送到中央数据收集点的消息数量。