超属性（Hyperproperties）的集中式监控系统与去中心化监控系统

《ACM Transactions on Computational Logic》：Centralized vs Decentralized Monitors for Hyperproperties

本文研究Hyper-recHML逻辑的运行时验证，提出集中式监控器语言和去中心化监控器语言，并设计合成算法生成正确监控器，其中去中心化监控器的正确性基于与集中式监控器的弱双模拟关系。

　　

摘要

本文重点研究了在Hyper-recHML中表达的超属性的运行时验证问题。Hyper-recHML是一种表达能力强且简单的逻辑语言，用于描述轨迹集合的属性。为此，我们设计了一种简单的监控器语言，这种监控器能够观察系统执行的轨迹集合，并针对给定的Hyper-recHML公式给出判断结果。首先，我们使用了一种全局监控器，它能够集中观察所有系统轨迹。由于集中式监控器并不适用于分布式环境，我们还提供了一种用于分布式监控器的语言，在这种语言中，每个轨迹都由一个专用的监控器负责监控；这些监控器通过相互通信来生成唯一的判断结果。对于集中式和分布式环境，我们都提供了一种合成算法，该算法能够根据给定的公式生成一个正确的监控器（即满足完备性和正确性要求的监控器）。证明分布式监控器合成算法正确性的关键步骤是证明：对于每个公式，生成的集中式监控器与其对应的分布式监控器在某种适当的弱双模拟（weak bisimulation）概念下是弱双相似的。