On the Reachability Problem for Two-Dimensional Branching VASS

Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there exists a run from an initial configuration to a final one. This problem was shown decidable more than forty years ago [26] but its precise complexity was only established a few years ago [23, 9, 22]. Several VASS extensions have been introduced and studied, most notably unordered data nets [20], pushdown VASS [1, 19], and branching VASS [10, 31]. But so far, the reachability problem is still open for these models.

One of the first subclasses of VASS for which reachability was shown to be decidable is the class of $2$-dimensional VASS. For this class, Hopcroft and Pansiot devised an algorithm that computes a finite description (more precisely, a semilinear presentation) of the reachability set [16]. As an immediate consequence, they obtained that reachability is decidable for this class. In fact, the algorithm of Hopcroft and Pansiot can be viewed as a refinement of the classical Karp-Miller algorithm [18] where the abstract pumping of cycles (putting $\omega$ in some components) is replaced by an exact acceleration of cycles (adding new vectors to the current set of periods).

In this paper, we investigate the reachability problem for branching VASS (shortly called BVASS in the sequel), a branching generalization of VASS. More precisely, BVASS extend VASS with special branching transitions that merge configurations (by summing their vectors). This model has gained a lot of interest recently due to strong links with several fields in computer science such as cryptographic protocols [31], linear logic [10, 21], recursively parallel programs [5], timed pushdown systems [7], computational linguistic [29, 30], game semantics [8], equational tree automata [28, 25] and data logics [17, 4]. For instance, provability in the multiplicative exponential fragment of linear logic (MELL) is inter-reducible with the reachability problem in BVASS [10]. As mentioned before, the reachability problem is still open in arbitrary dimension for BVASS. In dimension one, the reachability problem is decidable and the exact complexity is known [15, 12]. The objective of our work was to investigate the decidability of the reachability problem for $2$-dimensional BVASS.

We denote by $\mathbb{Z}$ the set of integers, $\mathbb{N}$ the set of natural numbers, by $\mathbb{Q}$ the set of rational numbers, and by ${\mathbb{Q}}_{\ge 0}$ the set of non-negative rational numbers. We also introduce ${\mathbb{N}}_{>0}$ and ${\mathbb{Q}}_{>0}$ defined as $\mathbb{N}\setminus \{0\}$ and ${\mathbb{Q}}_{\ge 0}\setminus \{0\}$, respectively. The powerset of a set $S$ is written $\mathbb{P}(S)$.

A $d$-dimensional branching vector addition system with states ($d$-BVASS for short) is a pair $ℬ=(Q,\mathrm{\Delta })$ where $Q$ is a finite non-empty set of states and $\mathrm{\Delta }\subseteq (\mathbb{P}(Q)\times {\mathbb{Z}}^d\times Q)$ is a finite set of transition rules. A transition rule $\delta =(S,𝐚,q)$ in $\mathrm{\Delta }$ consists in a set $S\subseteq Q$ of input states, a displacement $𝐚\in {\mathbb{Z}}^d$, and a single output state $q\in Q$. Intuitively, assuming that $S=\{q_1,\mathrm{\dots },q_k\}$, this transition rule can be seen as the rewriting rule $q_1({𝚡}_1),\mathrm{\dots },q_k({𝚡}_k)\to q(𝐚+{𝚡}_1+\mathrm{\cdots }+{𝚡}_k)$ with formal parameters ${𝚡}_1,\mathrm{\dots },{𝚡}_k$. Note that our definition forbids a state from occurring twice on the left-hand side of a transition rule (as this left-hand side is given by a set of states). This restriction is only a matter of technical convenience. A transition rule $\delta =(S,𝐚,q)$ is called initial when $S=\mathrm{\varnothing }$, unary when $|S|=1$, and branching when $|S|\ge 2$. A $d$-dimensional vector addition system with states ($d$-VASS for short) is a $d$-BVASS $𝒱=(Q,\mathrm{\Delta })$ such that $|S|\le 1$ for every transition rule $(S,𝐚,q)$ in $\mathrm{\Delta }$.

