On the Complexity of Reachability in Parametric Markov Decision Processes
本文研究了参数马尔可夫决策过程（pMDP），它是马尔可夫决策过程（MDP）的一种扩展，其中转移概率由有限参数集上的多项式描述。固定所有参数的值会产生MDP。特别是，本文研究了这些参数的值，使诱导MDP满足一些可达性约束的复杂性。我们讨论不同的变体取决于比较运算符的约束和域的参数值。我们改进了该问题的所有已知下界，并特别提供了该问题不同变体的ETR完整性结果。此外，我们提供的见解在功能描述诱导可达性概率，以及如何pMDPs概括并发随机可达性游戏。
2019-04-02 cs.CC cs.LO
The surprizing complexity of generalized reachability games
图上的游戏为反应系统提供了一个自然而强大的模型。在本文中，我们考虑广义可达目标，定义为合取的可达目标。我们首先证明，在这样的游戏中，决定赢家是$\PSPACE$ -完全的，虽然它是固定参数易处理的可达性目标的数量作为参数。此外，我们考虑了两个球员的记忆要求，并给出匹配的上界和下界的大小获胜的策略。为了允许更有效的算法，我们考虑广义可达性游戏的子类。我们表明，边界的可达集的大小给出了两个自然的子类，决定赢家可以有效地完成。
2012-02-03 cs.CC cs.GT cs.LO
The Complexity of Reachability Problems for Flat Counter Machines with Periodic Loops
本文证明了NP-完全性的可达性问题的类平面计数器的不同的界限，更一般地说，八边形关系，标签上的转变的循环。证明是基于这样的事实，即这种关系的功率序列$\{R^i\}_{i=1}^\infty$可以被编码为矩阵的周期序列，并且该序列的前缀和周期都是关系$R$的二进制编码$\bin{R}$的大小的$2^{\mathcal{O}(\bin{R})}$。这一结果允许表征计数器机器\cite{cav10,comon-jurski98}的最研究的类之一的可达性问题的复杂性，并具有潜在的影响，在程序验证的其他问题。
2016-02-14 cs.CC cs.LO
Dynamic complexity of Reachability: How many changes can we handle?
在2015年，有研究表明，任意有向图的可达性可以在插入或删除单条边后通过一阶公式更新。后来，在2018年，这被扩展为大小$\frac{\log n}{\log \log n}$的更改，其中$n$是图形的大小。当多数量词也可以使用时，可以处理多对数大小的变化。在本文中，我们扩展这些结果表明，对于多对数大小的变化，一阶更新公式足以保持（1）无向可达性，（2）定向可达下插入。对于高效并行算法可以计算非零循环权重的有向图类，可以利用更新公式来保持可达性，该更新公式可以在多对数大小的变化下使用“模2”量词。这些类的例子包括平面图和有界树宽的图。这里显示了后者。由于我们考虑的逻辑不能在较大的变化下保持可达性，因此我们的结果对于变化的大小是最优的。
2020-04-27 cs.CC 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
Decidability and Complexity of Decision Problems for Affine Continuous VASS
本文研究仿射连续VASS的可达性、可覆盖性与状态可达性问题，针对不同仿射操作类给出几乎完全的可判定性分类，并补充紧复杂性上下界。
2024-05-17 cs.LO
On the quantifier-free dynamic complexity of Reachability
在Patnaik和Immerman的动态复杂度框架下，研究了可达性查询的动态复杂度，并限制在无量词更新公式下。结果表明，与此限制，可达性查询不能动态维护，既不与二进制辅助关系，也不与一元辅助功能，和三元辅助关系是更强大的图查询比二进制辅助关系。进一步的不可表达的结果给出了可达性查询在不同的设置，以及无量词更新公式的语法限制。此外，一些其他查询的不可表达的结果。
2015-01-28 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
On The Complexity of Counter Reachability Games
对抗可达性博弈是由两个玩家在一个带有标签边的图上进行的。每次移动包括从当前位置拾取一条边，并将其标签添加到一个反向量。目标是在给定位置达到给定的计数器值。我们区分三种语义计数器可达性游戏，根据发生什么时，计数器值将成为负的：边缘被禁用，或启用，但计数器值变为零，或启用。我们考虑的问题，决定在计数器可达性游戏的赢家，并表明，在大多数情况下，它具有相同的复杂性下的所有语义。令人惊讶的是，在一种语义下，维度1的复杂性取决于目标值是零还是任何其他整数。
2013-07-19 cs.GT cs.LO
The Complexity of Reachability in Parametric Markov Decision Processes
本文介绍了参数马尔可夫决策过程（pMDP）的可达性决策问题的复杂性，马尔可夫决策过程（MDP）的扩展，其中转移概率由多项式描述的一个有限的参数集。特别是，我们研究了这些参数的值，使诱导MDP满足一些最大或最小的可达性概率约束的复杂性。我们讨论不同的变体取决于比较运算符的约束和域的参数值。我们改进了所有已知的下界这个问题，并特别提供了ETR的完整性结果，这个问题的不同变体。
2020-09-28 cs.LO
The Cost of Parameterized Reachability in Mobile Ad Hoc Networks
我们调查的影响，自发运动的复杂性验证问题的自动机为基础的协议模型的网络与选择性广播通信。我们首先考虑错误状态的可达性，并证明参数化验证是可判定的多项式复杂性。然后，我们转向更丰富的查询，并显示当考虑具有否定或基数约束的属性时，复杂性如何变化。
2012-02-27 cs.LO
Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints
本文研究了具有非负速率的矩形混合自动机（RHA+）的时间有界可达性问题。这个问题最近被证明是可判定的[Brihaye et al，ICALP 11]（即使对于非常简单的混合自动机类，无界可达性问题也是不可判定的）。然而，[Brihaye等人，ICALP 11]没有提供时间有界可达性问题的复杂性的精确表征。本文件的贡献有三个方面。首先，我们提供了一个新的NExpTime算法来解决RHA+上的时间有界可达性问题。该算法对[Brihaye等人，ICALP 11]的算法进行了至少一个指数改进。其次，我们证明了这种新算法是最优的，通过建立一个匹配的下限：时间有界的RHA+的可达性，因此是NExpTime完成。第三，我们在实际的方向上扩展了这些结果，通过证明我们可以有效地计算不动点，这些不动点覆盖可达的状态集（分别为）。共同可达）。
2012-11-06 cs.LO
Reachability analysis of first-order definable pushdown systems
我们研究下推系统的控制状态，堆栈字母表，和过渡关系，而不是有限的，是一阶定义在一个固定的可数无限结构。我们表明，可达性分析可以解决与众所周知的饱和技术的广泛的一类寡纯结构。此外，对于更严格的齐次结构，我们能够给出具体的复杂性上界。我们展示了充分的适用性，我们的技术提出了几个具体的例子，同质结构，包含，最佳的复杂性，从文献中已知的结果。我们表明，无穷多个这样的例子，可以得到均匀结构与经典的圈产品建设。
2015-07-17 cs.FL cs.LO
On the Reachability Problem for Two-Dimensional Branching VASS
本文研究了二维分支向量加法系统（BVASS）的可达性问题，证明了该问题在二维下是可判定的，并证明其可达集具有可计算的半线性表示。
2025-06-27 cs.FL cs.LO
Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes
研究了具有状态的向量加法系统（VASSes）在固定维数下的可达性问题的复杂性。我们提供了四个改进目前已知的现有技术的下界：1）\np -一元平坦$4$ -血管（维度4中的血管）的硬度，2）\pspace -一元$5$ -血管的硬度，3）\expspace -二元$6$ -血管的硬度，和4）\tower -一元$8$ -血管的硬度。
2022-03-08 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
Vector Addition System Reversible Reachability Problem
向量加法系统的可达性问题是网理论的一个中心问题。这个问题已知是可判定的，但其复杂性仍然未知。而这个问题是EXPSPACE-硬的，没有基本的上限复杂性是已知的。在本文中，我们考虑可逆的可达性问题。这个问题包括决定两个配置是否彼此可达，或者等价地，如果它们在可达图的同一个强连通分量中。我们证明了这个问题是EXPSPACE完全的。作为所介绍的材料的应用，我们描述了一个矢量加法系统的可逆域。
2013-02-26 cs.LO
The reachability problem for vector addition systems with a stack is not elementary
通过适应迭代码构造Stockmeyer，我们证明了向量加法系统的可达性问题与堆栈不具有初等复杂性。作为一个推论，同样的下界也适用于树上的二元一阶逻辑的可满足性问题，其中无界数据只能标记叶节点。这两个问题是否可以解决仍然是一个悬而未决的问题。
2013-10-07 cs.FL cs.LO
A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter
该研究针对三类单计数器系统，通过引入Presburger公式的通用框架，证明了半线性目标集问题的复杂性二分定理，且可判定公式所属的复杂度侧。
2025-05-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
The Reachability Problem for Petri Nets is Not Primitive Recursive
我们提供了一个阿克曼复杂性下界检查程序的可达性问题，一个模型相当于Petri网。此外，在固定维数的$2d+4$中，我们证明了该问题是$\mathbb{F}_d$ -困难的.作为一个直接的推论，10维中的可达性问题不是基本的。
2021-09-02 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 is Tower Complete
向量加法系统可达性问题复杂性的完整刻画一直是一个悬而未决的问题。问题显示为塔完成。
2020-03-21 cs.LO
The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
Technische Universität Darmstadt（达姆施塔特工业大学）；Université libre de Bruxelles（布鲁塞尔自由大学）；Departement d’Informatique（计算机系）
研究了具有无限时域可达性目标的马尔可夫决策过程的永不变差关系。如果从p到达目标状态集的最大概率至多与从q到达的最大概率相同，则状态q永远不会比状态p差，而不考虑标记转移的概率。极端概率态、终结分量和本质态都是由NWR导出的等价关系的特例。使用NWR，可以折叠相同等价类中的状态。然后，可以移除导致次优状态的动作。我们证明了与计算NWR相关的自然决策问题是CONP完全的。最后，我们扩展了以前已知的不完全多项式时间迭代算法下近似的NWR。
2018-02-24 cs.AI cs.LO
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
本文研究终止项重写系统中是否可到达大小不超过 n 的项，按终止性证明方法给出 NP、N2ExpTime/NExpTime 与 PSpace 等复杂性分类，并分析合流性及大项变体的影响。
2025-10-14 cs.LO
Reachability in 3-VASS is Elementary
本文研究了带状态的3维向量加法系统（3-VASS）的可达性问题，通过引入用小半线性集逼近2-VASS可达集的新技术，证明了最短路径长度存在三指数上界，从而将该问题的复杂度上界改进为双指数空间，显著缩小了复杂度差距。
2025-04-28 cs.FL cs.LO
Improved Algorithm for Reachability in $d$-VASS
本文提出了一种结合线性路径方案与一般分解算法的新算法，将固定维度VASS可达性问题的复杂度上界从$\mathsf{F}_{d + 4}$改进至$\mathsf{F}_{d}$。
2024-04-23 cs.FL cs.LO
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
本文研究定量可达性博弈中SPE的复杂性，证明约束存在性问题是PSPACE完全的，并提出一种通过迭代约束至不动点来刻画SPE结果集的新算法。
2020-11-04 cs.GT cs.LO
Demystifying Reachability in Vector Addition Systems
在向量加法系统（VAS）成立30多年后，向量加法系统（VAS）可达性的可判定性证明仍然保持着许多神秘。这些证明依赖于一个关键的分解运行先后完善迈尔，Kjuaju，和兰伯特，这似乎是相当神奇的，并没有复杂性上限是已知的。我们首先提供了一个理由，这种分解技术，通过显示，它计算的理想分解的运行集，使用运行之间的自然嵌入关系以及准序。在第二部分中，我们应用最近的结果终止的复杂性，以及准订单和订单，以获得三次阿克曼上界的分解算法，从而提供了第一个已知的上界一般VAS可达性。
2015-05-13 cs.LO
Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
参数时间自动机（PTA）是时间自动机的扩展，其中时钟可以与参数进行比较。可达性问题要求存在一个非负整数的参数分配，使得可达性在底层的时间自动机中保持。PTA的可达性问题长期以来被认为是不可判定的，已经超过了三个参数时钟。几年前，Bundala和Ouaknine证明了对于两个参数时钟和一个参数的PTA，可达性问题是可判定的，并且还证明了复杂度类PSPACE^NEXP的下界。我们的主要结果是，具有一个参数的两参数时间自动机的可达性问题是EXPSPACE-完全的。我们的贡献是双重的。对于EXPSPACE下界，我们利用复杂性理论的深层结果，即EXPSPACE的可串行化表征（基于巴林顿定理）和中国剩余表示中的数字的对数空间翻译为二进制表示。对于EXPSPACE上界，我们给出了一个仔细的指数时间减少PTA两个参数的时钟和一个参数的参数单计数器自动机（POCA）的一个参数的基础上轻微的调整，由于Bundala和Ouaknine建设的一个子类。我们提供了一系列的技术来分区一个虚构的运行的POCA到几个精心选择的子运行，使我们能够证明，它是足够的，只考虑指数量级的参数值。这使我们能够显示一个双指数上界的值的唯一参数的PTA在两个参数时钟和一个参数。我们希望我们的技术的扩展导致最终建立的可达性参数时间自动机与两个参数时钟（和任意多个参数）的长期开放的问题的可判定性。
2020-11-13 cs.FL cs.LO
Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives
我们考虑有限状态并发随机博弈，由k>=2个参与者进行无限轮的博弈，其中在每一轮中，每个参与者同时且独立于其他参与者选择一个行动，此后，后继状态由当前状态和所选择的行动给出的概率分布确定。我们认为可达性目标，给定的目标集的状态要求，在目标中的一些状态被访问，和双重安全目标，给定的目标集要求，只有在目标集中的状态被访问。我们感兴趣的是固定策略的复杂性，衡量他们的耐心，这是定义为最小的非零概率的倒数。我们的主要结果如下：我们证明了在两人零和并发随机对策中，（一个局中人的可达性目标和另一个局中人的互补安全目标）：（i）对于两个局中人，最优策略和ε-最优策略的耐心的最优界都是双指数的;和（ii）即使在一个单一的非吸收状态指数（在行动的数量）耐心的游戏是必要的。在一般情况下，我们研究类的非零和游戏承认固定的ε-纳什均衡。我们证明了如果至少有一个局中人具有可达性目标，那么双指数耐心可能是必需的双-纳什均衡策略，而与此相反，如果所有局中人都具有安全目标，则双-纳什均衡策略的最优耐心界限仅是指数的。
2015-06-08 cs.GT cs.LO
On the Reachability Problem for One-Dimensional Thin Grammar Vector Addition Systems
Shanghai Jiao Tong University（上海交通大学）
本文提出了一种针对一维薄语法向量加法系统可达性问题的有效整数规划方法，并给出了具有更紧上界的非确定算法。
2026-02-05 cs.LO
Reachability in Fixed VASS: Expressiveness and Lower Bounds
本文研究了固定 VASS 且仅初始配置可变时的可达性问题，证明固定 VASS 能完全表达自然数初始段算术，并揭示了一元配置下的弱归约及二元配置下五计数器 VASS 的 PSPACE-hard 下界。
2023-10-25 cs.FL cs.LO
Petri Net Reachability Graphs: Decidability Status of First Order Properties
我们调查的可判定性和复杂性状态的模型检查问题的无标签的可达图的Petri网，考虑一阶和模态语言没有标签的过渡或原子命题标记。我们考虑几个参数来区分可判定问题和不可判定问题。我们不仅能够提供精确的边界和系统的分析，而且还展示了我们证明技术的鲁棒性。
2012-10-19 cs.LO
Dynamic Complexity under Definable Changes
本文在Patnaik和Immerman的DynFO框架下研究了可定义变更操作下的动态复杂性。它示出的变化定义的参数自由的一阶公式，所有（统一）$AC^1$查询可以保持一阶动态程序。进一步地，许多单元组变化的维护结果被扩展到更强大的变化操作：（1）无向图的可达性查询在单元组变化和一阶定义插入下是一阶维护，同样地，有向无环图的可达性查询在无量词插入下也是一阶维护。(2)上下文无关语言是在$Σ_1$定义的变化下的一阶维护。这些结果是补充了几个不可表达的结果，例如，可达性查询不能保持下定义的，无量词删除的无量词程序。
2017-01-10 cs.DB cs.LO
3-VASS Reachability is in EXPSPACE
Shanghai Jiao Tong University（上海交通大学）；Shanghai Normal University（上海师范大学）
研究三维向量加法系统可达性问题的复杂度，通过分层可泵性分析，证明该问题属于指数空间，此前已知算法是非初等的，此研究给出新结论。
2026-07-17 cs.FL cs.LO
Flatness and Complexity of Immediate Observation Petri Nets
在以前的论文中，我们介绍了即时观察（IO）Petri网，一类感兴趣的研究人口协议和酶化学网络。在本文的第一部分中，我们表明，IO网是全球平坦的，所以他们的安全性能可以检查有效的符号模型检验工具，使用加速技术，如FAST。在第二部分中，我们研究了分支IO网（BIO网），其转换可以创建令牌。BIO网扩展了IO网和无通信网，也称为BPP网，这是一个广泛研究的类别。我们表明，虽然BIO网不再是全球平坦的，他们的可达标记集可能是非半线性的，他们仍然是局部平坦的。因此，BIO网的可覆盖性和可达性问题，甚至是它们的某个集合参数化版本，都在PSPACE中。这使得BIO网的第一个自然网类与非半线性可达性关系，可达性问题是可证明的简单比一般的Petri网。
2020-07-21 cs.LO
The Complexity of Concurrent Rational Synthesis
在本文中，我们研究了合理的合成问题的并发博弈结构的各种目标，从可达性的Muller条件。我们提出了一个新的算法，建立了非合作的理性综合问题，完全依赖于博弈论技术，而不是以前的方法，是基于逻辑的可判定性。由于这种方法，我们构建了一个零和回合制游戏，可以适应上述每一个目标，从而获得新的复杂性结果。特别是，我们表明，可达性，安全性，Büchi，和合作Büchi条件是PSpace完全的，穆勒，街，和拉宾是PSpace硬和ExpTime。
2018-06-08 cs.GT cs.LO
Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth?
答案集编程（ASP）是一个问题建模和解决框架的几个问题，在KR与日益增长的工业应用。ASP也是近年来研究计算复杂性和深入理解计算难度及其来源的一个热点。这些研究导致了富有成效的表征方面的复杂性类，细粒度的见解形式的二分法风格的结果，以及详细的参数化的复杂性景观。最近，这导致了一个新的结果，建立的措施树宽，它捕获的程序的结构密度，评估的知名类正常的程序预计将稍微困难比决定可满足性（SAT）。然而，目前还不清楚如何利用ASP的这种结构性力量。本文论述了一种新的减少SAT到正常的ASP，超越了众所周知的编码：我们明确利用ASP的结构功率，从而我们次线性地减少树的宽度，这可能无法显着改善。然后，与现有的结果相比，这通过建立依赖图的周期长度（SCC大小）对树宽的所需函数依赖来以细粒度的方式表征硬度。
2023-01-18 cs.AI cs.DM cs.LO
Non-Elementary Complexities for Branching VASS, MELL, and Extensions
我们研究了向量加法系统的分支扩展上的可达性问题的复杂性，这使我们能够推导出命题线性逻辑的片段和变体的新的非初等复杂性界。我们证明了乘法指数片段的可证明性在仿射情况下已经是塔硬的，因此是非初等的。我们匹配这个下界的充分命题仿射线性逻辑，证明其塔完全性。我们还证明了命题压缩线性逻辑的可证性是阿克曼完备的。
2022-05-16 cs.LO
Complexity of Verification and Synthesis of Threshold Automata
本文研究了阈值自动机的验证与合成问题的复杂性，证明了多个核心问题的计算复杂度，并提出了一种基于Presburger公式的新算法。
2025-11-28 cs.DC cs.LO
Alleviating State-space Explosion in Component-based Systems with Distributed, Parallel Reachability Analysis Algorithm
在这项工作中，我们减轻了著名的状态空间爆炸（SSE）的问题，基于组件的系统（CBS）。我们认为CBS可以被指定为一个系统的n个通信有限状态机（CFSMs）的交会/握手方法进行交互。为了避免传统的基于交错语义的乘积机器组合所带来的SSE问题，我们构造了一种基于面向状态的偏序语义的和机器组合.求和机由一组n个展开的CFSM组成。通过静态地存储在同步点处的全局状态向量的仅一个小子集（称为同步环境向量）并且根据要验证的可达性在需要的基础上动态地生成全局状态向量的其余部分，求和机对乘积机的SSE进行量化。我们证明了检查的全局状态向量的可达性检查给定的状态向量的组件的局部可达性，通过一个并行的，分布式的算法的实施。并行和分布式算法来生成和机和验证它的可达性都没有指数复杂度是这项工作的贡献。保留字：交错语义，偏序语义，和机，积机，同步点，同步环境状态向量，可达性。
2018-08-13 cs.LO cs.MA
