论文标题
预言变量用于超专业验证
Prophecy Variables for Hyperproperty Verification
论文作者
论文摘要
超级专业的时间逻辑（例如HyperLTL）使用痕量量化器来表达与多个系统运行相关的属性。实际上，此类规格的验证主要仅限于无量词交替的公式，在这种情况下，可以将验证降低为对系统自我组成的痕量属性。量化器交替，例如$ \forallπ。 \存在π'。 ϕ $，可以通过补充解决，也可以通过解释为$ \ forall $ - 玩家之间的两人游戏，他们会逐步构建trace $π$，而存在$ \的$ \ player，他们以$π$和$π$ and $π'$ calide的方式构建$π'$。基于游戏的方法非常便宜，但不完整，因为$ \存在$ \ - 玩家不知道$ \ forall $ - 玩家的未来动作。在本文中，我们确定可以通过添加（$ω$的）时间预言来完成基于游戏的方法。我们的证明是建设性的，为产生完整的预言提供了有效的算法。
Temporal logics for hyperproperties like HyperLTL use trace quantifiers to express properties that relate multiple system runs. In practice, the verification of such specifications is mostly limited to formulas without quantifier alternation, where verification can be reduced to checking a trace property over the self-composition of the system. Quantifier alternations like $\forall π. \exists π'. ϕ$, can either be solved by complementation or with an interpretation as a two-person game between a $\forall$-player, who incrementally constructs the trace $π$, and an $\exists$-player, who constructs $π'$ in such a way that $π$ and $π'$ together satisfy $ϕ$. The game-based approach is significantly cheaper but incomplete because the $\exists$-player does not know the future moves of the $\forall$-player. In this paper, we establish that the game-based approach can be made complete by adding ($ω$-regular) temporal prophecies. Our proof is constructive, yielding an effective algorithm for the generation of a complete set of prophecies.
