paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests

带星号的 Presburger 算术、图群的有理子集与嵌套零测试
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 2/10 · 该论文是纯逻辑与自动机复杂性理论研究,涉及 Presburger 算术、图群有理子集和嵌套零测试可达性,属于形式验证基础,但未涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户画像的核心交叉方向几乎没有直接关联。引用 11 inbox
Christoph Haase, Georg Zetzsche
crossref: 2026-09-12

AI 速览

一句话:证明带星号的存在性 Presburger 算术为 NEXP 完全,并统一三个判定问题及其固定参数复杂度。

本文研究带 Kleene 星号(可嵌套)的存在性 Presburger 算术的可满足性复杂度。该逻辑自然扩展了 Presburger 算术,并统一了图群中有理子集成员问题与带状态和嵌套零测试的整数向量加法系统可达性问题。作者证明带星号存在性 Presburger 算术可满足性为 NEXP 完全,且上述三个问题可在多项式时间互相归约。对于固定参数变体,即固定逻辑的星号高度、图群成员问题的图参数、以及整数向量加法系统中不同零测试的个数,三者均为 NP 完全。由此得到固定图群上有理子集成员问题的完整复杂度图景:图为团时为 NL 完全,为不相交团并时为 P 完全,为传递森林且非团并时为 NP 完全,否则不可判定。

问题
研究带(可嵌套)Kleene 星号的存在性 Presburger 算术可满足性,以及图群有理子集成员问题和带嵌套零测试的整数向量加法系统可达性的复杂度。
方法
通过证明三个问题多项式时间互相归约,并分析固定星号高度、固定图参数和固定零测试数目等参数化变体。
评估
建立 NEXP 完全与固定参数 NP 完全结果,并给出固定图群成员问题的完整复杂度分类(NL/P/NP 完全或不可判定)。
原文摘要(Abstract)

We study the computational complexity of existential Presburger arithmetic with (possibly nested occurrences of) a Kleene-star operator. In addition to being a natural extension of Presburger arithmetic, our investigation is motivated by two other decision problems. The first problem is the rational subset membership problem in graph groups. A graph group is an infinite group specified by a finite undirected graph. While a characterisation of graph groups with a decidable rational subset membership problem was given by Lohrey and Steinberg [J. Algebra, 320(2) (2008)], it has been an open problem (i) whether the decidable fragment has elementary complexity and (ii) what is the complexity for each fixed graph group. The second problem is the reachability problem for integer vector addition systems with states and nested zero tests. We prove that the satisfiability problem for existential Pres-burger arithmetic with stars is NEXP-complete and that all three problems are polynomially inter-reducible. Moreover, we consider for each problem a variant with a fixed parameter: We fix the star-height in the logic, a graph parameter for the membership problem, and the number of distinct zero-tests in the integer vector addition systems. We establish NP-completeness of all problems with fixed parameters. In particular, this enables us to obtain a complete description of the complexity landscape of the rational subset membership problem for fixed graph groups: If the graph is a clique, the problem is N L-complete. If the graph is a disjoint union of cliques, it is P-complete. If it is a transitive forest (and not a union of cliques), the problem is NP-complete. Otherwise, the problem is undecidable.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot5027,
  title = {Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests},
  author = {Christoph Haase and Georg Zetzsche},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785850}
}