We formulate the semantics of a $d$-BVASS $ℬ=(Q,\mathrm{\Delta })$ in terms of a configuration-set transformer $\mathrm{Post}$. A configuration of $ℬ$ is a pair $(q,𝐱)$ in $Q\times {\mathbb{N}}^d$, also written as $q(𝐱)$ in the sequel. By extension, given a set $𝐗\subseteq {\mathbb{N}}^d$, we let $q(𝐗)$ denote the set of configurations $\{q\}\times 𝐗$. The set of initial configurations of $ℬ$ is $\{q(𝐚)\mid (\mathrm{\varnothing },𝐚,q)\in \mathrm{\Delta }\text{ and }𝐚\ge \mathrm{𝟎}\}$. For each transition rule $\delta =(S,𝐚,q)$ in $\mathrm{\Delta }$, we define the function ${\mathrm{Post}}_{\delta }:\mathbb{P}(Q\times {\mathbb{N}}^d)\to \mathbb{P}(Q\times {\mathbb{N}}^d)$ by¹¹1We use double braces $\{\{\mathrm{\cdots }\}\}$ to denote multisets. Here, the condition $S=\{\{r\mid r(𝐳)\in D\}\}$ means that, firstly, the set $S$ is equal to the set $\{r\mid r(𝐳)\in D\}$, and, secondly, $r_1\ne r_2$ for every two distinct configurations $r_1({𝐳}_1),r_2({𝐳}_2)$ in $D$.

for every set $C\subseteq Q\times {\mathbb{N}}^d$. We also introduce ${\mathrm{Post}}_{ℬ}:\mathbb{P}(Q\times {\mathbb{N}}^d)\to \mathbb{P}(Q\times {\mathbb{N}}^d)$, defined by ${\mathrm{Post}}_{ℬ}(C)={\bigcup }_{\delta \in \mathrm{\Delta }}{\mathrm{Post}}_{\delta }(C)$. Note that ${\mathrm{Post}}_{ℬ}$ is $\subseteq$-nondecreasing and that ${\mathrm{Post}}_{ℬ}(\mathrm{\varnothing })$ coincides with the set of initial configurations of $ℬ$. The reachability set of $ℬ$, written $⟦ℬ⟧$, is the $\subseteq$-least set $C\subseteq Q\times {\mathbb{N}}^d$ such that ${\mathrm{Post}}_{ℬ}(C)\subseteq C$.

A set of configurations $C\subseteq Q\times {\mathbb{N}}^d$ is said to be semilinear if $C$ is a finite union of sets of the form $q(𝐋)$ where $q\in Q$ and $𝐋\subseteq {\mathbb{N}}^d$ is linear, i.e. a set of the form $𝐛+\mathrm{Per}(𝐀)$ for some $𝐛\in {\mathbb{N}}^d$ and some finite subset $𝐀$ of ${\mathbb{N}}^d$. A presentation of a semilinear set of configurations $C\subseteq Q\times {\mathbb{N}}^d$ is a finite set $\{(q_1,{𝐛}_1,{𝐀}_1),\mathrm{\dots },(q_k,{𝐛}_k,{𝐀}_k)\}$, where $q_j\in Q$, ${𝐛}_j\in {\mathbb{N}}^d$, and ${𝐀}_j$ is a finite subset of ${\mathbb{N}}^d$, such that $C={\bigcup }_{j=1}^k{q}_j({𝐛}_j+\mathrm{Per}({𝐀}_j))$. The main contribution of this paper is the generalization to $2$-BVASS of the following theorem.

In order to generalize Theorem 3.2 to 2-BVASS, we will extend to BVASS some techniques developed for classical VASS. A linear (i.e., non-branching) view of BVASS behaviors is required to do so. Intuitively, this view is obtained by instantiating transition rules $\delta =(S,𝐚,q)$ with $|S|\ge 2$ into unary transition rules. This instantiation can be performed at the semantic level or at the syntactic level. Let us make these ideas more concrete. We assume that $ℬ=(Q,\mathrm{\Delta })$ is a $d$-BVASS for the remainder of this section.

