双向推动下的可达性问题
摘要：带有状态的推入向量加法系统是在向量加法系统模型的基础上引入了推入栈的扩展。如果每个转换（推入/弹出符号或修改计数器）都有相应的相反转换来反转效果，则称为双向化。双向化在许多模型中自然产生；它也可以看作是可达性的一种过度近似。我们证明，对于双向化的带有状态的PVASS，可达性问题在阿克曼时间内是可判定的，并且对于任意固定维度，是原始递归的。对于一维双向化PVASS的特殊情况，我们证明可达性属于$PSPACE$，实际上，如果堆栈是多项式界限的话，可以在多项式时间内解决。我们的结果与有向设置相反，对于一维PVASS，其中可达性的可判定性已经是一个悬而未决的开放问题，并且对于有界堆栈的一维PVASS，已经存在$PSPACE$下界。 双向化（无状态）情况下的可达关系是$mathbb{N}^d$上的一种同余关系。我们的上界利用了关于同余的饱和技术。特别地，我们展示了通过有限向量对生成的同余的元素时间构造半线性表示的新颖的初等时间构造。对于一维PVASS的情况，我们使用了一个关于有界大小计数器的饱和过程。 我们通过使用Lazi和Totzke的迭代求幂实现技术，在任意维度上证明了我们的上界与一个$TOWER$-难问题的相关性，以及在维度$2k+6$上的$ k $-$mathsf{EXPSPACE}$难度。
作者：Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Sch"utze, Georg Zetzsche
论文ID：2204.11799
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-04-26