价值系统中的范围限定可达性
摘要：多推栈系统是并发递归程序的标准模型，但它们具有不可判定的可达性问题。因此，已经提出了几种方法来对其运行集进行下估计，从而使在该下估计中的可达性问题变得可判定。其中一种能够覆盖相对较高比例运行的下估计是作用域有界性。在这样的运行中，对于每次对栈$i$的推入操作，相应的弹出操作必须在有界次访问栈$i$后进行。在本文中，我们将这种方法推广到了一个较大的无限状态系统类别中。 对此，我们考虑了价值系统的模型，它由有限状态控制和由有限无向图指定的无限状态存储机制组成。这个框架涵盖了推栈机、向量加法系统、整数向量加法系统以及它们的组合。对于这个框架，我们提出了作用域有界性的概念，当存储机制恰好是多推栈时，与经典概念相一致。我们证明了在这个概念下，每个存储机制的可达性问题都可以在PSPACE中决定。此外，我们描述了在所有存储机制的情况下，无论是作用域边界作为输入还是作为固定范围的情况下，该问题的完整复杂度情况。 最后，我们提供了一个几乎完整的描述，即如果存储机制的描述甚至包含在输入中，复杂度情况如何。
作者：Aneesh K. Shetty and S. Krishna and Georg Zetzsche
论文ID：2108.00963
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2021-08-03