For each transition rule $\delta =(S,𝐚,q)$ in $\mathrm{\Delta }$, we introduce the binary relation $\stackrel{𝛿}{\Rightarrow }$ on $Q\times {\mathbb{N}}^d$ defined as the set of pairs $(p(𝐱),q(𝐲))\in {(Q\times {\mathbb{N}}^d)}^2$ such that $p\in S$ and there exists a set $D\subseteq ⟦ℬ⟧$ verifying $(S\setminus \{p\})=\{\{r\mid r(𝐳)\in D\}\}$ and $𝐲=𝐚+𝐱+{\sum }_{r(𝐳)\in D}𝐳$. The binary relation $\stackrel{𝛿}{\Rightarrow }$ instantiates the transition rule $\delta$ at the semantic level as it relies on the reachability set $⟦ℬ⟧$ of $ℬ$. We also introduce the binary step relation $\stackrel{}{\Rightarrow }$ on $Q\times {\mathbb{N}}^d$ defined as the union ${\bigcup }_{\delta \in \mathrm{\Delta }}\stackrel{𝛿}{\Rightarrow }$. The reflexive-transitive closure of $\stackrel{}{\Rightarrow }$ is denoted by $\stackrel{\ast }{\Rightarrow }$. It is readily seen that $\stackrel{}{\Rightarrow }$ and $\stackrel{\ast }{\Rightarrow }$ are diagonal.²²2 A binary relation $\bowtie$ on $Q\times {\mathbb{N}}^d$ is called diagonal if $p(𝐱)\bowtie q(𝐲)$ implies $p(𝐱+𝐮)\bowtie q(𝐲+𝐮)$, for every configurations $p(𝐱),q(𝐲)\in Q\times {\mathbb{N}}^d$ and vector $𝐮\in {\mathbb{N}}^d$. Using square brackets to denote relational images³³3Given a binary relation $\bowtie$ on a set $S$ and a subset $X$ of $S$, we let $\bowtie [X]$ denote the relational image of $X$ under $\bowtie$, defined by $\bowtie [X]=\{y\in S\mid \exists x\in X:x\bowtie y\}$. , we have ${\mathrm{Post}}_{ℬ}(C)\subseteq \stackrel{}{\Rightarrow }[C]\subseteq \stackrel{\ast }{\Rightarrow }[C]\subseteq ⟦ℬ⟧$ for every set of configurations $C\subseteq ⟦ℬ⟧$.

Let us now instantiate transition rules at the syntactic level. Given a finite set $F\subseteq Q\times {\mathbb{N}}^d$, the instantiation of $ℬ$ with $F$, written $ℬ⟨F⟩$, is the $d$-VASS $ℬ⟨F⟩=(Q,{\mathrm{\Delta }}^{\prime })$ where ${\mathrm{\Delta }}^{\prime }$ is the set of triples $(\{p\},{𝐚}^{\prime },q)$ such that there exist a transition rule $(S,𝐚,q)\in \mathrm{\Delta }$ with $p\in S$ and a set $D\subseteq F$ verifying $(S\setminus \{p\})=\{\{r\mid r(𝐳)\in D\}\}$ and ${𝐚}^{\prime }=𝐚+{\sum }_{r(𝐳)\in D}𝐳$. We observe that if $F\subseteq ⟦ℬ⟧$ then the step relation of $ℬ⟨F⟩$ is contained in the step relation of $ℬ$.

We conclude this section with notions that are specific to classical VASS. Consider a $d$-VASS $𝒱=(Q,\mathrm{\Delta })$. From now on, unary transition rules $(\{p\},𝐚,q)\in \mathrm{\Delta }$ will be written $(p,𝐚,q)$ for short. A path of $𝒱$ is a non-empty sequence $\theta =(p_1,{𝐚}_1,q_1)\mathrm{\cdots }(p_k,{𝐚}_k,q_k)$ of unary transition rules $(p_i,{𝐚}_i,q_i)\in \mathrm{\Delta }$ such that $q_i=p_{i+1}$ for all $i\in \{1,\mathrm{\dots },k-1\}$. Such a path $\theta$ is also shortly written $\theta =p_1\stackrel{{𝐚}_1}{\hookrightarrow }{q}_1\mathrm{\cdots }\stackrel{{𝐚}_k}{\hookrightarrow }{q}_k$. We call $p_1$ and $q_k$ the start and the end of $\theta$, respectively. The displacement of $\theta$ is ${\sum }_{i=1}^k{𝐚}_i$. We say that $\theta$ is a cycle if $p_1=q_k$. It is an elementary cycle if $p_1=q_k$ and $p_1,\mathrm{\dots },p_k$ are pairwise distinct.

We present in this section an algorithm to compute the reachability set for $2$-BVASS. More precisely, given a $2$-BVASS $ℬ$, our algorithm returns a finite exploration of $ℬ$ that is both sound and complete. We start by defining what we mean by sound and complete exploration.

