Integer Vector Addition Systems with States
本文研究了带状态的可达向量加法系统（ZVASS）的可达性、可覆盖性和包含性问题及其推广和限制。ZVASS包括有限状态控制器，该有限状态控制器具有在整数范围内的有限数量的计数器。虽然ZVASS中的可达性是NP完全的，但事实证明，尽管它们是自然的，从复杂性的角度来看，这个类在文献中很少受到关注。我们填补了这一空白，提供了一个深入的分析上述决策问题的计算复杂性。最有趣的是，事实证明，虽然将重置操作添加到普通VASS中分别导致可达性和可覆盖性的不可判定性和阿克曼硬度，但它们可以添加到ZVASS中，同时保留可覆盖性和可达性的NP完全性。
2014-07-28 cs.FL
Zenoness for Timed Pushdown Automata
时间下推自动机是用有限个实值时钟扩展的下推自动机。此外，堆栈中的每个符号都配备了表示其年龄的值。转变的启用可取决于时钟的值和最顶部码元的年龄。因此，稠密时间下推自动机是下推自动机和时间自动机的子类。我们之前已经证明了这个模型的可达性问题是可判定的。本文研究了zenoness问题，证明了它是EXPTIME-完全的。
2014-02-27 cs.FL
Reachability in One-Dimensional Pushdown Vector Addition Systems is Decidable
该研究解决了一维下推向量加法系统可达性这一十年开放问题，通过构造等价的薄性质文法向量加法系统，结合已有结论证明其可达性可判定，并推导了初等时间判定的传递性。
2024-11-04 cs.FL
Approaching the Coverability Problem Continuously
Petri网的可覆盖性问题在并发共享内存程序的验证中起着核心作用。然而，它的高EXPSPACE完全复杂性在现实世界的实例中遇到时构成了挑战。在本文中，我们开发了一种新的方法来解决这个问题，这主要是基于应用前向覆盖连续Petri网作为修剪标准内的向后覆盖框架。我们的方法的基石是最近开发的多项式时间算法的可达性在连续Petri网到SMT的有效编码。我们证明了我们的方法在文献标准基准测试中的有效性，这表明我们的方法比任何现有的工具决定了更多的实例，而且通常更快，特别是在大型实例上。
2016-01-09 cs.FL cs.LO
Turn Complexity of Context-free Languages, Pushdown Automata and One-Counter Automata
Università degli Studi di Milano（米兰大学）；Dipartimento di Informatica（计算机系）
研究了推导机和一计数器机在有限turn内的接受复杂度，证明了某些语言在亚线性但非常数数量的turn内被接受，并展示了复杂性层次的无限性。
2026-03-09 cs.FL
Verifying Unboundedness via Amalgamation
该研究提出配备良拟序且支持运行合并的抽象系统概念，涵盖VAS、PDS等多类无限状态系统，为无界性相关问题提供通用简洁的算法方案，带来简化证明或新的可判定性结果。
2024-06-20 cs.FL
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
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
本文研究文法控制向量加法系统（GVASes）弱可计算的函数，证明其能计算快速增长函数但无法计算逆函数或次线性函数，基于独立有趣的泵引理。
2019-12-17 cs.FL cs.LO
Reachability Problem for Weak Multi-Pushdown Automata
本文研究了多下推自动机的一个受限子类的可达性分析。我们假设自动机的控制状态是偏序的，并且自动机的所有转换都是相对于顺序向下的。我们证明了可达性问题的可判定性和向后可达集的可计算性。作为主要的贡献，我们确定相关的子类的可达性问题成为NP完全。这与无通信向量加法系统（无状态多下推自动机的特殊情况）的相同问题的复杂性相匹配。
2013-09-20 cs.FL cs.LO
Pushdown automata, lambda-graph systems and C*-algebras
一个$λ$ -图系统是一个带有某种附加结构的标号Bratteli图，它表示一个子移位并产生一个$C^*$ -代数.本文从下推自动机出发构造了一个$λ$ -图系统，使得该自动机所接受的语言与$λ$ -图系统所给出的子移位的可接受词的语言一致.给出了接受Markov-Dyck移位和sofic-Dyck移位语言的下推自动机的$λ$ -图系统。
2014-07-26 cs.FL math.DS math.OA
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
Techniques for Showing the Decidability of the Boundedness Problem of Language Acceptors
本文针对多数自动机/文法模型有界性问题可判定性未知的背景，提出多带自动机刻画、存储语言两种新技术，归约证明更大类单向非确定自动机和文法模型的有界性可判定。
2024-05-17 cs.FL
Pushdown Automata and Context-Free Grammars in Bisimulation Semantics
本文在反应式图灵机及互模拟语义下，通过引入带中间接受的序列算子与状态感知概念，恢复了下推自动机与上下文无关文法之间的经典对应关系。
2023-03-01 cs.FL cs.LO
Unary Pushdown Automata and Straight-Line Programs
我们考虑一元字母表上的确定性下推自动机（简称udpda）的决策问题。Udpda是一种简单的计算模型，它完全接受一元正则语言，但比有限状态自动机更简洁。我们完成了udpda的复杂性景观表明，空性（从而普遍性）是P-硬，等价和压缩的成员资格问题是P-完全的，包含是coNP-完全的。我们的上限是基于一个翻译定理之间的udpda和直线程序的二进制字母表（SLP）。我们发现，任何udpda的特征序列可以表示为一对SLP-一个前缀，一个套索-具有线性的大小的udpda的大小，可以在多项式时间计算。因此，udpda上的决策问题被简化为SLP上的决策问题。相反，任何SLP都可以在对数空间中转换为udpda，这构成了我们的下界证明的基础。我们展示了SLP的有序匹配问题的CoNP-硬度，从中我们推导出包含的CoNP-硬度。此外，我们完成了一元不确定下推自动机的复杂性景观显示的普遍性问题是$Π_2 \mathrm P$硬，使用一类新的整数表达式。我们的技术有超越udpda的应用。我们表明，我们的研究结果意味着$Π_2 \mathrm P$ -完整的Presburger算法和压缩匹配问题与一个字符的通配符的coNP下界的自然片段。
2014-03-03 cs.CC cs.FL
Exploring VASS Parameterised by Geometric Dimension
University of Warsaw（华沙大学）；Shanghai Jiao Tong University（上海交通大学）
本文研究了VASS中几何维度参数化下的可达性问题，改进了覆盖性和无界性问题的复杂度分析，并探讨了几何维度与SCC维度的差异。
2026-02-17 cs.FL
PVASS Reachability is Decidable
University of Warsaw（华沙大学）；TU Braunschweig（布伦瑞克工业大学）
本文证明了具有状态的推导向量加法系统（PVASS）可达性问题在一般情况下是可判定的，方法类似于VASS可达性的KLMST算法，但利用了更复杂的进程总结形式。
2026-02-18 cs.FL cs.LO
Visual Execution and Validation of Finite-State Machines and Pushdown Automata
针对自动机理论课程中学生理解非确定性与下推自动机的困难，提出两种动态可视化工具，逐步展示所有计算并支持状态属性验证，以辅助机器设计与验证。
2025-08-05 cs.FL cs.HC cs.PL
Infinite-State Energy Games
能量游戏是一类在有限图上的2人回合制游戏，其中转换用整数向量标记，表示多维资源（能量）的变化。一个参与者试图保持每个组成部分的累积变化都是非负的，而另一个参与者试图阻止这一点。我们考虑广义能量游戏无限游戏图引起的下推自动机（建模递归）或其子类的一计数器自动机。我们的主要结果是，能量游戏是可判定的情况下，游戏图是由一个计数器自动机和能量是一维的。另一方面，每一个进一步的推广都是不可判定的：具有二维能量的单计数器自动机上的能量博弈是不可判定的，即使能量是一维的，下推自动机上的能量博弈也是不可判定的。此外，我们证明了能量游戏和模拟游戏是相互可约的，因此我们还获得了几个新的（非）可判定性的问题之间的下推自动机和向量加法系统的模拟前序检查结果。
2014-05-03 cs.FL cs.GT
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
本文研究可重构广播、带标识符寄存器的多智能体参数化网络，证明一般可覆盖性可判定但非原始递归，其他同步问题不可判定，而单寄存器情形为 NP 完全。
2024-03-04 cs.DC cs.FL cs.LO
Monus semantics in vector addition systems with states
研究了带状态向量加法系统（VASS）的 monus 过近似语义，允许递减零值计数器，证明全程使用该语义时可达性保持可判定，并全面刻画了可达性、零可达性和覆盖性问题的复杂度。
2023-09-12 cs.FL cs.LO
An Approach to Regular Separability in Vector Addition Systems
研究了状态向量加法系统语言的正则可分性问题。它询问对于两个给定的VASS语言K和L，是否存在一个包含K且与L不相交的正则语言R。虽然问题的可判定性仍然是一个开放的问题，但有几个子类已经证明了可判定性：它对（i）一维VASS，（ii）VASS覆盖性语言，（iii）整数VASS语言和（iv）交换VASS语言是可判定的。我们提出了一个一般的方法来确定定期可分性。我们用它来决定一个任意的VASS语言从类（i），（ii）和（iii）中的任何语言的正则可分性。这推广了所有以前的结果，包括（iv）。
2020-06-30 cs.FL cs.LO
Oracle Pushdown Automata, Nondeterministic Reducibilities, and the CFL Hierarchy over the Family of Context-Free Languages
为了扩展上下文无关语言的基本理论，我们在不确定的单向下推自动机中加入了额外的预言机机制，从而自然地在形式语言中引入了各种不确定的可约性。作为NP-约简的一个自然限制，我们引入了多-一CFL约简的概念，并为进一步的论述制定了一个连贯的框架。两个更强大的约简-有界真值表和图灵CFL-约简-也进行了比较讨论。特别是图灵CFL-约简，帮助我们引入了一个精致的层次结构，称为CFL层次结构，建立在上下文无关语言的CFL家族之上。对于这个层次结构的每一个层次，其基本的结构性质证明和三个可供选择的特征。NC（2）中不包括第二水平，除非NP= NC（2）。层次结构的第一级和第二级是不同的。层次结构的其余部分（更强烈地说，在层次结构的每一层上建立的布尔层次结构）也是无限的，除非NP上的多项式层次结构崩溃。这是根据使用对数空间多-一归约的CFL层次结构的第k+1级上的布尔层次结构的多项式层次结构的第k级上的布尔层次结构的表征得出的。类似地，复杂度类Theta（k）与在对数空间真值表归约下CFL层级的第k层的闭合有关。我们还认为，CFL的层次结构与CFL的层次结构相吻合的应用程序的许多一个CFL减少。我们表明，BPCFL-有界错误概率版本的CFL-不包括在CFL中，即使在存在的意见。采用一个已知的电路下界和开关引理，我们表现出一个相对化的世界，BPCFL是不是位于CFL层次的第二层。
2015-05-23 cs.CC cs.FL
Universality Problem for Unambiguous VASS
我们研究无歧义VASS语言，即具有状态的向量加法系统，其转换从有限字母表中读取字母，并且其接受条件由一组最终状态定义（即，的语言）。我们表明，明确的VASS的普遍性的问题是ExpSpace完整的，在纯粹的对比，阿克曼完整的任意VASS，即使在1维。当维数d固定时，如果d至少为2，则普适性问题是PSpace完全的，并且对于1维VASS（也称为单计数器网）是coNP困难的。
2020-07-21 cs.FL cs.LO
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
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
Checking Refinement of Asynchronous Programs against Context-Free Specifications
本文研究异步程序对Dyck语言规范的细化验证问题，证明其EXPSPACE完全，通过向下闭包构造将上下文无关任务替换为正则语言并归约到VASS，捕获引用计数资源模式。
2023-06-22 cs.FL
History-deterministic Vector Addition Systems
本文研究向量加法系统的历史确定性，证明 HD-VASS 严格介于确定性与非确定性 VASS 之间，并揭示从二维起其判定问题因可模拟 Minsky 机而不可判定。
2023-07-10 cs.FL cs.LO
Extended Models of Finite Automata
在文献中提出的许多自动机模型可以被看作是一个有限自动机配备了一个额外的存储机制。在这篇论文中，我们主要研究了两个这样的模型，即群上的有限自动机和归巢向量自动机。群$ G $上的有限自动机是配备有保持群$ G $的元素的寄存器的非确定性有限自动机。寄存器被初始化为群的单位元素，并且如果在每一步与群元素相乘之后，寄存器等于计算结束时的单位元素，则计算成功。我们调查的语言识别能力的有限自动机在整数和有理矩阵组，并揭示了新的语言类之间的关系，这些模型。我们研究了各种参数对语言识别能力的影响。我们建立了矩阵半群的决策问题和相应的自动机之间的联系。给出了关于价下推自动机和上下文无关价文法的一些新结果。我们还提出了新的归巢向量自动机模型，这是一个有限自动机配备了一个向量，可以乘以一个矩阵在每一步。可以检查向量是否与初始向量等效，并且验收标准最终处于接受状态，其中向量的值等于初始向量。我们研究的效果，各种限制的模型，限制矩阵到一个特定的集合，并允许等价性测试只在计算结束时。我们定义了模型的不同变体，并将其语言识别能力与经典模型进行了比较。
2019-12-25 cs.FL
Algebraic Closure of Matrix Sets Recognized by 1-VASS
University of Oxford（牛津大学）；Université Paris Cité, IRIF（巴黎西岱大学，IRIF）；CNRS, IRIF（法国国家科学研究中心，IRIF）
本文研究由上下文无关语言定义的矩阵集合的Zariski闭包计算问题，给出单计数器语言的可判定过程，并证明索引语言情形不可判定，采用Simon因子分解森林的推广作为关键技术。
2025-10-26 cs.FL cs.LO math.AG
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
