Integer Vector Addition Systems with States
本文研究了带状态的可达向量加法系统（ZVASS）的可达性、可覆盖性和包含性问题及其推广和限制。ZVASS包括有限状态控制器，该有限状态控制器具有在整数范围内的有限数量的计数器。虽然ZVASS中的可达性是NP完全的，但事实证明，尽管它们是自然的，从复杂性的角度来看，这个类在文献中很少受到关注。我们填补了这一空白，提供了一个深入的分析上述决策问题的计算复杂性。最有趣的是，事实证明，虽然将重置操作添加到普通VASS中分别导致可达性和可覆盖性的不可判定性和阿克曼硬度，但它们可以添加到ZVASS中，同时保留可覆盖性和可达性的NP完全性。
2014-07-28 cs.FL
Long Runs Imply Big Separators in Vector Addition Systems
尽管最近的进展解决了向量加法系统的可达性问题的复杂性与状态（VASS）作为阿克曼完全，我们仍然缺乏对这个问题的理解。一个突出的例子是三维VASS（3-VASS）的可达性问题：它只知道是PSpace-hard的，而不知道是初等的。一种可能的方法，这是成功的许多VASS子类是证明，检查可达性，它足以检查一些有限长度的运行。然而，这种方法有其局限性，它通常是很难设计一个算法大大快于可能的大小有限的可达集在该VASS子类。它激发了对其他技术的搜索，这些技术可能适合于设计快速算法。在2010年，Leroux证明了两个配置之间的不可达性意味着源和目标通过某个半线性集是可分性的，这是一个归纳不变量。可以有一个合理的希望，它足以寻找有界大小的分隔符，这将提供一个有效的算法VASS可达性。在本文中，我们表明，这种方法也遇到了一个障碍：在VASS满足一些相当自然的条件存在的一些配置之间只有长期运行意味着存在的一些其他配置之间只有大的分离器（并在一个稍微修改的VASS）。此外，我们证明了一些已知的例子涉及VASS满足上述条件。因此，使用分隔符方法来提高可达性问题的复杂性（对于任何子类）可能并不比使用短期方法简单。
2022-09-13 cs.FL
Geometry of Reachability sets of Vector Addition Systems
本文研究向量加法系统（VAS）可达集的几何性质，证明其可有限分解为具良好几何性质的互不相交近混合线性集且该分解可有效计算，由此推出判定VAS可达集半线性性的新算法及可达集补集含无限线性集的结论。
2023-07-23 cs.FL cs.LO
The reachability problem for vector addition systems with a stack is not elementary
通过适应迭代码构造Stockmeyer，我们证明了向量加法系统的可达性问题与堆栈不具有初等复杂性。作为一个推论，同样的下界也适用于树上的二元一阶逻辑的可满足性问题，其中无界数据只能标记叶节点。这两个问题是否可以解决仍然是一个悬而未决的问题。
2013-10-07 cs.FL cs.LO
Reachability in Vector Addition Systems is Ackermann-complete
向量加法系统和等价Petri网是一种成熟的并发模型。向量加法系统的核心算法问题是可达性问题，它询问是否存在从一个给定配置到另一个给定配置的运行。我们解决了它的复杂性是阿克曼完全的，从而关闭了45年的问题。特别是，我们证明了这个问题是$\mathcal{F}_k$ -困难的向量加法系统的状态在维度$6k$，其中$\mathcal{F}_k$是$k$ -th复杂性类的层次结构的快速增长的复杂性类。
2022-10-25 cs.FL cs.LO
Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free
状态向量加法系统是一种普遍存在的计算模型，在计算机科学中有着广泛的应用。向量加法系统的可达性问题是中心问题，因为许多其他问题都归结为这个问题。该问题是可判定的，最近证明了向量加法系统的维数是复杂性的一个重要参数。在大于2的固定维度中，复杂度是未知的（具有巨大的复杂度差距）。在二维中，Blondin等人在2015年证明了可达性问题是PSPACE完全的。我们考虑这个模型的扩展，称为2-TVASS，其中第一个计数器可以测试为零。该模型自然地扩展了单计数器自动机（OCA）的经典模型。我们证明了2-TVASS的可达性在多项式空间中仍然是可解的。正如Blondin等人的工作一样，我们的方法依赖于通过连接多项式多个循环而获得的小的可达性证书的存在。
2020-07-17 cs.FL cs.LO
Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants
LaBRI, University of Bordeaux, CNRS, Bordeaux INP（波尔多大学）；Institute of Informatics, University of Warsaw（华沙大学）
研究分支向量加法系统的可达性问题，核心方法是基于半线性归纳不变量，证明不可达配置存在不包含它的半线性归纳不变量，并据此推导出简单枚举算法解决该可达性问题。
2026-07-13 cs.FL cs.LO
Reachability in Bidirected Pushdown VASS
下推状态向量加法系统（PVASS）扩展了具有下推存储的向量加法系统模型。如果每个转换（压入/弹出符号或修改计数器）都有一个伴随的相反转换，使效果相反，则PVASS被称为\emph{bidirected}。双向性在许多模型中自然出现;它也可以被视为对可达性的过度近似。我们证明了\emph{bidirected} PVASS的可达性问题在Ackermann时间内是可判定的，并且对于任意固定维数是原始递归的。对于一维双向PVASS的特殊情况下，我们表明可达性是在$\mathsf{PSPACE}$，事实上，在多项式时间，如果堆栈是多项式有界的。我们的研究结果是相反的\emph{directed}设置，其中可达性的可判定性是一个长期存在的开放问题已经为一维PVASS，并有一个$\mathsf{PSPACE}$ -下界已经为一维PVASS有界堆栈。双向（无状态）情况下的可达性关系是$\mathbb{N}^d$上的同余。我们的上界利用饱和技术的同余。特别是，我们展示了新的基本时间结构的半线性表示的同余产生的多个向量对。在一维PVASS的情况下，我们采用了一个饱和的过程，在有界大小的计数器。我们补充我们的上限与$\mathsf{TOWER}$ -硬度结果为任意尺寸和$k$ - $\mathsf{EXPSPACE}$硬度尺寸$2k+6$使用Lazić和Totzke的技术来实现迭代求幂。
2022-04-25 cs.FL
Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete
状态向量加法系统（VASS）可达性问题的复杂性判定是计算机科学中一个长期存在的公开问题。长期以来，这个问题被认为是可判定的，直到今天，它还没有任何复杂性的上限。本文证明了二维的【形】VASS的可达性是PSPACE-完全的。这改善了以前已知的双指数时间界限由豪厄尔，Rosier，Huynh和严在1986年建立。可覆盖性和有界性问题也是PSPACE完备的。此外，对于二维的【形】VASS和整数VASS中的可达性问题，给出了一些复杂性结果。
2014-12-13 cs.CC cs.FL cs.LO
Reachability in Vector Addition System with States Parameterized by Geometric Dimension
本文从几何维度视角研究带状态向量加法系统（VASS）的可达性问题，通过扩展泵引理技术，证明几何1维和2维VASS的可达性问题均为PSPACE完全。
2024-12-19 cs.FL cs.LO
Reachability in VASS Extended with Integer Counters
University of Bordeaux（波尔多大学）；University of Warsaw（华沙大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
本文研究了带有整数计数器的VASS中可达性问题，证明了在特定条件下可达性的复杂性，并展示了Z计数器对降低所需N计数器数量的影响。
2026-08-25 cs.FL
Improving Reachability in Vector Addition Systems through Pumpability
Shanghai Jiao Tong University（上海交通大学）
本文研究了固定维度向量加法系统（VAS）的可达性问题，通过改进的泵性分析，得出了d维VAS可达性问题的F_{d-2}上界，优于传统VASS的F_d上界，并在低维VAS中取得新的上界结果。
2026-04-27 cs.FL cs.LO
3-VASS Reachability is in EXPSPACE
Shanghai Jiao Tong University（上海交通大学）；Shanghai Normal University（上海师范大学）
研究三维向量加法系统可达性问题的复杂度，通过分层可泵性分析，证明该问题属于指数空间，此前已知算法是非初等的，此研究给出新结论。
2026-07-17 cs.FL cs.LO
Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
针对带嵌套零检测的VASS可达性问题，本文得出Ackermann型上界，并提出统一方法以相同复杂度解决半线性性、可分离性等相关问题，填补了普通VASS部分问题的复杂度研究空白。
2025-05-19 cs.FL cs.LO
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
字符串上的有限状态自动机的扩展，如多头自动机或多计数器自动机，已成功地用于编码许多无限状态非正则验证问题。在本文中，我们考虑一个推广的自动机理论的无限状态验证从字符串标记串并行图。我们定义了一个模型的非确定性，2路，并发自动机工作串并行图和通信通过共享寄存器的节点上的图形。我们考虑以下验证问题：给定一个系列的串并行图描述的上下文无关的图转换系统（GTS），并在串并行图的并发自动机，是一些图所产生的GTS接受的自动机？一般的问题是不可判定的已经（单向）多头自动机字符串。我们表明，一个有界的版本，其中自动机使固定数量的反转沿图，并使用固定数量的共享寄存器是可判定的，即使有没有约束的GTS生成的串并行图的大小。我们的可判定性结果是基于建立上下文切换的数量是有界的，并对有界并发自动机的计算进行编码，以将空性问题减少到下推自动机的空性问题。
2015-09-24 cs.FL
Improved Algorithm for Reachability in $d$-VASS
本文提出了一种结合线性路径方案与一般分解算法的新算法，将固定维度VASS可达性问题的复杂度上界从$\mathsf{F}_{d + 4}$改进至$\mathsf{F}_{d}$。
2024-04-23 cs.FL cs.LO
Revisiting Underapproximate Reachability for Multipushdown Systems
具有多个递归线程的布尔程序可以被捕获为具有多个堆栈的下推自动机。这个模型是图灵完备的，因此，人们通常对分析仍然捕获有用行为的受限类感兴趣。在本文中，我们提出了一类新的下有界逼近的多下推系统，其中包括大多数现有的类。我们开发了一个有效的算法来解决下近似可达性问题，这是基于高效的不动点计算。我们实现它在我们的工具BHIM，并说明其适用性，通过生成一组相关的基准和检查其性能。作为额外的收获，BHIM解决了下推自动机中的二进制可达性问题。为了显示我们的方法的多功能性，我们然后扩展我们的算法的定时设置，并提供了第一个实现，可以处理定时多下推自动机与封闭的警卫。
2020-05-05 cs.FL
PVASS Reachability is Decidable
University of Warsaw（华沙大学）；TU Braunschweig（布伦瑞克工业大学）
本文证明了具有状态的推导向量加法系统（PVASS）可达性问题在一般情况下是可判定的，方法类似于VASS可达性的KLMST算法，但利用了更复杂的进程总结形式。
2026-02-18 cs.FL cs.LO
Reachability in Fixed-Dimensional Continuous VASS
University of Liverpool（利物浦大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；University of Warsaw（华沙大学）
研究固定维度连续向量加法系统（CVASS）的可达性和覆盖性问题，在有理数和整数转移向量下，证明维度1时问题属于AC^1，维度≥2时NP完全。
2026-06-29 cs.CC cs.FL cs.LO
Reasoning about Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spaces
针对随机VAS尤其CRN中稀有事件概率低、状态空间巨大的问题，提出ISR与SDP两种基于仿射向量空间的部分状态空间扩展启发式方法，以高效生成可能轨迹并计算可达概率下界。
2025-07-23 cs.FL
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
分支VASS（BVASS）通过允许在两个控制状态之间非确定性地分配计数器值的特殊分支转换来概括具有状态的向量加法系统。因此，BVASS的运行成为一棵树，可达性决定给定的配置是否是可达性树的根。本文证明了BVASS在一维上可达性的P-完全性，这是迄今为止已知的BVASS子类中可达性的第一个可判定性结果。此外，我们还证明了BVASS在一维上的可覆盖性和有界性也是P-完全的。
2016-05-06 cs.FL cs.LO
Reachability Problem for Weak Multi-Pushdown Automata
本文研究了多下推自动机的一个受限子类的可达性分析。我们假设自动机的控制状态是偏序的，并且自动机的所有转换都是相对于顺序向下的。我们证明了可达性问题的可判定性和向后可达集的可计算性。作为主要的贡献，我们确定相关的子类的可达性问题成为NP完全。这与无通信向量加法系统（无状态多下推自动机的特殊情况）的相同问题的复杂性相匹配。
2013-09-20 cs.FL cs.LO
The Complexity of Reachability in Affine Vector Addition Systems with States
该研究刻画了仿射VASS中整数可达性的复杂性，给出三分法：重置类NP完全，转移/复制类PSPACE完全，其余不可判定；标准可达性仅置换类可判定，并探讨了固定实例的复杂性任意性。
2021-07-19 cs.CC cs.FL cs.LO
New Lower Bounds for Reachability in Vector Addition Systems
研究向量加法系统及其带下推栈扩展的可达性问题的维度参数复杂度，提出新构造将VASS的F_k-难度下界降至维度2k+3，并首次为下推VASS建立维度k/2+4的F_k-难度下界，表明其复杂度可能高于VASS。
2023-11-13 cs.FL cs.LO
Reachability in Continuous Pushdown VASS
本文研究连续 PVASS 的可达性问题，证明其为 NEXPTIME 完全，并展示了该结果在二进制编码、固定维度、有界栈及一元编码等条件下的稳健性与困难性。
2023-10-31 cs.FL cs.PL
Reachability in 3-VASS is in Tower
本文研究固定维数 VASS 的可达性复杂度，证明 3 维 VASS 可达性属于 Tower，将此前 2019 年的 $\mathbf{F}_7$ 上界改进为塔式高度。
2023-08-21 cs.FL cs.LO
Improved Ackermannian lower bound for the Petri nets reachability problem
University of Warsaw（华沙大学）
Petri网，等价地表示为具有状态的向量加法系统，是具有广泛应用的已建立的并发模型。可达性问题，我们问从一个给定的初始配置是否存在一个序列的有效执行步骤达到一个给定的最终配置，是这个模型的核心算法问题。直到最近，问题的复杂性仍然是并发系统验证中最难的开放问题之一。Leroux和Schmitz在2015年才给出了第一个上界，然后在2019年由同一作者改进为非原始递归阿克曼上界。Lipton在1976年已经证明了指数空间下界，40多年来一直是唯一已知的，直到2019年Czerwi{\displaystyle {\frac}ski}，Lasota，Lazic，Leroux和Mazowiecki突破了非初等下界。最后，Czerwi{\displaystyle Czerwi}ski和Orlikowski在今年宣布了一个匹配的阿克曼下界，并由Leroux独立地建立了问题的复杂性。我们的主要贡献是对前一种结构的改进，使其在概念上更简单，更直接。在方法上，我们改进了具有固定维状态的向量加法系统（或者等价地，具有固定位置数的Petri网）的下界：虽然Czerwi{\displaystyle {\frac {frac}）和Orlikowski证明了$F_k$ -硬度（在Grzegorczyk层次中$k$第th层的硬度）在$3k+2$维中，我们的简化构造已经在PDMAT
2022-01-13 cs.CL cs.FL
Reachability in Symmetric VASS
University of Warsaw（华沙大学）
本文研究了对称VASS中的可达性问题，证明其在PSPACE内可解，并探讨了不同群结构对复杂性的影响。
2026-09-29 cs.CL cs.FL
Senescent Ground Tree Rewrite Systems
已知具有状态的基础树重写系统具有不可判定的控制状态可达性问题。从最近引入的范围有界的多栈下推系统的灵感，我们定义衰老地面树重写系统。这些是具有状态的基础树重写系统的限制，使得树的节点在已经见证了先验固定数量的控制状态改变之后不再被重写。以及推广范围有界的多栈下推系统，我们表明-通过减少和重置Petri网-这些系统有一个阿克曼完全控制状态可达性问题。然而，正规树集的可达性仍然是不可判定的。
2013-11-19 cs.FL cs.LO
Monus semantics in vector addition systems with states
研究了带状态向量加法系统（VASS）的 monus 过近似语义，允许递减零值计数器，证明全程使用该语义时可达性保持可判定，并全面刻画了可达性、零可达性和覆盖性问题的复杂度。
2023-09-12 cs.FL cs.LO
The Tractability Border of Reachability in Simple Vector Addition Systems with States
本文全面刻画了一元编码下 VASS 可达性的易处理性边界，证明了 3-SLPS 中可达性为 NP 困难，并提出了二进制配置下 2-SLPS 可达性的多项式时间算法。
2024-12-21 cs.FL cs.LO
Reachability in 3-VASS is Elementary
本文研究了带状态的3维向量加法系统（3-VASS）的可达性问题，通过引入用小半线性集逼近2-VASS可达集的新技术，证明了最短路径长度存在三指数上界，从而将该问题的复杂度上界改进为双指数空间，显著缩小了复杂度差距。
2025-04-28 cs.FL cs.LO
On the Reachability Problem for Two-Dimensional Branching VASS
本文研究了二维分支向量加法系统（BVASS）的可达性问题，证明了该问题在二维下是可判定的，并证明其可达集具有可计算的半线性表示。
2025-06-27 cs.FL cs.LO
Reachability in Geometrically $d$-Dimensional VASS
针对向量加法状态系统（VASS）的可达性问题，本文提出几何d维VASS的概念，并证明当d>2时其可达性仍属于F_d复杂度类，拓展了现有d维VASS的复杂度结果。
2025-03-05 cs.CC cs.FL cs.LO
Continuous Pushdown VASS in One Dimension are Easy
本文研究一维下推向量加法系统，通过将计数器更新连续化，证明其可达性、可覆盖性和有界性可在多项式时间内判定，并进一步给出带下界守卫扩展模型的 NP 与 coNP 复杂度结果。
2024-02-20 cs.FL cs.LO
Decision Questions for Probabilistic Automata on Small Alphabets
研究一元和二元概率有限自动机的空性与$\lambda$-可达性问题，根据歧义度和字母表大小刻画其复杂度，揭示了多项式与有限歧义下的NP困难性及EXPTIME可解性。
2023-12-20 cs.FL cs.LO
Model Checking Vector Addition Systems with one zero-test
我们设计了Karp-Miller算法的一个变体，以向前的方式计算覆盖的有限表示（即，可达集的向下闭包）的一个零测试的向量加法系统。该算法产生的决策程序，这些系统的几个问题，开放到现在，如地方有界性或LTL模型检查。处理零测试的证明技术基于两个新的覆盖概念：精炼覆盖和过滤覆盖。精化覆盖是可达集和经典覆盖的混合。它继承了可达集的性质：两个加细覆盖的相等性是不可判定的，即使对于通常的向量加法系统（没有零检验），但向量加法系统的加细覆盖是递归集。覆盖的第二个概念，称为过滤覆盖，是我们算法的核心工具。它继承了经典覆盖的性质，特别是，可以有效地计算这个集合的有限表示，即使对于具有一个零测试的向量加法系统。
2012-06-17 cs.DM cs.FL
The Reachability Problem for Petri Nets is Not Elementary
Petri网，也被称为向量加法系统，是一种建立已久的并发模型，广泛应用于硬件，软件和数据库系统以及化学，生物和商业过程的建模和分析。Petri网的核心算法问题是可达性：从给定的初始配置是否存在一系列有效的执行步骤，达到给定的最终配置。这个问题的复杂性自20世纪60年代以来一直没有得到解决，它是验证理论中最突出的开放问题之一。可判定性是由Mayr在他的开创性的STOC 1981工作中证明的，目前最好的已发表的上限是LICS 2019的Leroux和Schmitz的非原始递归阿克曼。我们建立了一个非初等的下界，即可达性问题需要一个时间和空间的指数塔。直到这项工作，最好的下界一直是指数空间，由于利普顿在1976年。新的下界是一个重大突破，原因有几个。首先，它表明可达性问题比可覆盖性问题困难得多（即，状态可达性）问题，这也是普遍存在的，但自20世纪70年代后期以来，已知对于指数空间是完备的。其次，它意味着大量的问题，从形式语言，逻辑，并发系统，过程演算和其他领域，这是已知的承认减少从Petri网的可达性问题，也不是基本的。第三，它使目前最好的下界的可达性问题的两个关键扩展的Petri网：分支和下推栈。
2019-04-11 cs.FL cs.LO
Bridging the Gap Between Plain VASS and Branching VASS
University of Bordeaux, CNRS, Bordeaux INP（波尔多大学）；University of Warsaw（华沙大学）
本文研究分支VASS的可达性问题，证明其可达集是VASS的截面，并利用新的良拟序和融合性质，得出5维BVAS可达集有效半线性的结论。
2026-09-15 cs.FL cs.LO
