一句话：为单计数器整数 VASS、Parikh 自动机与标准 VASS 的广义可达性问题建立三条 AC1/NP 完全复杂度二分定理。
覆盖性通常比可达性复杂度低。本文将二者统一为：给定 Presburger 公式 F(t,x) 与目标向量 t，询问是否存在可达 x 满足 F(t,x)。研究带一个计数器、二进制更新的三类系统：整数 VASS、Parikh 自动机与标准非负 VASS，其可达性为 NP 完全，覆盖性为多项式时间。作者证明三条复杂度二分定理：对任意 F，问题要么 NP 完全，要么属于 AC1，且可判定落在哪一侧。对前两类，引入整数向量集密度度量，密度为正则 AC1 可解，否则 NP 完全；对标准 VASS，用一致准向上封闭性刻画边界。并将二进制 1-VASS 覆盖性上界从 NC2 改进到 AC1。
In many kinds of infinite-state systems, the cover-ability problem has significantly lower complexity than the reach-ability problem. In order to delineate the border of computational hardness between coverability and reachability, we propose to place these problems in a more general context, which makes it possible to prove complexity dichotomies.The more general setting arises as follows. We note that for coverability, we are given a vector t and are asked if there is a reachable vector x satisfying the relation "x equals t". For reachability, we want to satisfy the relation "x is at least t". In the more general setting, there is a Presburger formula F over t and x, and we are given t and are asked if there is a reachable x such that F is satisfied.We study this setting for systems with one counter and binary updates: (i) integer VASS, (ii) Parikh automata, and (iii) standard (non-negative) VASS. In each of these cases, reachability is NP-complete, but coverability is known to be in polynomial time. Our main results are three dichotomy theorems, one for each of the cases (i)–(iii). In each case, we show that for every F, the problem is either NP-complete or belongs to AC1, a circuit complexity class within polynomial time. We also show that it is decidable on which side of the dichotomy a given formula falls.For (i) and (ii), we introduce novel density measures for sets of integer vectors, and show an AC1 upper bound if the respective density of the set defined by F is positive; and NP-completeness otherwise. For (iii), the complexity border is characterized by a new notion of uniform quasi-upward closedness. In particular, we improve the best known upper bound for coverability in (binary encoded) 1-VASS from NC2 (as shown by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell in 2020) to AC1.
DOI 原文 ·
@inproceedings{paperbot8639,
title = {A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter},
author = {Yousef Shakiba and Henry Sinclair-Banks and Georg Zetzsche},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00051}
}