长跑意味着向量加法系统中存在较大的分隔符
摘要：关于三维向量加法状态系统（3-VASS）的可达性问题存在一定的困难。尽管最近已经对向量加法状态系统（VASS）可达性问题的复杂性进行了研究, 确定了其为Ackermann-完全, 但我们对该问题仍然缺乏很多理解。一种可能的方法是证明检查可达性仅需要检查一些有限长度的运行路径，这种方法在许多VASS子类中取得成功。然而，这种方法有其局限性，通常很难设计出比该VASS子类中的有限可达性集合可能的大小更快的算法。鉴于此，我们需要寻找其他技术，以设计出更快速的算法。Leroux在2010年证明了两个配置之间的不可达性意味着源配置与目标配置之间存在一些半线性集合，它们是归纳不变量。我们有理由相信，只需要寻找有限大小的分隔符，就可以得到有效的VASS可达性算法。然而，本文证明了这种方法也会遇到阻碍：在一些自然条件的VASS中，一些配置之间只存在长路径，则意味着另一些配置之间存在较大的分隔符（在稍微修改的VASS中）。此外，我们还证明了一些已知的复杂VASS示例满足上述条件。因此，使用分隔符方法改进可达性问题（对于任何子类）的复杂性可能并不比使用短路径方法简单。
作者：Wojciech Czerwi''nski, Adam Jk{e}drych
论文ID：2105.00052
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-09-14