Decidability and Complexity Borders of Reachability Problems

In the area of infinite-state systems, there is a wide variety of automata models that feature finitely many control states and have access to some “storage mechanism”. Examples include pushdown systems (which have access to a stack), vector addition systems with states (which feature $\mathbb{N}$-valued counters), counter systems (which have a counters that can be zero-tested), and so on. Given the ubiquitous nature of the reachability problem, there has been a significant amount of work that aims to understand for which of these storage mechanisms the reachability problem is decidable.

A similar situation exists in Computational Group Theory: One considers an infinite structure (infinite groups, resp. a storage mechanism) and investigates whether a particular decision problem permits an algorithm. This is because many decision problem in group theory can be considered for each infinite group. As above, this raises the question for which groups a particular problem is decidable.

In fact, in group theory, there is a long tradition of providing algebraic (or structural) descriptions of those groups for which a particular problem is decidable. A prominent example is the Boone-Higman Theorem [6, Theorem I]. It concerns the word problem of a finitely generated group, which asks whether two given sequences of generators multiply up to the same element. The theorem states that this is decidable for precisely those finitely generated groups that can be embedded in a simple group that in turn embeds into a finitely presented group. Here, informally, finitely presented means “described by finitely many equations”.

The line of work outlined here applies the same spirit to infinite-state systems: Can we somehow structurally characterize those storage mechanisms for which a particular decision problem (here: reachability) is decidable? Obtaining such results requires describing storage mechanisms as mathematical structures, so that we can then characterize those structures that permit decidability.

We shall discuss the framework of valence systems over graph monoids (introduced in [33, 31]). Informally, these are automata consisting of finitely many control states that have access to some storage mechanism, and the storage mechanism itself is described by a finite (undirected) graph (with self-loops allowed). Then, for certain graphs, one obtains automata with a pushdown, with others one obtains automata with counters, etc. It should be noted that there are other results in the same spirit in the infinite-state area, such as for asynchronous programs [23] or affine vector addition systems with integer [5] or continuous counters [3]. Moreover, there is of course a rich variety of sufficient conditions on infinite-state systems for certain reachability problems being decidable, most prominently the well-structured transition systems [1, 12].

Formally, a graph is a pair $\mathrm{\Gamma }=(V,E)$ where $V$ is a finite set of vertices and $E\subseteq \{S\subseteq V\mid |S|\le 2\}$ is its set of edges. Here, a singleton $\{a\}\in E$ for $a\in V$ means that $a$ has a self-loop, in which case $a$ is called looped. A clique is a set of pairwise adjacent vertices. In an independent set, all vertices are pairwise non-adjacent. An induced subgraph of $\mathrm{\Gamma }$ is a graph $(V^{\prime },E^{\prime })$, where $V^{\prime }\subseteq V$ and also $E^{\prime }=\{S\in E\mid S\subseteq V^{\prime }\}$, i.e. among its vertices, ${\mathrm{\Gamma }}^{\prime }$ has precisely those edges that appear in $\mathrm{\Gamma }$. If there is no danger of confusion, we also call a graph $\mathrm{\Delta }$ induced subgraph of $\mathrm{\Gamma }$ if $\mathrm{\Delta }$ is isomorphic to an induced subgraph of $\mathrm{\Gamma }$.

To each graph $\mathrm{\Gamma }$, we associate the alphabet $\mathrm{\Sigma }=V\cup \overline{V}$, where $\overline{V}=\{\overline{a}\mid a\in V\}$ contains decorated versions of the letters in $V$. On ${\mathrm{\Sigma }}^{\ast }$, the set of words over $\mathrm{\Sigma }$, we consider the smallest congruence ${\equiv }_{\mathrm{\Gamma }}$ that satisfies:

