paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes

固定维数 VASS 可达性问题的下界
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 论文研究固定维数 VASS 可达性问题的复杂度下界，属于自动机与形式化验证的理论基础，与画像核心的 PL→AI 静态分析、Agentic 程序、浮点程序分析、贝叶斯程序分析及其与 LLM 的交叉均无直接关联；仅与形式化验证有很弱的理论关联。引用 15 inbox
Wojciech Czerwinski, Lukasz Orlikowski
逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：为固定维数 VASS 的可达性问题给出四个改进的复杂度下界，覆盖 4 到 8 维的不同变体。

本文研究固定维数下带状态向量加法系统（VASS）可达性问题的复杂度。作者给出四个新的下界，均优于此前已知结果：一元 flat 4-VASS 为 NP-hard，一元 5-VASS 为 PSpace-hard，二进制 6-VASS 为 ExpSpace-hard，一元 8-VASS 为 Tower-hard。这些结果揭示了随着维数和编码方式变化，VASS 可达性的难度如何迅速上升，尤其是一元 8 维已达到 Tower 级下界。论文通过复杂度下界证明推进了固定维数 VASS 可达性的精确复杂度认识，并为相关验证问题的算法设计提供了理论边界。

问题
固定维数 VASS 的可达性问题复杂度尚未被完全刻画，尤其缺乏足够强的下界。
方法
该理论研究通过复杂度下界证明，针对 flat、一元与二进制编码以及不同维数的 VASS 变体建立新的难度结果。
评估
以理论复杂度证明作为评估，给出四个改进下界，覆盖一元 flat 4-VASS、一元 5-VASS、二进制 6-VASS 和一元 8-VASS。
原文摘要（Abstract）

We study the complexity of the reachability problem for Vector Addition Systems with States (VASSes) in fixed dimensions. We provide four lower bounds improving the currently known state-of-the-art: 1) NP-hardness for unary flat 4-VASSes (VASSes in dimension 4), 2) PSpace-hardness for unary 5-VASSes, 3) ExpSpace-hardness for binary 6-VASSes and 4) Tower-hardness for unary 8-VASSes.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{abs-2203-04243,
  title = {Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes},
  author = {Wojciech Czerwinski and Lukasz Orlikowski},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533357}
}