论文标题
无限单词的帕里克自动机
Parikh Automata over Infinite Words
论文作者
论文摘要
Parikh Automata通过可以在半连接组中测试会员资格的计数器扩展有限自动机，但仅在运行结束时，从而保留了许多有限自动机的理想算法属性。在这里，我们研究了经典框架的扩展到无限的输入：我们介绍了无限单词和研究表达性，闭合特性以及验证问题的复杂性的无限性，Büchi和Co-BüchiParikhAutomata。 我们表明，在确定性和非确定性情况下，几乎所有类别的自动机都具有成对的无与伦比的表现力。结果与$ω$等级设置中众所周知的层次结构形成鲜明对比。此外，对于具有可及性或Büchi接受的Parikh Automata，空虚是可决定的，但由于安全性和co-Büchi的接受度不可决定。最重要的是，我们显示了模型检查的可定义性，并具有确定性帕里克自动机给出的规格，并获得了安全性或co-büchi的接受性，但对所有其他类型的自动机都不可证明。最后，解决所有类型的求解游戏都是不可决定的。
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the nondeterministic case; a result that sharply contrasts with the well-known hierarchy in the $ω$-regular setting. Furthermore, emptiness is shown decidable for Parikh automata with reachability or Büchi acceptance, but undecidable for safety and co-Büchi acceptance. Most importantly, we show decidability of model checking with specifications given by deterministic Parikh automata with safety or co-Büchi acceptance, but also undecidability for all other types of automata. Finally, solving games is undecidable for all types.
