如今我们监控永不止步
计算机科学中的逻辑
2022-11-22 v1
摘要
并非所有性质都是可监控的。这是一个众所周知的事实，它意味着存在无法在运行时被完全验证的性质。然而，给定一个不可监控的性质，仍然可以合成一个监视器，但它可能会进入这样一种状态：对于该性质的满足（或违反）永远不会得出任何判定。出于这个原因，不可监控的性质通常被舍弃。在本文中，我们对可监控性以及不可监控的性质如何仍能被部分验证进行了深入分析。我们在语义层面给出了理论结果，而不聚焦于某种特定形式化方法。随后，我们展示了如何将我们的理论应用于实现线性时序逻辑（LTL）的部分运行时验证。
引用
@article{arxiv.2211.11544,
title = {Ain't No Stopping Us Monitoring Now},
author = {Luca Ciccone and Francesco Dagnino and Angelo Ferrando},
journal= {arXiv preprint arXiv:2211.11544},
year = {2022}
}