可扩展性的冒险：从分支到线性时间再回来
Adventures in Monitorability: From Branching to Linear Time and Back Again
摘要：
本文建立了一个全面的Hennessy-Milner逻辑与递归，一个非常有表现力的变种模态$μ$演算的运行时监控性理论。它调查的可监测性，逻辑与线性时间语义，然后比较所获得的结果与以前在文献中提出的分支时间设置。我们的工作建立了一个表达层次的Hennessy-Milner逻辑递归的可监控片段的线性时间设置，并确切地确定了什么样的保证，可以使用运行时监视器的层次结构中的每个片段。每个片段被证明是完整的，在这个意义上，它可以表达所有的属性，可以在相应的保证下进行监控。该研究是使用一个原则性的方法来监测连接的逻辑和操作语义的监视器的语义。建议的框架支持自动合成正确的监视器从可监视的属性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
