标记游戏与历史确定性量化自动机
摘要：非确定有限自动机是历史确定性的，如果它的非确定性只能通过考虑已读单词的前缀来解决。由于其良好的组合特性，历史确定性自动机在解决游戏和综合问题中很有用。确定给定的非确定有限自动机是否是历史确定性的（HDness问题）通常是一个困难的任务，可能涉及指数级的过程，甚至是不可判定的，例如下推自动机的情况。令牌游戏为B"uchi和coB"uchi自动机的HDness问题提供了PTime解决方案，并且有推测认为2令牌游戏能够刻画所有$omega$-regular自动机的HDness问题。 我们将令牌游戏扩展到定量设置，并分析其在帮助决定定量自动机的HDness问题方面的潜力。特别地，我们展示了1令牌游戏能够刻画所有有限单词上的定量（和布尔）自动机的HDness，以及无穷单词上的折扣和（DSum）、Inf和Reachability自动机的HDness；而2令牌游戏能够刻画LimInf和LimSup自动机的HDness，以及无穷单词上的Sup自动机的HDness。利用这些刻画，我们在PTime中提供了对有限和无穷单词上的Safety、Reachability、Inf和Sup自动机的HDness问题的解决方案，在NP$cap$co-NP中提供了对有限和无穷单词上的DSum自动机的解决方案，在准多项式时间中提供了对LimSup自动机的解决方案，并且对于具有对数个权重的自动机，对LimInf自动机的解决方案是多项式的。
作者：Udi Boker and Karoliina Lehtinen
论文ID：2110.14308
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-08-22