Intuitively, the label $\lambda (n)=({𝐚}_n,q_n,{𝐳}_n,{𝐏}_n)$ of a node $n$ provides, firstly, the displacement ${𝐚}_n$ of the transition rule used to create $n$ (this will be made clear later on and can be ignored for now), and, secondly, the set of configurations $q_n({𝐳}_n+{𝐏}_n)$ associated with the node $n$. Recall that $⟦ℬ⟧$ denotes the reachability set of a $2$-BVASS $ℬ$. Similarly, we associate to an exploration $𝒢=(N,\to ,\lambda )$ of $ℬ$ the set of configurations $⟦𝒢⟧={\bigcup }_{n\in N}{q}_n({𝐳}_n+{𝐏}_n)$. We say that $𝒢$ is sound when $⟦𝒢⟧\subseteq ⟦ℬ⟧$ and that it is complete when $⟦𝒢⟧\supseteq ⟦ℬ⟧$. A node $n\in N$ is called redundant if there exists $s\in N$ verifying $s\stackrel{+}{\to }n$ and $q_n({𝐳}_n+{𝐏}_n)\subseteq q_s({𝐳}_s+{𝐏}_s)$. We say that $𝒢$ is non-redundant when every redundant node is a leaf.

As in Hopcroft and Pansiot’s algorithm for classical $2$-VASS [16], a crucial ingredient of our algorithm is the acceleration of cycles. The purpose of cycle acceleration is to make the periodic sets ${𝐏}_n$ grow. We will utilize three kinds of cycles. Consider an exploration $𝒢=(N,\to ,\lambda )$ of a $2$-BVASS $ℬ=(Q,\mathrm{\Delta })$. We associate to each node $n\in N$ the $2$-VASS ${𝒱}_n$ defined as the instantiation $ℬ⟨F⟩$ of $ℬ$ with the finite set of configurations $F=\{q_s({𝐳}_s)\mid s\in N,s\stackrel{+}{\to }n\}$. In particular, if $n$ is a source then ${𝒱}_n=ℬ⟨\mathrm{\varnothing }⟩=(Q,{\mathrm{\Delta }}^{\prime })$ where ${\mathrm{\Delta }}^{\prime }=\{(S,𝐚,q)\in \mathrm{\Delta }\mid |S|=1\}$ is the set of unary transition rules in $\mathrm{\Delta }$. We introduce three finite subsets of ${\mathbb{Z}}^2$, namely ${𝐄}_n$, ${𝐂}_n$ and ${\overline{𝐂}}_n$, that correspond to the three kinds of cycles mentioned above. Let us define $c=|Q|{\max }_{i\in \{1,2\}}{\max }_{(S,𝐚,q)\in \mathrm{\Delta }}-𝐚(i)$. We call $c$ the constant of iteration of $ℬ$. Observe that $c$ is the same constant as the one in ˜3.4.

• $\mathrm{■}$

  ${𝐄}_n$ is the set of vectors $𝐯\in {\mathbb{Z}}^2$ such that there exist an elementary cycle $\theta$ of ${𝒱}_n$ with displacement $𝐯$ and a node $s\in \mathrm{Anc}(n)$ verifying $q_s$ is the start of $\theta$, ${𝐳}_s\ge (c,c)$ and $s\ne n$ implies $𝐯\ge (0,0)$.

• $\mathrm{■}$

  ${𝐂}_n$ is the set of vectors $𝐯\in {\mathbb{Z}}^2$ such that there exists a node $s\in \mathrm{Anc}(n)$ verifying $q_s=q_n$, $𝐯={𝐳}_n-{𝐳}_s$, ${𝐳}_n\ngeqq (c,c)$ and ${𝐳}_s\ngeqq (c,c)$.

• $\mathrm{■}$

  ${\overline{𝐂}}_n$ is the set of vectors $𝐯\in {\mathbb{Z}}^2$ such that there exists a node $s\in \mathrm{Anc}(n)$ verifying $q_s=q_n$ and $𝐯={𝐳}_n-{𝐳}_s$.

Note that ${𝐂}_n\subseteq {\overline{𝐂}}_n$. We also introduce the finite set ${𝐈}_n$ defined by ${𝐈}_n={𝐄}_n\cup {\overline{𝐂}}_n$ if ${\sum }_{m\to n}{𝐏}_m=\{(0,0)\}$ and ${𝐈}_n={𝐄}_n\cup {𝐂}_n$ otherwise. Vectors in ${𝐄}_n$, ${𝐂}_n$, and ${𝐈}_n$ are respectively called $n$-elementary, $n$-consecutive and $n$-iterable.

