有界验证的完美模型
摘要：非确定多头下推自动机可以接受语言的类在有界语言下是完美的。 完美性通过布尔操作来保持，同时空集问题是可判定的。 对于上下文无关语言来说，没有类可以包含它们而又是完美的，因为它们的不相交性问题是不可判定的。 在实践中，非完美语言类的验证问题通常通过检查系统行为的一个固定子集是否满足属性来进行欠估计。 一个常用的方法是使用有界语言来指定行为子集。 一个语言类C是在有界语言下完美的，如果对于每个有界语言而言，它在布尔操作下仍然保持完美，并且在有界语言下空集问题是可判定的。 我们考虑在有界语言下寻找完美的语言类。 我们展示了非确定多头下推自动机接受的语言类在有界语言下是完美的，并且给出了决策问题的复杂性特征。 我们还展示了有界语言是可以达到完美性的最大类。 我们证明了一些已知系统模型的计算，如递归多线程程序、递归计数机以及通信有限状态机可以被编码为非确定多头下推自动机，从而得到了在有界语言下的统一和最优的欠估计算法。
作者：Javier Esparza, Pierre Ganty, Rupak Majumdar
论文ID：1201.3194
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2012-08-28