论文标题
用电路监视超构物
Monitoring hyperproperties with circuits
论文作者
论文摘要
本文以Hyper-LTL精神呈现了Hennessy-Milner逻辑的安全片段的扩展。然后,它引入了一种新型的监视设置,该设置采用了类似电路的结构来结合常规显示器的判决。这项研究的主要贡献是监视器及其语义本身,以及从逻辑中的公式中进行的监视器合成程序,这些程序在有限的无限轨迹上产生了这种声音和违规的“电路样监测器”。
This paper presents an extension of the safety fragment of Hennessy-Milner Logic with recursion over sets of traces, in the spirit of Hyper-LTL. It then introduces a novel monitoring setup that employs circuit-like structures to combine verdicts from regular monitors. The main contribution of this study is the monitors and their semantics themselves, as well as a monitor-synthesis procedure from formulae in the logic that yields `circuit-like monitors' of this type that are sound and violation complete over a finite set of infinite traces.