论文标题
现在没有阻止我们监视
Ain't No Stopping Us Monitoring Now
论文作者
论文摘要
并非所有属性都是可监视的。这是一个众所周知的事实，这意味着存在在运行时无法完全验证的属性。但是，鉴于不可监护的属性，仍可以合成监视器，但最终可能会以一种对财产的满意度（分别，违反）的判决。因此，通常会丢弃不可监护的属性。在本文中，我们对可监视性进行了深入的分析，以及如何部分验证不可监督的属性。我们在语义层面上介绍了我们的理论结果，而不关注特定的形式主义。然后，我们展示了如何应用理论来实现线性时间逻辑（LTL）的部分运行时验证。
Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this paper, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of Linear Temporal Logic (LTL).
