一句话：建立了带递归 Hennessy-Milner 逻辑的运行时可监控性理论，给出线性时间下可监控片段的表达力层级与监控保证。
论文研究带递归的 Hennessy-Milner 逻辑（HML）这一极具表达力的模态 μ-演算变体在运行时监控中的可监控性。作者以线性时间语义考察该逻辑，并通过连接逻辑语义与监控器操作语义的原则化框架，与既有分支时间结果进行比较。主要结果包括：在线性时间设置下建立可监控片段的表达力层级，精确刻画每一层级片段能够提供的运行时保证；证明每个片段在相应保证下都是完备的，即可表达所有可在该保证下被监控的性质；该框架还支持从可监控性质自动、组合式地合成正确监控器。
This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal µ-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.
@article{paperbot648,
title = {Adventures in monitorability: from branching to linear time and back again},
author = {Luca Aceto and Antonis Achilleos and Adrian Francalanza and Anna Ingólfsdóttir and Karoliina Lehtinen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290365}
}