Reachability is Tower Complete

Taming Past LTL and Flat Counter Systems

Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that the problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. Actually, the NP upper bound is shown by adequately combining a new stuttering theorem for Past LTL and the property of small integer solutions for quantifier-free Presburger formulae. Other complexity result…

完全鲁棒混合系统可达性

Complete Robust Hybrid Systems Reachability

本文提出鲁棒微分动态逻辑，证明其对混合系统可达性问题的绝对完备性，为精确语义的混合系统提供自动验证方法。

A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems

We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proofs.

Vector Addition System Reversible Reachability Problem

The reachability problem for vector addition systems is a central problem of net theory. This problem is known to be decidable but the complexity is still unknown. Whereas the problem is EXPSPACE-hard, no elementary upper bounds complexity are known. In this paper we consider the reversible reachability problem. This problem consists to decide if two configurations are reachable one from each other, or equivalently if they are in the same strongly connected component of the reachability graph. We show that this problem is EXPSPACE-complete. As an application of the introduced materials we char…

终止项重写系统的小项可达性及相关问题

Small Term Reachability and Related Problems for Terminating Term Rewriting Systems

本文研究终止项重写系统中是否可到达大小不超过 n 的项，按终止性证明方法给出 NP、N2ExpTime/NExpTime 与 PSpace 等复杂性分类，并分析合流性及大项变体的影响。

Reachability in Vector Addition Systems is Ackermann-complete

Vector Addition Systems and equivalent Petri nets are a well established models of concurrency. The central algorithmic problem for Vector Addition Systems with a long research history is the reachability problem asking whether there exists a run from one given configuration to another. We settle its complexity to be Ackermann-complete thus closing the problem open for 45 years. In particular we prove that the problem is $\mathcal{F}_k$-hard for Vector Addition Systems with States in dimension $6k$, where $\mathcal{F}_k$ is the $k$-th complexity class from the hierarchy of fast-growing complex…

The Reachability Problem for Petri Nets is Not Elementary

Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verificatio…

Multi-weighted Markov Decision Processes with Reachability Objectives

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasabili…

多环境 MDP 中的鲁棒几乎必然可达性

Robust Almost-Sure Reachability in Multi-Environment MDPs

本文研究 MEMDP 中对所有环境鲁棒满足几乎必然可达性的策略合成问题，证明其存在性判定为 PSPACE 完全，并实现算法在多个基准上验证有效性。

Levels of Undecidability in Infinitary Rewriting: Normalization and Reachability

In [EGZ09] it has been shown that infinitary strong normalization (SNi) is Pi-1-1-complete. Suprisingly, it turns out that infinitary weak normalization (WNi) is a harder problem, being Pi-1-2-complete, and thereby strictly higher in the analytical hierarchy.

Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete

Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound whatsoever. In this paper, reachability for two-dimensional VASS is shown PSPACE-complete. This improves on a previously known doubly exponential time bound established by Howell, Rosier, Huynh and Yen in 1986. The coverability and boundedness problems are also noted to be PSPACE-complete. In addition, some complexity results are given for the reachability p…

The Complexity of Reachability in Parametric Markov Decision Processes

This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. In particular, we study the complexity of finding values for these parameters such that the induced MDP satisfies some maximal or minimal reachability probability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds …

Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints

In this paper, we study thetime-bounded reachability problem for rectangular hybrid automata with non-negative rates (RHA+). This problem was recently shown to be decidable [Brihaye et al, ICALP11] (even though the unbounded reachability problem for even very simple classes of hybrid automata is well-known to be undecidable). However, [Brihaye et al, ICALP11] does not provide a precise characterisation of the complexity of the time-bounded reachability problem. The contribution of the present paper is threefold. First, we provide a new NExpTime algorithm to solve the timed-bounded reachability…

对混合系统的有界可达性进行Delta-完全分析

Delta-Complete Analysis for Bounded Reachability of Hybrid Systems

本文提出了一种用于混合系统有界可达性问题的Delta-完全分析框架，通过求解实数上的Delta决策问题进行有界可达性检查，并考虑系统在数值扰动下的鲁棒性。

多面体可达性逻辑

Logics of polyhedral reachability

本文针对含类Until空间模态词的多面体可达性逻辑，提出公理系统并通过两步证明其相对于多面体语义学的完备性，为3D网格模型检测等应用提供理论支撑。

VASS reachability in three steps

