从命题监控到一阶监控
计算机科学中的逻辑
2013-03-18 v1 形式语言与自动机理论
摘要
本文的主要目的是引入一阶时序逻辑 LTLFO，以及基于一种新型自动机（称为衍生自动机）的相应监控器构造。具体而言，我们证明了对 LTLFO 中的规约进行监控可归结为一个不可判定的判定问题。该结果的证明围绕着我们关于何为“恰当”监控器的特定观点展开。由于这些观点具有普适性，我们首先在标准 LTL 的背景下概述它们，然后再将其提升至一阶逻辑和 LTLFO 的背景。尽管由于上述结果，人们无法期望获得完备的 LTLFO 监控器，但我们证明了基于自动机的构造的可靠性，并给出了其实现的实验结果。这些结果似乎证实了我们的假设，即基于自动机的构造能够产生高效的运行时监控器，其规模不会随着迹长度的增加而增长（这在类似方法中常被观察到）。然而，我们也讨论了无论选择何种监控方法，其规模增长都不可避免的公式。
引用
@article{arxiv.1303.3645,
title = {From propositional to first-order monitoring},
author = {Andreas Bauer and Jan-Christoph Küster and Gil Vegliach},
journal= {arXiv preprint arXiv:1303.3645},
year = {2013}
}