Adventures in Monitorability: From Branching to Linear Time and Back Again
Adventures in Monitorability: From Branching to Linear Time and Back Again
复制标题
DOI：
10.1145/3290365
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Lehtinen, Karoliina
中科院分区：
文献类型：
--
作者：
Aceto, Luca;Achilleos, Antonis;Lehtinen, Karoliina
本文建立了一种全面的理论，即具有递归的轩尼诗 - 米尔纳逻辑的运行时可监测性，这是模态P-alculus的非常表现力的变体。它通过线性时间语义研究了该逻辑的可监视性，然后将获得的结果与先前在文献中呈现的分支时间设置的结果进行了比较。我们的工作建立了轩尼诗杂项逻辑的可监视片段的表达性层次结构，并在线性时间设置中递归，并准确地使用层次结构中每个片段的运行时显示器可以提供哪些保证。每个片段都显示为完整，从某种意义上说，它可以表达所有可以在相应保证下监视的属性。这项研究是使用一种原则性的监测方法进行的，该方法将逻辑语义和监视器的操作语义连接起来。所提出的框架支持可监视性能的正确监视器的自动组成合成。
This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal p-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.