具有一个一元计数器的 2-VASS 的可覆盖性属于 NP
形式语言与自动机理论
2023-02-01 v1
摘要
Petri 网中的可覆盖性在反应系统安全性质验证中有应用。我们研究等价模型：带状态向量加法系统（VASS）中的可覆盖性。一个 k-VASS 可看作 k 个计数器和一个有限自动机，其转移标以 k 个整数。计数器值通过加上相应转移标签来更新。该系统中的一个配置由一个状态和 k 个计数值组成。重要的是，计数器绝不允许取负值。可覆盖性问题询问能否从初始配置遍历 k-VASS 到达一个计数值至少等于目标计数值的配置。在关于 k-VASS 的一系列成熟工作中，当整数更新以二进制编码时，2-VASS 中的可覆盖性已是 PSPACE 困难的。该下界限制了应用的实用性，因此关注限制条件很自然。本文开启了具有一个一元计数器的 2-VASS 的研究。此处，一个计数器接收二进制编码的更新，另一个接收一元编码的更新。我们的主要结果是：具有一个一元计数器的 2-VASS 的可覆盖性属于 NP。这改进了已有的 PSPACE 上界。我们的主要技术贡献在于只需考虑某种压缩线性形式的运行。
引用
@article{arxiv.2301.13543,
title = {Coverability in 2-VASS with One Unary Counter is in NP},
author = {Filip Mazowiecki and Henry Sinclair-Banks and Karol Węgrzycki},
journal= {arXiv preprint arXiv:2301.13543},
year = {2023}
}
备注
Preprint for FoSSaCS'23 containing 20 pages and 7 figures