Here, $a=b$ is allowed, meaning if $a$ is looped, then $\overline{a}a{\equiv }_{\mathrm{\Gamma }}a\overline{a}{\equiv }_{\mathrm{\Gamma }}\epsilon$. The congruence gives rise to a monoid, which is a set $M$ together with an associative operation and a neutral element $1\in M$. Specifically, we have the monoid ${𝕄}_{\mathrm{\Gamma }}:={\mathrm{\Sigma }}^{\ast }/{\equiv }_{\mathrm{\Gamma }}$. For a word $w\in {\mathrm{\Sigma }}^{\ast }$, we use $[w]$ to denote the congruence class of $w$.

A valence system over a graph $\mathrm{\Gamma }$ is a tuple $𝒜=(Q,\delta )$, where $Q$ is a finite set of states, $\delta \subseteq Q\times \mathrm{\Sigma }\ast \times Q$ is a finite set of transitions, and $q_0\in Q$ is its initial state, in which $\mathrm{\Sigma }$ is the alphabet associated with $\mathrm{\Gamma }$.

A configuration is a pair $(q,x)\in Q\times {𝕄}_{\mathrm{\Gamma }}$. For two configurations $(p,x),(q,y)\in Q\times {𝕄}_{\mathrm{\Gamma }}$, we write $(p,x)\to (q,y)$ if there is a transition $(p,z,q)\in \delta$ such that $y=xz$. In other words, the edges of a valence system contain elements of the monoid ${𝕄}_{\mathrm{\Gamma }}$, and taking a transition $(p,z,q)$ means we move from state $p$ to state $q$ and we multiply the effect $z$ with the element in the previous configuration. By $\stackrel{\ast }{\to }$, we denote the reflexive, transitive closure of $\to$.

The reachability problem for valence systems over $\mathrm{\Gamma }$ is the following:

Given

A valence system $𝒜=(Q,\delta )$ over $\mathrm{\Gamma }$, together with states $p,q\in Q$.

Question

Does $(p,1)\stackrel{\ast }{\to }(q,1)$?

We denote this decision problem by $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\mathrm{\Gamma })$. Note that here, $1\in {𝕄}_{\mathrm{\Gamma }}$ is the neutral element of ${𝕄}_{\mathrm{\Gamma }}$, which equals $[\epsilon ]$, the congruence class of the empty word $\epsilon \in {\mathrm{\Sigma }}^{\ast }$.

To illustrate the definition, let us see some examples. First, suppose $\mathrm{\Gamma }=(V,E)$ has no edges at all, such as in Figure 1(a). Then the only relations induced by Equations 1 and 2 are $a\overline{a}\equiv \epsilon$ for every $a\in V$. This means, a word $w\in {\mathrm{\Sigma }}^{\ast }$ has $w\equiv \epsilon$ if and only if $w$ can be transformed into the empty word by deleting factors $a\overline{a}$, $a\in V$. This means, we have $w\equiv \epsilon$ if and only if $w$ belongs to the Dyck language; in other words, viewing $a$’s as opening brackets and $\overline{a}$ as $a$’s matching closing bracket, we have $w\equiv \epsilon$ if and only if $w$ is a well-bracketed expression. Put in yet another way, if we interpret $a$ as “push an $a$” and $\overline{a}$ as “pop an $a$”, then $w\equiv \epsilon$ if and only if the sequence $w$ is a valid sequence of instructions of a pushdown that leads from the empty stack to the empty stack. Therefore, valence systems over independent graphs are equivalent to pushdown systems.

