可监控性探秘：从分支时间到线性时间再返回

本文为带递归的 Hennessy-Milner 逻辑（模态 $\mu$-演算的一个极具表达力的变体）建立了运行时可监控性的综合理论。它研究了该逻辑在线性时间语义下的可监控性，并将所得结果与文献中先前给出的分支时间设定下的结果进行比较。我们的工作在线性时间设定下建立了带递归的 Hennessy-Milner 逻辑中可监控片段的表达能力层级，并精确识别了该层级中每个片段使用运行时监控器所能给出的保证类型。每个片段被证明是完备的，即它能表达在相应保证下所有可被监控的性质。该研究采用一种将逻辑语义与监控器操作语义相关联的原则性监控方法。所提出的框架支持从可监控性质自动、组合地合成正确监控器。