$ω$-正则语言的可监测性
摘要：运行时验证系统中，ω-regular语言作为规范形式在许多方法中发挥着重要作用。然而，由于它们的元素是无穷长的单词，当只有一个有限前缀的单词（模拟到目前为止观察到的系统行为）可用时，并不是每个ω-regular语言都可以在运行时合理监测。因此，ω-regular语言L的可监测性是一个属性，即对于任何有限单词u，观察到目前为止，可以添加另一个有限单词v，使得uv成为相对于L的有限证明；也就是说，对于任何无限单词w，我们有uvw属于L，或者对于任何无限单词w，我们有uvw不属于L。这个概念过去已被一些作者研究过，并且已知可监测语言的类比常用的安全语言类别要更具表达力。但是，到目前为止，对可监测语言的准确分类还缺失。受在许多运行时验证方法中使用线性时态逻辑（LTL）的启发，本文首先确定了当L由一个LTL公式给出时，可监测性问题的复杂性。此外，它还表明了这个结果实际上可以推广到一般的ω-regular语言，即无论它们是由LTL公式、非确定性Buechi自动机还是ω-regular表达式给出。
作者：Andreas Bauer
论文ID：1006.3638
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2010-06-21