论文标题

用电路监视超构物

Monitoring hyperproperties with circuits

论文作者

Aceto, Luca, Achilleos, Antonios, Anastasiadi, Elli, Francalanza, Adrian

论文摘要

本文以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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源