This note is a product of digestion of the famous proof of decidability of the reachability problem for vector addition systems with states (VASS), as first established by Mayr in 1981 and then simplified by Kosaraju in 1982. The note is neither intended to be rigorously formal nor complete; it is rather intended to be an intuitive but precise enough description of main concepts exploited in the proof. Very roughly, the overall idea is to provide a decidable condition Theta on a VASS such that Theta implies reachability and its negation implies that the size of VASS can be reduced. With these …

Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete

Parametric timed automata (PTA) are an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPAC…

Tower-Complete Problems in Contraction-Free Substructural Logics

We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazić and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening ($\mathbf{FL}_{\mathbf{ew}}$) is not in Elementary (i.e., the class of decision problems that can be decided in time bounded by an elementary recursive function), but is in PR (i.e., the class of decision problems that can be decided in time bounded by a primitive recursive function). More precisely, we show that this prob…

Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verify the safety property under consideration. To avoid this, invariants can be used to dramatically prune the search space. Indeed, the problem is to guess such appropriate invariants. In this paper, we p…

几何d维向量加法状态系统（VASS）的可达性

Reachability in Geometrically $d$-Dimensional VASS

针对向量加法状态系统（VASS）的可达性问题，本文提出几何d维VASS的概念，并证明当d>2时其可达性仍属于F_d复杂度类，拓展了现有d维VASS的复杂度结果。

Optimal Label Splitting for Embedding an LTS into an arbitrary Petri Net Reachability Graph is NP-complete

For a given labelled transition system (LTS), synthesis is the task to find an unlabelled Petri net with an isomorphic reachability graph. Even when just demanding an embedding into a reachability graph instead of an isomorphism, a solution is not guaranteed. In such a case, label splitting is an option, i.e. relabelling edges of the LTS such that differently labelled edges remain different. With an appropriate label splitting, we can always obtain a solution for the synthesis or embedding problem. Using the label splitting, we can construct a labelled Petri net with the intended bahaviour (e.…

Reachability Problem for Weak Multi-Pushdown Automata

This paper is about reachability analysis in a restricted subclass of multi-pushdown automata. We assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We prove decidability of the reachability problem, and computability of the backward reachability set. As the main contribution, we identify relevant subclasses where the reachability problem becomes NP-complete. This matches the complexity of the same problem for communication-free vector addition systems, a special case of stateless multi-pushdown auto…

Efficient Restrictions of Immediate Observation Petri Nets

In a previous paper we introduced immediate observation Petri nets, a subclass of Petri nets with application domains in distributed protocols (population protocols) and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties, but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, …

路径可达性的拓扑逻辑

Topological Logics of Path-Reachability

研究一种类似Until的路径可达性模态的拓扑语义，结合Cantor导数模态给出公理系统，证明其在T1拓扑和度量空间类上的完备性与可判定性。

Inductive Reachability Witnesses

In this work, we consider the fundamental problem of reachability analysis over imperative programs with real variables. The reachability property requires that a program can reach certain target states during its execution. Previous works that tackle reachability analysis are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic/reverse Hoare logic). In contrast, we propose a novel approach for reachability analysis that can handle general programs, …

即使对于安全 λ-项，简单类型可转换性也是 TOWER 完全的

Simply typed convertibility is TOWER-complete even for safe lambda-terms

本文证明 Blum–Ong 安全 λ-演算中的 β-及 βη-可转换性仍为 TOWER 完全，将此前 PSPACE 难的下界提升至塔层完全。

Reachability Analysis of Communicating Pushdown Systems

The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received). The problem is EXPTIME-complete in the decidable case. The second result is a doubly exponential time algorithm for bounded context analysis in this setting, together with a matching lower bound. Both results extend and improve p…

仿射向量加法系统状态的可达性复杂性

The Complexity of Reachability in Affine Vector Addition Systems with States

该研究刻画了仿射VASS中整数可达性的复杂性，给出三分法：重置类NP完全，转移/复制类PSPACE完全，其余不可判定；标准可达性仅置换类可判定，并探讨了固定实例的复杂性任意性。

The surprizing complexity of generalized reachability games

Games on graphs provide a natural and powerful model for reactive systems. In this paper, we consider generalized reachability objectives, defined as conjunctions of reachability objectives. We first prove that deciding the winner in such games is $\PSPACE$-complete, although it is fixed-parameter tractable with the number of reachability objectives as parameter. Moreover, we consider the memory requirements for both players and give matching upper and lower bounds on the size of winning strategies. In order to allow more efficient algorithms, we consider subclasses of generalized reachability…