Given a set $𝐈\subseteq {\mathbb{Z}}^2$ and a periodic set $𝐏\subseteq {\mathbb{N}}^2$, we introduce the periodic set ${\mathrm{Add}}_{𝐈}^{\ast }(𝐏)$ defined as the set of vectors $𝐩+{𝐯}_1+\mathrm{\cdots }+{𝐯}_k$ where $𝐩\in 𝐏$, $k\in \mathbb{N}$, and ${𝐯}_1,\mathrm{\dots },{𝐯}_k$ are vectors in $𝐈$ such that $𝐩+{𝐯}_1+\mathrm{\cdots }+{𝐯}_{\mathrm{\ell }}\ge (0,0)$ for every $\mathrm{\ell }\in \{1,\mathrm{\dots },k\}$.

This section is devoted to the partial correctness of our algorithm $\mathrm{𝙴𝚡𝚙𝚕𝚘𝚛𝚎}$ (see Algorithm 1). Its termination is much more involved and will be the subject of the next sections. We first refine the notion of exploration to account for the behavior of our algorithm.

Intuitively, Conditions 1 and 2 ensure that the exploration conforms to the semantics of $2$-BVASS. As hinted before, the vector ${𝐚}_n$ is the displacement of the transition rule leading to $n$ (see Condition 1). Notice these two conditions entail in particular that $q_n({𝐳}_n)$ is an initial configuration for every source $n$. Condition 3 corresponds to the previously-mentioned cycle acceleration step (see line 10 of Algorithm 1).

In the rest of this section, we show, firstly, that every algorithmic exploration is sound, and secondly, that our algorithm constructs explorations that are algorithmic and complete.

A graph $(N,\to )$ is called a forest if the edge relation $\to$ is well-founded (hence acyclic) and the set $\{m\in N\mid m\to n\}$ contains at most one node for every node $n\in N$. A forest is said to be finitely-branching if the set of source nodes is finite and the set $\{n\in N\mid m\to n\}$ is finite for every node $m\in N$. We say that a graph $𝒢=(N,\to )$ is spannable if there exists a subrelation ${\to }_{ℱ}$ of $\to$ such that $ℱ=(N,{\to }_{ℱ})$ is a finitely-branching forest. In that case, $ℱ$ is called a spanning forest of $𝒢$. Explorations ${\widehat{𝒢}}^{\sigma }$ built by algorithm $\mathrm{𝙴𝚡𝚙𝚕𝚘𝚛𝚎}(ℬ)$ are spannable. This property is obtained by observing that along the execution of the algorithm, new created nodes are connected, thanks to an edge that we call special, to a node that is removed from the worklist at that step. The spanning forest is then obtained by restricting the exploration to the special edges.

A branch $\beta$ of a forest $(N,{\to }_{ℱ})$ is an infinite sequence $\beta ={({\beta }_n)}_{n\in \mathbb{N}}$ of nodes such that ${\beta }_0$ is a source node of $ℱ$ and such that ${\beta }_i{\to }_{ℱ}{\beta }_{i+1}$ for every $i\ge 0$. Thanks to the Koenig’s lemma, we know that any infinite finitely-branching forest admits a branch. Such a branch can be seen as a witness of infinity of $ℱ$. We extend this notion of witnesses to infinite spannable graphs in a non-trivial way. Naturally, denoting by $ℱ$ a spanning forest of $𝒢$, any branch of $ℱ$ is a kind of witness of infinity of $𝒢$. However such a witness depends somehow on the choice of $ℱ$ and does not take into account the structure of $𝒢$.

Our “core” witness of infinity of an infinite spannable graph is defined thanks to the notion of primary and directed graphs. A graph $𝒢=(N,\to )$ is said to be primary if $N\setminus \mathrm{Des}(n)$ is finite for every node $n\in N$. A graph $𝒢=(N,\to )$ is said to be directed if for every $n,m\in N$, there exists $s\in N$ such that $n\stackrel{\ast }{\to }s$ and $m\stackrel{\ast }{\to }s$. The following lemma will be useful to extract from an infinite spannable graph a “core” subset of nodes that explain its infinity.