具有一个一元计数器的2-VASS中的可达性问题属于NP
摘要：Petri网中的覆盖性在验证反应式系统的安全性属性中找到了应用。我们研究了等价模型中的覆盖性：带有状态的向量加法系统（VASS）。 k-VASS可以看作是k个计数器和一个有限自动机，其转换标记为k个整数。通过将相应的转换标签添加到计数器的值来更新计数器的值。该系统中的配置由一个状态和k个计数器值组成。重要的是，计数器不允许取负值。覆盖性问题询问是否可以从初始配置遍历k-VASS到至少具有目标计数器值的配置。 在对k-VASS的已有工作线路中，当整数更新以二进制编码时，2-VASS的覆盖性已经是PSPACE-hard问题。这个下界限制了应用的实用性，因此专注于限制是很自然的。在本文中，我们初步研究了具有一个一元计数器的2-VASS。这里，一个计数器接收二进制编码的更新，另一个计数器接收一元编码的更新。我们的主要结果是，在具有一个一元计数器的2-VASS中，覆盖性问题是在NP中的。这改进了继承的PSPACE上界的最新技术贡献是只需要考虑某种压缩线性形式的运行。
作者：Filip Mazowiecki, Henry Sinclair-Banks, and Karol Wk{e}grzycki
论文ID：2301.13543
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-02-01