Reachability in fixed dimension vector addition systems with states
可达性问题是基于状态向量加法系统（VASS）的形式化验证的核心决策问题，VASS等价于Petri网，是研究和应用最多的并发模型之一。VASS的可达性也与来自计算机科学的许多领域的过多问题相互简化。尽管最近的进展，可达性问题的复杂性仍然悬而未决，它是密切相关的最短的VASS运行，见证可达性的长度。我们考虑固定维数的VASS，得到三个主要结果。对于前两个，我们假设输入中的整数以一元形式给出，并且给定VASS的控制图是平坦的（即，没有嵌套循环）。我们得到了一个家庭的VASS在3维的最短可达见证运行是指数，我们表明，可达性问题是NP-困难的7维。这些结果从负面解决了Blondin等人在LICS 2015年和Englert等人在LICS 2016年的工作中提出的问题，并贡献了区分3维平面VASS和2维VASS的第一个构造。我们的第三个结果，通过一个新的家庭的产品的整数分数，表明4维VASS可以有双指数长的最短可达见证运行。以前已知的最小尺寸是14。
2020-05-10 cs.FL
Reachability analysis of first-order definable pushdown systems
我们研究下推系统的控制状态，堆栈字母表，和过渡关系，而不是有限的，是一阶定义在一个固定的可数无限结构。我们表明，可达性分析可以解决与众所周知的饱和技术的广泛的一类寡纯结构。此外，对于更严格的齐次结构，我们能够给出具体的复杂性上界。我们展示了充分的适用性，我们的技术提出了几个具体的例子，同质结构，包含，最佳的复杂性，从文献中已知的结果。我们表明，无穷多个这样的例子，可以得到均匀结构与经典的圈产品建设。
2015-07-17 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
Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
针对带嵌套零检测的VASS可达性问题，本文得出Ackermann型上界，并提出统一方法以相同复杂度解决半线性性、可分离性等相关问题，填补了普通VASS部分问题的复杂度研究空白。
2025-05-19 cs.FL cs.LO
Universality Problem for Unambiguous VASS
我们研究无歧义VASS语言，即具有状态的向量加法系统，其转换从有限字母表中读取字母，并且其接受条件由一组最终状态定义（即，的语言）。我们表明，明确的VASS的普遍性的问题是ExpSpace完整的，在纯粹的对比，阿克曼完整的任意VASS，即使在1维。当维数d固定时，如果d至少为2，则普适性问题是PSpace完全的，并且对于1维VASS（也称为单计数器网）是coNP困难的。
2020-07-21 cs.FL cs.LO
Senescent Ground Tree Rewrite Systems
已知具有状态的基础树重写系统具有不可判定的控制状态可达性问题。从最近引入的范围有界的多栈下推系统的灵感，我们定义衰老地面树重写系统。这些是具有状态的基础树重写系统的限制，使得树的节点在已经见证了先验固定数量的控制状态改变之后不再被重写。以及推广范围有界的多栈下推系统，我们表明-通过减少和重置Petri网-这些系统有一个阿克曼完全控制状态可达性问题。然而，正规树集的可达性仍然是不可判定的。
2013-11-19 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
Reachability for Bounded Branching VASS
本文考虑有界分支VASS的可达性问题。有界VASS是经典VASS模型的一种变体，其中所有配置中的所有值的上限都是一个固定的自然数，在输入中以二进制编码。这个模型在2012年获得了很多关注，当时Haase等人展示了它与时间自动机的联系。2013年，Fearnley和Jurdzienski证明了这个模型中的可达性问题即使在1维中也是PSPACE完全的。在这里，我们调查的可达性问题的复杂性时，该模型扩展与分支过渡，我们证明了这个问题是EXPTIME完全时，尺寸为2或更大。
2019-08-19 cs.FL
Decision Questions for Probabilistic Automata on Small Alphabets
研究一元和二元概率有限自动机的空性与$\lambda$-可达性问题，根据歧义度和字母表大小刻画其复杂度，揭示了多项式与有限歧义下的NP困难性及EXPTIME可解性。
2023-12-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
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 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
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
字符串上的有限状态自动机的扩展，如多头自动机或多计数器自动机，已成功地用于编码许多无限状态非正则验证问题。在本文中，我们考虑一个推广的自动机理论的无限状态验证从字符串标记串并行图。我们定义了一个模型的非确定性，2路，并发自动机工作串并行图和通信通过共享寄存器的节点上的图形。我们考虑以下验证问题：给定一个系列的串并行图描述的上下文无关的图转换系统（GTS），并在串并行图的并发自动机，是一些图所产生的GTS接受的自动机？一般的问题是不可判定的已经（单向）多头自动机字符串。我们表明，一个有界的版本，其中自动机使固定数量的反转沿图，并使用固定数量的共享寄存器是可判定的，即使有没有约束的GTS生成的串并行图的大小。我们的可判定性结果是基于建立上下文切换的数量是有界的，并对有界并发自动机的计算进行编码，以将空性问题减少到下推自动机的空性问题。
2015-09-24 cs.FL
Reachability in Continuous Pushdown VASS
本文研究连续 PVASS 的可达性问题，证明其为 NEXPTIME 完全，并展示了该结果在二进制编码、固定维度、有界栈及一元编码等条件下的稳健性与困难性。
2023-10-31 cs.FL cs.PL
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
The complexity of bounded context switching with dynamic thread creation
并发下推系统动态网络（DCPS）是具有共享全局状态和动态创建线程的多线程递归程序的理论模型。DCPS的（全局）状态可达性问题通常是不可判定的，但Atig等人（2009）表明，当每个线程被限制为固定数量的上下文切换时，它变得可判定，并且在2 EXPSPACE中。该问题的最著名的下限是EXPSPACE-hard，并且当每个线程是有限状态机并且原子地运行到完成时（即，不切换上下文）。在本文中，我们关闭的差距表明，状态可达性是2 EXPSPACE硬已经只有一个上下文切换。有趣的是，状态可达性分析在EXPSPACE中既适用于没有上下文切换的下推线程，也适用于具有任意上下文切换的有限状态线程。因此，递归线程与单个上下文切换一起提供指数优势。我们的证明技术对2 EXPSPACE硬度结果具有独立的兴趣。我们介绍了传感器定义的Petri网，一个简洁的表示Petri网，并显示覆盖是2 EXPSPACE-硬的这个模型。为了显示2 EXPSPACE-硬度，我们提出了一个修改版本的Lipton的模拟计数器机的Petri网，其中的网程序可以显式递归过程调用到一个有界的深度。
2020-11-11 cs.FL cs.LO cs.PL
Complexity of Liveness in Parameterized Systems
我们研究了领袖贡献者系统的活性验证的细粒度复杂性。这些由一个指定的领导者线程和任意数量的相同的贡献者线程通过共享内存进行通信。活性验证问题询问是否存在领导者无限频繁地到达最终状态的系统的无限计算。与其对应的可达性问题一样，该问题也是NP完全问题。我们的研究结果表明，即使从细粒度的角度来看，复杂性的差异只有一个多项式的因素。活性验证分解为可达性和循环检测。我们提出了一个不动点迭代法，在多项式时间内求解后者。对于可达性，我们重新考虑两个标准参数化。当由领导者的状态数L和数据域D的大小参数化时，我们给出了（L + D）^O（L + D）时间算法。它改进了以前的算法，从而解决了一个开放的问题。当由贡献者C的状态数参数化时，我们重用O *（2^C）时间算法。我们将展示如何将这两种算法与循环检测连接起来，以获得用于活性验证的算法。组合算法的运行时间匹配的可达性，证明了细粒度的活性验证的下限得到满足。
2019-10-07 cs.CC cs.FL
Interrupt Timed Automata: verification and expressiveness
我们介绍了类的混合时间自动机（ITA），一个子类的混合自动机非常适合于描述的时间多任务系统在单处理器环境中的中断。虽然可达性问题是不可判定的混合自动机，我们证明了它是可判定的ITA。更确切地说，我们证明了untimed语言的ITA是定期的，通过建立一个有限自动机作为一个广义类图。然后，我们建立ITA的可达性问题是在NEXPTIME和PTIME时，时钟的数量是固定的。为了证明第一个结果，我们定义了ITA的一个子类ITA-，并证明了（1）任何ITA都可以在ITA-中约简为一个语言等价的自动机，（2）这个子类中的可达性问题在NEXPTIME中（没有任何类图）。在接下来的步骤中，我们将研究ITA上实时的属性的验证。我们证明了模型检验SCL，一个片段的时间线性时间逻辑，是不可判定的。另一方面，我们给出了两个定时分支时间逻辑片段的模型检验过程。我们还比较了经典的时间自动机和ITA的表达能力，并证明了相应的家庭接受的语言是无与伦比的。结果也适用于受控实时自动机（CRTA），扩展时间自动机接受的语言。最后，我们结合ITA与CRTA，在一个模型，其中包括两个类，并表明可达性问题仍然是可判定的。此外，我们表明，ITA的语言既不是封闭的互补下，也没有交叉。
2012-03-29 cs.FL
Guessing the buffer bound for k-synchronizability
如果表示执行的所有消息序列图可以被划分为$k$发送后接$k$接收的片段，则通信系统是$k$可同步的。前面已经表明，对于一个固定的给定$k$，可以决定一个通信系统是否是$k$ -同步的。这个结果是有趣的，因为可达性问题可以解决$k$ -同步系统。然而，决策过程假设边界$k$是固定的。在本文中，我们改进了这一结果，并表明，它是可能的，以决定是否存在这样的界$k$。
2021-04-29 cs.FL
Courcelle's Theorem Made Dynamic
动态复杂度是指当输入稍微改变时，更新问题的输出。我们研究了动态复杂性的模型检验一个固定的一元二阶公式在一个固定的最大图有界树宽度的子图的发展，在这里的子图的发展失去或获得边缘（从最大图）。我们表明，这个问题是在DynFO（与LOGSPACE预计算），通过减少一个戴克可达性问题的非循环自动机。
2017-02-16 cs.CC cs.FL
Complexity of the dynamics of reaction systems
反应系统是受生物化学过程启发的离散动力系统，其动力学行为由有限集合上的集合论运算表示。因此，反应系统提供了对生物化学现象的描述，补充了更传统的方法，例如基于微分方程的方法。一个关于反应系统动力学行为的决策问题（如循环和不动点/周期点，吸引子和可达性）的全面列表，以及相应的计算复杂性，从易处理的问题到PSPACE完全问题。
2019-03-19 cs.DM cs.FL