On the Complexity of Reachability in Parametric Markov Decision Processes

This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably p…

按几何维度参数化的带状态向量加法系统的可达性

Reachability in Vector Addition System with States Parameterized by Geometric Dimension

本文从几何维度视角研究带状态向量加法系统（VASS）的可达性问题，通过扩展泵引理技术，证明几何1维和2维VASS的可达性问题均为PSPACE完全。

The Complexity of Reachability Problems for Flat Counter Machines with Periodic Loops

This paper proves the NP-completeness of the reachability problem for the class of flat counter machines with difference bounds and, more generally, octagonal relations, labeling the transitions on the loops. The proof is based on the fact that the sequence of powers $\{R^i\}_{i=1}^\infty$ of such relations can be encoded as a periodic sequence of matrices, and that both the prefix and the period of this sequence are $2^{\mathcal{O}(\bin{R})}$ in the size of the binary encoding $\bin{R}$ of a relation $R$. This result allows to characterize the complexity of the reachability problem for one of…

Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free

Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extens…

The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes

We study the never-worse relation (NWR) for Markov decision processes with an infinite-horizon reachability objective. A state q is never worse than a state p if the maximal probability of reaching the target set of states from p is at most the same value from q, regard- less of the probabilities labelling the transitions. Extremal-probability states, end components, and essential states are all special cases of the equivalence relation induced by the NWR. Using the NWR, states in the same equivalence class can be collapsed. Then, actions leading to sub- optimal states can be removed. We show …

On parametrized verification of asynchronous, shared-memory pushdown systems

We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdar'13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar'15]. We show here that the liveness problem is PSPACE-complete. We also introduce the universal reachability problem. We show that it is decidable, and coNEXPTIME-complete. Finally, using these results, we prove that the verifying regular properties of traces of executions,…

带重置的无环Petri网与工作流网

Acyclic Petri and Workflow Nets with Resets

本文提出两类带重置的无环Petri网新子类，证明其可覆盖性或可达性问题复杂度从Ackermann难/不可判定降至PSPACE完全，为相关问题求解提供了可处理的网类。

三维向量加法系统可达性问题属于指数空间

3-VASS Reachability is in EXPSPACE

研究三维向量加法系统可达性问题的复杂度，通过分层可泵性分析，证明该问题属于指数空间，此前已知算法是非初等的，此研究给出新结论。

定量可达性博弈中子博弈完美均衡的复杂性

The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

本文研究定量可达性博弈中SPE的复杂性，证明约束存在性问题是PSPACE完全的，并提出一种通过迭代约束至不动点来刻画SPE结果集的新算法。

固定维度连续VASS的可达性

Reachability in Fixed-Dimensional Continuous VASS

研究固定维度连续向量加法系统（CVASS）的可达性和覆盖性问题，在有理数和整数转移向量下，证明维度1时问题属于AC^1，维度≥2时NP完全。

Senescent Ground Tree Rewrite Systems

Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scope-bounded multi-stack pushdown systems, we show --- via reductions to and from reset Petri-nets --- that these systems have a…

带状态向量加法系统中的 monus 语义

Monus semantics in vector addition systems with states

研究了带状态向量加法系统（VASS）的 monus 过近似语义，允许递减零值计数器，证明全程使用该语义时可达性保持可判定，并全面刻画了可达性、零可达性和覆盖性问题的复杂度。

完成循环：具有表达力循环引用的可达性类型（扩展版）

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)

本文扩展 Reachability Types，引入循环引用、浅层限定符追踪和带引用子类型的逃逸规则，在 $\mathsf{F}_{<:}^{\circ}$-演算中证明类型可靠性并展示更强表达力。

Reachability in Augmented Interval Markov Chains

In this paper we propose augmented interval Markov chains (AIMCs): a generalisation of the familiar interval Markov chains (IMCs) where uncertain transition probabilities are in addition allowed to depend on one another. This new model preserves the flexibility afforded by IMCs for describing stochastic systems where the parameters are unclear, for example due to measurement error, but also allows us to specify transitions with probabilities known to be identical, thereby lending further expressivity. The focus of this paper is reachability in AIMCs. We study the qualitative, exact quantitativ…

向量加法系统中可达性的新下界

New Lower Bounds for Reachability in Vector Addition Systems

研究向量加法系统及其带下推栈扩展的可达性问题的维度参数复杂度，提出新构造将VASS的F_k-难度下界降至维度2k+3，并首次为下推VASS建立维度k/2+4的F_k-难度下界，表明其复杂度可能高于VASS。