Now suppose $\mathrm{\Gamma }=(V,E)$ is a clique, meaning we have $\{a,b\}\in E$ if and only if $a\ne b$ for $a,b\in V$, such as in Figure 1(b). We can then argue as above that a word $w\in {\{a,\overline{a}\}}^{\ast }$ will satisfy $w\equiv \epsilon$ if and only if $w$ is well-bracketed, but over a single pair of brackets. Equivalently, we have $w\equiv \epsilon$ if and only if every prefix $u$ of $w$ has ${|u|}_a\ge {|u|}_{\overline{a}}$ and we also have ${|w|}_a={|w|}_{\overline{a}}$. Hence, if $|V|=1$, then valence systems over $\mathrm{\Gamma }$ are just systems with a single counter that (i) can be incremented and decremented and (ii) can never go below zero. Moreover, the reachability problem asks whether we can go from counter-value-zero to counter-value-zero. If $|V|>1$, then notice that Equation 2 allows us to commute any two letters that stem from distinct vertices. Therefore, for $w\in {\mathrm{\Sigma }}^{\ast }$, we have $w\equiv \epsilon$ if and only if, projecting to each subalphabet $\{b,\overline{b}\}$ for $b\in V$, leads to a well-bracketed word over $\{b,\overline{b}\}$. Thus, valence systems over $\mathrm{\Gamma }$ can be viewed as automata over $|\mathrm{\Gamma }|$-many $\mathbb{N}$-counters as above, i.e. which cannot go below zero. Such systems are also called vector addition systems with states (VASS) [11].

If $\mathrm{\Gamma }=(V,E)$ is a clique with self-loops everywhere, such as in Figure 1(c), then one can see that $w\equiv \epsilon$ if and only if ${|w|}_a={|w|}_{\overline{a}}$ for every $a\in V$. Hence, valence systems over $\mathrm{\Gamma }$ are automata with $\mathbb{Z}$-counters, i.e. ones that can go below zero. These are also known as integer VASS [17] or automata with blind counters [14].

With similar arguments, one can observe that if $\mathrm{\Gamma }$ is the graph in Figure 1(d), then valence systems over $\mathrm{\Gamma }$ correspond to automata with access to two separate stacks, for which the reachability problem is well-known to be undecidable.

Finally, with $\mathrm{\Gamma }$ being the graph in Figure 1(e), valence systems over $\mathrm{\Gamma }$ are equivalent (in terms of reachability) to automata with one pushdown and two $\mathbb{N}$-counters. Such systems are usually called pushdown vector addition systems with states (PVASS), and the number of $\mathbb{N}$-counters is called their dimension.

Among those $\mathrm{\Gamma }$ where every vertex has a self-loop, it is well-understood which $\mathrm{\Gamma }$ have a decidable $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\mathrm{\Gamma })$. Note that in the presence of self-loops everywhere, the monoid ${𝕄}_{\mathrm{\Gamma }}$ is actually a group. Groups that arise in this way are also called graph groups or right-angled Artin groups. They are a prominent class in group theory, which motivated Lohrey and Steinberg to study $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\mathrm{\Gamma })$, which in this context is called the rational subset membership problem for the group ${𝕄}_{\mathrm{\Gamma }}$. A graph $\mathrm{\Gamma }=(V,E)$ is a transitive forest if it is obtained from a forest (i.e. a graph without cycles, but where self-loops are allowed) by (i) picking a root node in each tree of the forest and (ii) adding edges between any two nodes that lie on a path from the root to a leaf. Remarkably, Lohrey and Steinberg obtained the following complete characterization in the case of graph groups [22, Theorem 2]:

In the decidable cases, the complexity was described in [18].

However, when we move beyond the case of groups, the algorithmic methods of [22, 18] are not applicable anymore. The latter approaches exploit semilinearity of Parikh images (in the case of looped transitive forests), which already fails for . In fact, for many concrete graphs $\mathrm{\Gamma }$, it remains open whether $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\mathrm{\Gamma })$ is decidable. Specifically, for PVASS, decidability was a long-standing open problem and only settled very recently, first in dimension one by Bizière and Czerwiński [4], and then in arbitrary dimension by Guttenberg, Keskin, and Meyer [16].

However, among those $\mathrm{\Gamma }$ that in some sense “avoid PVASS”, a full characterization is again available. Let us make this precise. It is not difficult to see that for the following three graphs $\mathrm{\Gamma }$:

