一句话：证明带嵌套零测试的 VASS 可达性具有 Ackermann 上界，并统一判定半线性、可分性等相关问题
向量加法系统（VASS，又称 Petri 网）是并发系统的常用模型。论文研究带嵌套零测试的 VASS 的可达性问题：判断目标格局是否可从初始格局到达。作者给出该问题的 Ackermann 上界（固定维数下为原始递归），显著扩展了已知可判定性与复杂度结果。其证明提供一种统一方法，不仅能处理可达性，还能以相同复杂度判定半线性（semilinearity）和可分性（separability）等若干相关问题。特别地，对其中一些问题，即使不含零测试的普通 VASS，此前复杂度也未知。因此该工作为 VASS 扩展模型及相关判定问题建立了统一的复杂度上界。
Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS.
DOI 原文 ·
@inproceedings{paperbot8641,
title = {Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests},
author = {Roland Guttenberg and Wojciech Czerwiński and Sławomir Lasota},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00050}
}