the problem $\mathrm{𝖱𝖾𝖺𝖼𝗁}(\mathrm{\Gamma })$ is equivalent to reachability in one-dimensional PVASS. We therefore say that a graph $\mathrm{\Gamma }$ is PVASS-free if it has none of the three graphs in Equation 3 as an induced subgraph. Then, for PVASS-free graphs, the equivalence of Lohrey and Steinberg continues to hold [34, Theorem 3.3]:

Here, the algorithm for the decidable reachability reduces to reachability in VASS with nested zero tests [27, 15]. These have $d$-many $\mathbb{N}$-counters, for some $d\ge 0$, and for each $k\in \{1,\mathrm{\dots },d\}$, they have an instruction that tests all counters $1,\mathrm{\dots },k$ for zero.

Beyond the PVASS-free graphs, there still remains an infinite hierarchy of graphs $\mathrm{\Gamma }$ that are not covered by Theorem 1.2. Let us describe this hierarchy in terms of the concrete storage mechanisms that correspond to it. At the lowest level, this hierarchy consists of PVASS, for which decidability is now established [4, 16]. The next level is obtained by building stacks: Here, the storage content consists of a stack where instead of individual letters, we can store PVASS configurations, i.e. a stack and values of $\mathbb{N}$-counters. After building stacks, the next level is obtained by adding $\mathbb{N}$-counters: We introduce new, separate counters that can be used independently of the “stack of PVASS”. Then, the levels of our hierarchy are obtained by alternating building stacks and adding $\mathbb{N}$-counters.

Given that the first level of this hierarchy (namely, PVASS) is known to be decidable, we conjecture that decidability holds for all levels. This is equivalent to the following:

More information on various types of reachability problems in connection with valence systems can be found in the survey [35].

Valence systems over graph monoids have been studied from various other angles, such as first-order logic on configuration graphs [10] finite-state abstractions and unboundedness problems [2, 32, 7], expressiveness of silent transitions [31], games [25, 28], and overapproximations [13] and underapproximations [24, 30] of the reachability relation.

Formally, we consider systems of the form $𝒜=(Q,\delta )$, where $Q$ is a finite set of control states and $\delta \subseteq Q\times \mathbb{Z}\times Q$ is a finite set of transitions. Importantly, the numbers on the transitions are encoded in binary. A configuration is a pair $(q,x)\in Q\times \mathbb{Z}$. For configurations $(p,x),(q,y)\in Q\times \mathbb{Z}$, we write $(p,x)\to (q,y)$ if there is a transition $(p,z,q)\in \delta$ with $y=x+z$. Then, $\stackrel{\ast }{\to }$ is the reflexive, transitive closure of $\to$.

In the classical reachability problem, we are given states $q_0,q_1\in Q$ and a target $t\in \mathbb{Z}$, and we want to know whether $(q_0,0)\stackrel{\ast }{\to }(q_1,t)$. This is clearly $\mathrm{𝖭𝖯}$-complete, where hardness directly follows from subset sum.

To put the settings of (i) “reaching an exact configuration” and (ii) “covering a configuration” in a general framework, we rely on Presburger arithmetic. The idea is that, for (i), we are given $t\in \mathbb{Z}$ and we want to reach $(q_1,x)$ with $x=t$. For (ii), however, we are also given $t$, but we want to reach $(q_1,x)$ such that $x\ge t$. The idea of the framework is to generalize these two relationships, “$x=t$” and “$x\ge t$”, by a formula in Presburger arithmetic, the first-order theory of the structure $(\mathbb{Z};+,\le ,0,1)$.

This means, our setting consists of a Presburger formula $\phi$ with $p+1$ free variables. Moreover, instead of having as input a single number $t$, we have as input a vector $𝒕\in {\mathbb{Z}}^p$. Instead of defining the problem with the Presburger formula, it will be more convenient to talk about the set $S\subseteq {\mathbb{Z}}^{p+1}$ of vectors satisfying $\phi$. Sets obtained in this way are called Presburger-definable. For such a set, we define

i.e. the set of admissible target numbers for the parameter vector $𝒕\in {\mathbb{Z}}^p$. Thus, for each Presburger-definable set $S\subseteq {\mathbb{Z}}^{p+1}$, we consider the following problem, denoted $\mathrm{𝖱𝖾𝖺𝖼𝗁}(S)$:

Given

A system $𝒜=(Q,\delta )$ with one integer counter, states $q_0,q_1\in Q$, and a vector $𝒕\in {\mathbb{Z}}^p$.

Question

Is there a number $x\in \mathbb{Z}$ such that $(q_0,0)\stackrel{\ast }{\to }(q_1,x)$ and $x\in S[𝒕]$?

Then, if $p=1$ and $S=\{(t,x)\mid x=t\}$, then $\mathrm{𝖱𝖾𝖺𝖼𝗁}(S)$ is the classical reachability problem. However, if $S=\{(t,x)\mid x\ge t\}$, then $\mathrm{𝖱𝖾𝖺𝖼𝗁}(S)$ is the coverability problem. Another example is the set

For this set $R\subseteq {\mathbb{Z}}^{1+1}$, it is not immediately obvious whether $\mathrm{𝖱𝖾𝖺𝖼𝗁}(R)$ can be decided in polynomial time or whether it is $\mathrm{𝖭𝖯}$-hard.

It is well-known that the coverability problem is solvable in polynomial time, and even in the circuit complexity class ${\mathrm{𝖠𝖢}}^1$ (see, e.g. the remarks after [8, Corollary 4.9]). However, as mentioned above, the classical reachability problem is $\mathrm{𝖭𝖯}$-complete. Therefore here, we are interested in the question: For which sets $S$ is $\mathrm{𝖱𝖾𝖺𝖼𝗁}(S)$ in polynomial time?

Perhaps surprisingly, the complexity of $\mathrm{𝖱𝖾𝖺𝖼𝗁}(S)$ is determined by a particular density measure of $S$, which we define now. For a subset $A\subseteq \mathbb{Z}$ and $k\in \mathbb{N}$, we define the $k$-density of $A$ at point $x\in \mathbb{Z}$ as

Thus, $D_1(A,x)$ is the infimum of the probabilities of hitting $A$ when choosing points in intervals centered at $x$. And $D_k(A,x)$ is the variant where instead of intervals, we consider arithmetic progressions with period $k$, radiating outward from $x$.

For $A\ne \mathrm{\varnothing }$ as a whole, we define its local density $D(A)$ as

More generally, for a subset $S\subseteq {\mathbb{Z}}^{p+1}$, we define its local density $D(S)$ as

Thus intuitively, $D(S[𝒕])$ is a measure for how isolated the points in $S[𝒕]$ are, within arithmetic progressions. Moreover, $D(S)$ measures how much one can drive up isolation by choosing suitable $𝒕\in {\mathbb{Z}}^p$.

The following result, shown in [29, Theorem III.2] shows that the above measure of density characterizes those sets $S$ for which $\mathrm{𝖱𝖾𝖺𝖼𝗁}(S)$ is in polynomial time, resp. $\mathrm{𝖭𝖯}$-complete.

For example, consider the set $R$ from (4). Then $D_k(R[t],x)\ge \frac{1}{4}$ for any $x\in R[t]$: The lowest density is attained at $x=2t$, where we get $D_k(R[t],2t)\ge \frac{1}{4}$. Hence, we have $D(R)\ge \frac{1}{4}$, meaning Theorem 2.1 tells us that $\mathrm{𝖱𝖾𝖺𝖼𝗁}(R)$ is in ${\mathrm{𝖠𝖢}}^1$, and in particular in polynomial time.

The paper [29] also contains analogous results for systems where (i) all updates have to be natural numbers [29, Theorem III.9] or (ii) the updates are integers, but a run must stay within the natural numbers [29, Theorem III.13].