1 Introduction↩︎

1.0.0.1 Context.

Branching vector addition systems (BVAS) are a computational model for the distribution of additive resources through branching structures. The model can be traced back to the work of Rambow [1] in computational linguistics. To overcome the limitations of context-free grammars as a model of natural-language syntax, Rambow introduced multiset-valued linear index grammars (MV-LIG), in which nonterminals carry multisets of resources that are distributed among the children of a derivation node. When studying the language-emptiness problem for such grammars, the left-to-right order of derivation trees becomes irrelevant. The resulting abstraction is precisely a BVAS, and language emptiness can equivalently be viewed as a reachability problem.

A decade later, the same model was independently rediscovered in two seemingly unrelated contexts. Verma and Goubault-Larrecq [2] used BVAS to study a class of equational tree automata arising in the analysis of cryptographic protocols, obtaining decidability results for a lossy variant of the model. Around the same time, de Groote, Guillaume, and Salvati [3] proposed BVAS reachability as a natural automata-theoretic reformulation of provability in multiplicative exponential linear logic (MELL). In this setting, BVAS executions capture the flow of resources through proof trees.

Since then, BVAS and closely related models have appeared in a variety of areas of theoretical computer science, including logics over data trees [4]–[6], timed pushdown systems [7], verification of concurrent systems [8], and the semantics of higher-order functional languages [9].

Formally, a BVAS is a finite sequence \(\mathcal{B}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r)\) of finite subsets of \(\mathbb{Z}^d\). Each set \({\mathbf{\Delta}}_n\) in this sequence contains actions of arity \(n\). Intuitively, such an action \({\mathbf{v}} \in {\mathbf{\Delta}}_n\) may be viewed as the rewriting rule \(\mathtt{x}_1, \ldots, \mathtt{x}_n \rightarrow {\mathbf{v}} + \mathtt{x}_1 + \cdots + \mathtt{x}_n\) with formal parameters \(\mathtt{x}_1, \ldots, \mathtt{x}_n\). Configurations of \(\mathcal{B}\) are vectors in \(\mathbb{N}^d\), and executions are finite trees labeled by configurations in which every internal node is obtained by summing its \(n \ge 1\) children and adding an action from \({\mathbf{\Delta}}_n\). The reachability problem asks, given a BVAS, a target configuration and a finite set of initial configurations, whether there exists an execution with root labeled by the target and leaves labeled by initial configurations. The goal of this paper is to provide a solution to this long standing open problem.

1.0.0.2 Decidability of the VAS Reachability Problem.

Vector addition systems (VAS), or equivalently Petri nets, are obtained as the special case where \(r=1\). Executions then degenerate into sequences of configurations, and reachability asks whether a given target configuration can be obtained from an initial one by repeatedly applying additive actions from \({\mathbf{\Delta}}_1\).

VAS are a fundamental model for concurrency, and their reachability problem is one of the landmark decidability results in the theory of infinite-state systems. First posed in the late 1960s, it was shown decidable in the early 1980s through the works of Mayr [10] and Kosaraju [11]. The resulting proof was later refined by several authors, including Lambert [12], and became known as the KLM decomposition. Despite decades of subsequent work, the combinatorial principles underlying this decomposition remained only partially understood for a long time. One indication of this difficulty is that the first meaningful complexity upper bounds were obtained only much later [13] in 2015, culminating a few years later in the proof that VAS reachability is Ackermann-complete [14]–[16].

A conceptually different approach was introduced by Leroux in the 2010s [17], [18]. He showed that every unreachable configuration can be separated from the initial configurations by a semilinear (i.e., Presburger-definable) inductive invariant. Here, an inductive invariant is simply a set containing the initial configurations and closed under the actions of the VAS. This immediately yields a decision procedure by running in parallel one semi-algorithm enumerating executions and another enumerating semilinear sets until one is found to be an inductive invariant excluding the target.

1.0.0.3 Challenges of BVAS Reachability.

Despite these successes for VAS, the decidability of BVAS reachability has remained open for more than thirty years. Existing decidability and complexity results are restricted to small dimensions [19]–[22], to lossy variants of the model [2], [23]–[25], and to bounded counters [26]. At the same time, neither of the two classical approaches to VAS reachability appears to extend naturally to branching executions.

The KLM decomposition appears particularly difficult to generalize. Its original presentation relies on a delicate combinatorial analysis of linear executions, and its deeper structure only emerged through much later work on well-quasi-orderings and ideals [13]. At present, even the right formulation of a KLM-style decomposition for BVAS remains elusive.

The situation is yet more encouraging for the invariant-based approach. Leroux proved that VAS reachability sets enjoy strong geometric properties: they are almost semilinear and can therefore be closely approximated by semilinear sets. These properties were recently extended to BVAS [22]. Crucially, these approximations are only available from above: while VAS reachability sets admit semilinear overapproximations whose error has strictly smaller dimension, they do not admit analogous semilinear underapproximations in general.

Leroux circumvents this limitation by growing simultaneously two semilinear sets. The first one, denoted by \({\mathbf{S}}\), initially contains the initial configurations. The second one, denoted by \({\mathbf{T}}\), initially contains an unreachable target configuration that one wishes to exclude from the final invariant. Throughout the construction, no execution leads from a configuration in \({\mathbf{S}}\) to a configuration in \({\mathbf{T}}\). At each step, \({\mathbf{T}}\) is enlarged using the complement of a semilinear over-approximation of \(\operatorname{Post}^*_{}({\mathbf{S}})\), the set of configurations reachable from \({\mathbf{S}}\). Symmetrically, \({\mathbf{S}}\) is enlarged using the complement of a semilinear over-approximation of the backward reachability set \(\operatorname{Pre}^*_{}({\mathbf{T}})\), i.e., the set of configurations from which one can reach \({\mathbf{T}}\). The crucial observation is that \(\operatorname{Pre}^*_{}({\mathbf{T}})\) is itself a VAS reachability set, namely the reachability set of \({\mathbf{T}}\) in the VAS obtained by replacing each action with its opposite. Consequently, the same geometric machinery can be used to approximate both \(\operatorname{Post}^*_{}({\mathbf{S}})\) and \(\operatorname{Pre}^*_{}({\mathbf{T}})\).

This symmetry disappears in the branching setting, where there is no satisfactory analogue of backward reachability. More precisely, there is no operator \(\text{Pre}^*\) satisfying \[{\mathbf{S}} \cap \operatorname{Pre}^*_{}({\mathbf{T}}) \neq \emptyset \quad\Longleftrightarrow\quad \operatorname{Post}^*_{}({\mathbf{S}})\cap {\mathbf{T}} \neq \emptyset,\] since BVAS executions witnessing \(\operatorname{Post}^*_{}({\mathbf{S}})\cap {\mathbf{T}}\neq \emptyset\) may require several configurations from \({\mathbf{S}}\).

Thus, the first challenge in extending the inductive-invariant approach to BVAS is to construct the invariant using only forward reasoning, i.e., without relying on \(\text{Pre}^*\) or on a second set \({\mathbf{T}}\). Instead, one must grow a single set of configurations \({\mathbf{S}}\), while ensuring that it never contains the unreachable target, despite having access only to over-approximations. This is, however, not the only obstacle. The tree-shaped structure of BVAS executions introduces additional challenges compared to VAS. For instance, given two sets of configurations \({\mathbf{A}}_1\) and \({\mathbf{A}}_2\) that are each closed under the actions of a VAS, their union \({\mathbf{A}}_1 \cup {\mathbf{A}}_2\) is also closed. This property no longer holds for BVAS as branching executions may mix configurations from \({\mathbf{A}}_1\) and from \({\mathbf{A}}_2\).

1.0.0.4 Contributions.

We solve the reachability problem for BVAS through a novel forward-only invariant construction. Our approach relies on several new results and constructions:

• Our invariant is constructed iteratively. Starting from the empty set \({\mathbf{A}}\), we progressively add configurations until \({\mathbf{A}}\) becomes an inductive invariant. Throughout the construction, the set \({\mathbf{A}}\) excludes the unreachable target and is maintained as an attractor, a new notion related to inductive invariants that we introduce for BVAS to address the mix-approximation problem. An attractor is a set of configurations such that every execution with one leaf in the attractor and all other leaves in the attractor or reachable, has its root in the attractor. Inductive invariants are attractors, and attractors containing the initial configurations are inductive invariants. Moreover, the union of an attractor and the reachability set is an attractor.

• We introduce an abstract graph \(\mathcal{G}\) that captures executions outside the current attractor \({\mathbf{A}}\). Nodes of \(\mathcal{G}\) are pairs \((\rho,{\mathbf{C}})\) where \(\rho\) is an execution and \({\mathbf{C}}\) is a finitely-generated cone. The concretization of such a node is the set of executions larger than \(\rho\) (for a natural extension of the known well-quasi-order on VAS executions) that increase the target of \(\rho\) by a vector in \({\mathbf{C}}\). Edges of \(\mathcal{G}\) are defined by a standard \(\exists\exists\)-abstraction of the BVAS semantics. We use the abstract graph \(\mathcal{G}\) to extract semilinear approximations of the reachable configurations that avoid the mix-approximation problem. To do so, we impose an homogeneity condition that enforces the cone \({\mathbf{C}}\) of a node to only depend on its strongly connected component.

• We show that a part of the reachable configurations of a bottom strongly connected component \(\Gamma\) of \(\mathcal{G}\) can be captured by enlarging the attractor \({\mathbf{A}}\). Our construction is based on a new model, called well-structured vector addition systems (WSVAS), that naturally extends VAS with infinite sets of actions, while still preserving the well-quasi-order and amalgamation property on executions. We use WSVAS to simulate BVAS executions composed of a main branch with, on the side of this branch, configurations that are reachable or in \({\mathbf{A}}\).

• Once the attractor \({\mathbf{A}}\) has been enlarged, the abstract graph \(\mathcal{G}\) is updated by removing \(\Gamma\) and by adding new nodes corresponding to executions in the concretization of some nodes in \(\Gamma\) that are still not captured by the enlarged attractor. In order to preserve the homogeneity property of \(\mathcal{G}\), we establish a geometric decomposition result, that we dub face stripping theorem. This theorem provides a way to decompose the difference of two particular semilinear sets into a sequence of semilinear sets that respects the order induced by the reachability relation of the BVAS. Moreover, the updated abstract graph is smaller than \(\mathcal{G}\) for a natural well-founded relation.

We iteratively enlarge the attractor and update the abstract graph until the latter becomes empty (which is bound to happen). At that point, the attractor is guaranteed to be an inductive invariant that excludes the unreachable target. This allows us to conclude that the reachability problem for BVAS is decidable.

1.0.0.5 Related work.

Our result settles a long-standing open problem simultaneously arising in the theory of counter systems and in the proof theory of linear logic.

Understanding which extensions of VAS preserve decidability of reachability has been a recurring theme in the theory of infinite-state systems. Some extensions remain decidable despite their increased expressive power. This includes VAS equipped with a restricted form of zero tests, whose reachability problem was shown decidable in 2008 [27] and whose complexity was recently established to be Ackermann-complete [28], matching that of VAS. Another long-standing open problem was recently settled with the decidability of reachability in pushdown vector addition systems [29]. By contrast, the decidability of reachability remains open and actively investigated for unordered data nets [30]–[32].

The connection between counter systems, in particular VAS, and substructural logics, in particular linear logic, has motivated a long line of research. At an intuitive level, both formalisms reason about resources: VAS counters in one setting, and logical assumptions in the other. This intuition has repeatedly led to reductions relating fragments of linear logic and classes of counter systems. For example, Lincoln, Mitchell, Scedrov, and Shankar established the undecidability of linear-logic provability through a reduction from Minsky machines [33]. Conversely, Kanovich derived decidability for the !-Horn fragment of MELL by a reduction to VAS reachability [34]. BVAS provide a particularly striking instance of this connection through the inter-reducibility between BVAS reachability and provability in MELL, established by de Groote, Guillaume, and Salvati [3]. Our result entails that MELL provability is decidable.

2 Preliminaries↩︎

We start with basic definitions and notations that are used throughout the paper. Let \(\mathbb{Z}\) denote the set of integers, \(\mathbb{N}\) denote the set of natural numbers, \(\mathbb{Q}\) denote the set of rational numbers, and \(\mathbb{Q}_{\geq 0}\) denote the set of non-negative rational numbers. We also introduce the sets \(\mathbb{N}_{>0}\) and \(\mathbb{Q}_{>0}\) defined as \(\mathbb{N}\setminus \{0\}\) and \(\mathbb{Q}_{\geq 0}\setminus\{0\}\), respectively.

2.0.0.1 Orders

A quasi-ordered set (qoset for short) is a pair \((X, \preceq)\) where \(X\) is a set and \(\preceq\) is a reflexive and transitive binary relation on \(S\). We let \(\operatorname{Min}_{\preceq}(X)\) denote the set of minimal elements of a qoset \((X, \preceq)\). Recall that a minimal element of \((X, \preceq)\) is an element \(m \in X\) such that \(x \preceq m \Rightarrow m \preceq x\) for all \(x \in X\). A partially-ordered set (poset for short) is a qoset \((X, \preceq)\) such that \(\preceq\) is antisymmetric. A well-quasi-ordered set (wqo for short) is a qoset \((X, \preceq)\) such that every infinite sequence \(x_0, x_1, x_2, \ldots\) of elements in \(X\) contains an infinite subsequence \(x_{i_0} \preceq x_{i_1} \preceq x_{i_2} \cdots\) (with \(i_0 < i_1 < i_2 \cdots\)). A well-partially-ordered set (wpo for short) is a poset \((X, \preceq)\) such that \((X, \preceq)\) is a wqo. We recall that every wqo \((X, \preceq)\) contains a finite set \(M \subseteq X\) such that \(\operatorname{Min}_{\preceq}(X) = \{x \in X \mid \exists m \in M : m \preceq x \preceq m\}\) and \(X = \bigcup_{m \in M} \{x \in X \mid m \preceq x\}\). In particular, every wpo \((X, \preceq)\) has finitely many minimal elements. A map \(f\) from a qoset \((X, \preceq_X)\) to a qoset \((Y, \preceq_Y)\) is order-preserving if for every \(a, b \in X\), it holds that \(a \preceq_X b \Rightarrow f(a) \preceq_Y f(b)\).

2.0.0.2 Vectors

We consider a fixed dimension \(d \in \mathbb{N}_{>0}\) for the remainder of the paper. Vectors are typeset in bold face. Given \({\mathbf{x}} \in \mathbb{Q}^d\), we let \(({\mathbf{x}}(1), \ldots, {\mathbf{x}}(d))\) denote the vector of rational numbers defining \({\mathbf{x}}\). The dot-product of two vector \({\mathbf{x}},{\mathbf{y}}\in\mathbb{Q}^d\) is defined as \(\sum_{i=1}^d{\mathbf{x}}(i){\mathbf{y}}(i)\). The partial order \(\leq\) on \(\mathbb{Q}^d\) is the component-wise extension of the usual order \(\leq\) on \(\mathbb{Q}\) (i.e., \({\mathbf{x}} \leq {\mathbf{y}}\) when \({\mathbf{x}}(i) \leq {\mathbf{y}}(i)\) for all \(i \in \{1, \ldots, d\}\)). The sum and the subtraction of two vectors \({\mathbf{x}} + {\mathbf{y}}\) and \({\mathbf{x}}-{\mathbf{y}}\) are defined similarly component-wise. The sum and the subtraction operators over vectors are extended over sets \({\mathbf{X}},{\mathbf{Y}}\subseteq\mathbb{Q}^d\) by \({\mathbf{X}}+{\mathbf{Y}}\mathrel{\vcenter{:}}=\{{\mathbf{x}}+{\mathbf{y}}\mid {\mathbf{x}}\in{\mathbf{X}}\wedge{\mathbf{y}}\in{\mathbf{Y}}\}\) and \({\mathbf{X}}-{\mathbf{Y}}\mathrel{\vcenter{:}}= \{{\mathbf{x}}-{\mathbf{y}}\mid {\mathbf{x}}\in{\mathbf{X}}\wedge{\mathbf{y}}\in{\mathbf{Y}}\}\). To reduce clutter, singleton sets \(\{{\mathbf{x}}\}\) appearing in a sum of sets are shortly written \({\mathbf{x}}\) (i.e., without braces). We let \(\mathbb{Q}_{\geq 0}{\mathbf{X}}\) denote the set \(\{\lambda{\mathbf{x}} \mid \lambda\in \mathbb{Q}_{\geq 0}\wedge {\mathbf{x}}\in{\mathbf{X}}\}\).

2.1 Discrete Sets↩︎

2.1.0.1 Periodic Sets

A set \({\mathbf{P}}\subseteq \mathbb{Z}^d\) is called a periodic set if \({\mathbf{0}}\in {\mathbf{P}}\) and \({\mathbf{P}}+{\mathbf{P}}\subseteq {\mathbf{P}}\). The periodic set spanned by a set \({\mathbf{X}}\subseteq \mathbb{Z}^d\) is the set \(\operatorname{Per}({\mathbf{X}})\) of vectors of the form \({\mathbf{x}}_1+\cdots+{\mathbf{x}}_k\) where \(k\in\mathbb{N}\) and \({\mathbf{x}}_1,\ldots,{\mathbf{x}}_k\in {\mathbf{X}}\). This set is clearly the \(\subseteq\)-minimal periodic set containing \({\mathbf{X}}\). When \({\mathbf{X}}\) is finite, the periodic set \(\operatorname{Per}({\mathbf{X}})\) is said to be finitely-generated. We associate with a periodic set \({\mathbf{P}}\subseteq\mathbb{Z}^d\) the quasi-order \(\leq_{{\mathbf{P}}}\) on \(\mathbb{Z}^d\) defined by \({\mathbf{x}}\leq_{{\mathbf{P}}}{\mathbf{y}}\) if \({\mathbf{y}}\in {\mathbf{x}}+{\mathbf{P}}\). We recall the following folklore result, well-known when \({\mathbf{P}}\subseteq \mathbb{N}^d\). Its proof can be found in 9.

A linear set is a set \({\mathbf{L}}\subseteq \mathbb{Z}^d\) of the form \({\mathbf{b}}+{\mathbf{P}}\) where \({\mathbf{b}}\in\mathbb{Z}^d\) and \({\mathbf{P}}\subseteq \mathbb{Z}^d\) is a finitely-generated periodic set. A semilinear set is a finite union of linear sets. We recall that semilinear sets are effectively closed under union, intersection and complement. Semilinear sets coincide with the sets definable in the first-order theory \(\textrm{FO}(\mathbb{Z},+,\leq)\), known as Presburger arithmetic [35].

2.1.0.2 Cylindric Sets and Diagonal Relations

Let \({\mathbf{Q}}\subseteq \mathbb{Z}^d\) be a finitely-generated periodic set. A set \({\mathbf{S}}\subseteq \mathbb{Z}^d\) is said to be \({\mathbf{Q}}\)-cylindric if \({\mathbf{S}}+{\mathbf{Q}}\subseteq {\mathbf{S}}\). A set \({\mathbf{S}}\subseteq \mathbb{Z}^d\) is said to be finitary \({\mathbf{Q}}\)-cylindric if there exists a finite set \({\mathbf{B}}\subseteq \mathbb{Z}^d\) such that \({\mathbf{S}}={\mathbf{B}}+{\mathbf{Q}}\). Observe that \(\leq_{{\mathbf{Q}}}\) is a wqo on a \({\mathbf{Q}}\)-cylindric set \({\mathbf{S}}\) if, and only if, \({\mathbf{S}}\) is finitary \({\mathbf{Q}}\)-cylindric. This entails that \({\mathbf{Q}}\)-cylindric sets included in some finitary \({\mathbf{Q}}\)-cylindric set are finitary \({\mathbf{Q}}\)-cylindric. A binary relation \(R\) over \(\mathbb{Z}^d\) is said to be \({\mathbf{Q}}\)-diagonal if \(({\mathbf{x}},{\mathbf{y}})+({\mathbf{q}},{\mathbf{q}})\in R\) for every \(({\mathbf{x}},{\mathbf{y}})\in R\) and every \({\mathbf{q}}\in {\mathbf{Q}}\). Note that a binary relation is \({\mathbf{Q}}\)-diagonal if, and only if, it is \({\mathbf{Q}'}\)-cylindric for the finitely-generated periodic set \({\mathbf{Q}}'\mathrel{\vcenter{:}}=\{({\mathbf{q}},{\mathbf{q}}) \mid {\mathbf{q}}\in {\mathbf{Q}}\}\).

2.1.0.3 Groups

A set \({\mathbf{G}}\subseteq \mathbb{Z}^d\) is called a group if \({\mathbf{0}}\in {\mathbf{G}}\) and \({\mathbf{G}}+{\mathbf{G}}\subseteq {\mathbf{G}}\), and \(-{\mathbf{G}} \subseteq {\mathbf{G}}\). The group spanned by a set \({\mathbf{X}}\subseteq \mathbb{Z}^d\) is the set of vectors of the form \(z_1{\mathbf{x}}_1+\cdots+z_k{\mathbf{x}}_k\) where \(k\in\mathbb{N}\), \({\mathbf{x}}_1,\ldots,{\mathbf{x}}_k\in {\mathbf{X}}\), and \(z_1,\ldots,z_k\in\mathbb{Z}\). Let us recall that every group \({\mathbf{G}} \subseteq \mathbb{Z}^d\) is finitely-generated. Notice that the group spanned by a periodic set \({\mathbf{P}}\) is equal to \({\mathbf{P}}-{\mathbf{P}}\).

2.2 Dense Sets↩︎

2.2.0.1 Cones

A set \({\mathbf{C}}\subseteq \mathbb{Q}^d\) is called a cone if \({\mathbf{0}}\in {\mathbf{C}}\), \({\mathbf{C}}+{\mathbf{C}}\subseteq {\mathbf{C}}\), and \(\mathbb{Q}_{\geq 0}{\mathbf{C}}\subseteq {\mathbf{C}}\). The cone spanned by a set \({\mathbf{X}}\subseteq \mathbb{Q}^d\) is the set \(\operatorname{Con}({\mathbf{X}})\) of vectors of the form \(\lambda_1{\mathbf{x}}_1+\cdots+\lambda_k{\mathbf{x}}_k\) where \(k\in\mathbb{N}\), \({\mathbf{x}}_1,\ldots,{\mathbf{x}}_k\in {\mathbf{X}}\), and \(\lambda_1,\ldots,\lambda_k\in\mathbb{Q}_{\geq 0}\). This set is clearly the \(\subseteq\)-minimal cone containing \({\mathbf{X}}\). Notice that \(\operatorname{Con}({\mathbf{P}}) = \mathbb{Q}_{\geq 0}{\mathbf{P}}\) for every periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\).

2.2.0.2 Vector Spaces

A set \({\mathbf{V}}\subseteq\mathbb{Q}^d\) is called a vector space if \({\mathbf{0}}\in{\mathbf{V}}\), \({\mathbf{V}}+{\mathbf{V}}\subseteq {\mathbf{V}}\), and \(\mathbb{Q}{\mathbf{V}}\subseteq {\mathbf{V}}\). The vector space spanned by a set \({\mathbf{X}}\subseteq \mathbb{Q}^d\) is the set \(\operatorname{Vec}({\mathbf{X}})\) of vectors of the form \(\lambda_1{\mathbf{x}}_1+\cdots+\lambda_k{\mathbf{x}}_k\) where \(k\in\mathbb{N}\), \({\mathbf{x}}_1,\ldots,{\mathbf{x}}_k\in {\mathbf{X}}\), and \(\lambda_1,\ldots,\lambda_k\in\mathbb{Q}\). Let us recall that any vector space \({\mathbf{V}}\subseteq\mathbb{Q}^d\) is spanned by a finite set \({\mathbf{X}}\subseteq {\mathbf{V}}\). The minimal cardinality of such a set \({\mathbf{X}}\) is called the dimension of \({\mathbf{V}}\) and it is denoted as \(\operatorname{dim}({\mathbf{V}})\). Let us recall that given two vector spaces \({\mathbf{V}}\subsetneq {\mathbf{W}}\) we have \(\operatorname{dim}({\mathbf{V}})<\operatorname{dim}({\mathbf{W}})\). It follows that \(\operatorname{dim}({\mathbf{V}})\in\{0,\ldots,d\}\) for every vector space \({\mathbf{V}}\subseteq \mathbb{Q}^d\). Moreover, if \({\mathbf{V}}\) is the vector space spanned by a set \({\mathbf{X}}\subseteq \mathbb{Q}^d\), then \({\mathbf{V}}\) is also spanned by a set of \(\operatorname{dim}({\mathbf{V}})\) vectors in \({\mathbf{X}}\). Notice that \(\operatorname{Vec}({\mathbf{C}}) = {\mathbf{C}}-{\mathbf{C}}\) for every cone \({\mathbf{C}}\subseteq \mathbb{Q}^d\).

2.2.0.3 Topological Closure

We denote by \(\operatorname{Ball}_{{\mathbf{v}},\varepsilon}\) where \({\mathbf{v}}\in\mathbb{Q}^d\) and \(\varepsilon\in\mathbb{Q}_{>0}\) the open ball centered on \({\mathbf{v}}\) of radius \(\varepsilon\) and defined as the set of \({\mathbf{x}}\in\mathbb{Q}^d\) such that \({\mathopen{\|}{\mathbf{v}}-{\mathbf{x}}\mathclose{\|}}<\varepsilon\). A limit of a set \({\mathbf{X}}\subseteq \mathbb{Q}^d\) is a vector \({\mathbf{v}}\in\mathbb{Q}^d\) such that \(\operatorname{Ball}_{{\mathbf{v}},\varepsilon}\cap{\mathbf{X}}\not=\emptyset\) for every \(\varepsilon\in\mathbb{Q}_{>0}\). We denote by \(\overline{{\mathbf{X}}}\) the set of limits of \({\mathbf{X}}\), and called the topological closure of \({\mathbf{X}}\). When \(\overline{{\mathbf{X}}}={\mathbf{X}}\), we say that \({\mathbf{X}}\) is topologically closed. Recall that \(\overline{{\mathbf{X}}}\) is topologically closed for every set \({\mathbf{X}}\subseteq \mathbb{Q}^d\). Notice that if \({\mathbf{C}}\subseteq \mathbb{Q}^d\) is a cone, then \(\overline{{\mathbf{C}}}\) is a cone as well. Recall also that finitely-generated cones (including vector spaces) are topologically closed.

2.3 Linearizations↩︎

We recall the definition of full¹ periodic sets from [36]. A periodic set \({\mathbf{P}}\subseteq\mathbb{Z}^d\) is said to be full if \({\mathbf{P}}={\mathbf{G}}\cap{\mathbf{C}}\) for a group \({\mathbf{G}}\subseteq\mathbb{Z}^d\) and a cone \({\mathbf{C}}\subseteq\mathbb{Q}^d\). Given a periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\), its linearization [18] is the full periodic set \(\operatorname{Lin}({\mathbf{P}})\mathrel{\vcenter{:}}= ({\mathbf{P}}-{\mathbf{P}})\cap \mathbb{Q}_{\geq 0}{\mathbf{P}}\). Clearly, a periodic set \({\mathbf{P}}\) is full if, and only if, \(\operatorname{Lin}({\mathbf{P}})={\mathbf{P}}\). The closed linearization [17] of a periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\) is the full periodic set \(\overline{\operatorname{Lin}}({\mathbf{P}})\mathrel{\vcenter{:}}=({\mathbf{P}}-{\mathbf{P}})\cap\overline{\mathbb{Q}_{\geq 0}{\mathbf{P}}}\). As a side remark, we observe that these two linearizations are upper closure operators (i.e., order-preserving, extensive and idempotent operators) on the complete lattice of periodic subsets of \(\mathbb{Z}^d\) ordered by inclusion.

3 Safety Witnesses for Branching VAS and Overview of our Approach↩︎

A branching VAS (or BVAS for short) is a non-empty finite sequence \(\mathcal{B}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r)\) of finite subsets of \(\mathbb{Z}^d\). The natural number \(r \geq 1\) is the maximal arity of \(\mathcal{B}\), and each \({\mathbf{\Delta}}_n\) with \(n \in \{1,\ldots,r\}\) provides the set of \(n\)-ary actions. A configuration of \(\mathcal{B}\) is a vector in \(\mathbb{N}^d\). The set of runs of \(\mathcal{B}\) is defined inductively as follows.² A run is a pair \(\rho \mathrel{\vcenter{:}}= ({\mathbf{c}}, (\rho_1, \ldots, \rho_n))\) where \({\mathbf{c}} \in \mathbb{N}^d\) is called the target of \(\rho\) and \(\rho_1, \ldots, \rho_n\) is a (possibly empty) finite sequence of runs, with \(n \in \{0,\ldots,r\}\), whose respective targets \({\mathbf{c}}_1, \ldots, {\mathbf{c}}_n\) satisfy \({\mathbf{c}} - \sum_{j=1}^{n} {\mathbf{c}}_j\in {\mathbf{\Delta}}_n\) if \(n \geq 1\). Given such a run \(\rho\), we define \(\operatorname{tgt}(\rho) \mathrel{\vcenter{:}}= {\mathbf{c}}\), \(\operatorname{arity}(\rho) \mathrel{\vcenter{:}}= n\), \(\operatorname{act}(\rho) \mathrel{\vcenter{:}}= {\mathbf{c}} - \sum_{j=1}^{n} {\mathbf{c}}_j\), and \(\rho[j] \mathrel{\vcenter{:}}= \rho_j\) for each \(j \in \{1, \ldots, n\}\). The source of a run \(\rho \mathrel{\vcenter{:}}= ({\mathbf{c}}, (\rho_1, \ldots, \rho_n))\) is the non-empty word \(\operatorname{src}(\rho) \in (\mathbb{N}^d)^+\) defined inductively by \(\operatorname{src}(\rho) \mathrel{\vcenter{:}}= {\mathbf{c}}\) if \(n = 0\) and \(\operatorname{src}(\rho) \mathrel{\vcenter{:}}= \operatorname{src}(\rho_1) \cdots \operatorname{src}(\rho_n)\) if \(n \geq 1\). We write \(\operatorname{Runs}(\mathcal{B})\) the set of runs of \(\mathcal{B}\). Given a language \(L\subseteq (\mathbb{N}^d)^+\), the reachability set from \(L\), written \(\operatorname{Reach}_{}(L)\), is the set of targets of runs \(\rho\) such that \(\operatorname{src}(\rho)\in L\).

A VAS is a BVAS \(({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r)\) such that \(r = 1\). The following fact extends to BVAS runs the usual monotony property of VAS runs. Its proof is obtained by immediate induction on \(\rho\).

An initialized BVAS (or IBVAS for short) is a pair \(\mathcal{S}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_0, \mathcal{B})\) where \({\mathbf{\Delta}}_0 \subseteq \mathbb{N}^d\) is a finite set of initial configurations and \(\mathcal{B}\) is a BVAS. An initialized run (or irun for short) of \(\mathcal{S}\) is a run \(\rho\) of \(\mathcal{B}\) such that \(\operatorname{src}(\rho) \in {\mathbf{\Delta}}_0^+\). We let \(\operatorname{IRuns}(\mathcal{S})\) denote the set of iruns of \(\mathcal{S}\). The reachability set of \(\mathcal{S}\) is the set \(\operatorname{Reach}_{}(\mathcal{S}) \mathrel{\vcenter{:}}= \operatorname{Reach}_{}({\mathbf{\Delta}}_0^+)\). We also introduce the binary relation \(\xrightarrow{\mathcal{S}}\) on configurations defined by \({\mathbf{x}} \xrightarrow{\mathcal{S}} {\mathbf{y}}\) if \({\mathbf{y}} \in \operatorname{Reach}_{}({\mathbf{\Delta}}_0^* \, {\mathbf{x}} \, {\mathbf{\Delta}}_0^*)\).

The BVAS reachability problem takes as input an IBVAS \(\mathcal{S}\) and a configuration \({\mathbf{c}}\), and determines whether \({\mathbf{c}}\) is a member of \(\operatorname{Reach}_{}(\mathcal{S})\). Clearly, if \({\mathbf{c}}\in\operatorname{Reach}_{}(\mathcal{S})\) then there exists an irun \(\rho\) such that \(\operatorname{tgt}(\rho)={\mathbf{c}}\). It follows that the BVAS reachability problem is recursively enumerable. In order to prove that the problem is decidable, we show in this paper that if \({\mathbf{c}}\not\in\operatorname{Reach}_{}(\mathcal{S})\) then there exists a semilinear inductive invariant witnessing that property. We first recall some definitions.

An inductive invariant for an IBVAS \(\mathcal{S}= ({\mathbf{\Delta}}_0, ({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r))\) is a set \({\mathbf{I}}\subseteq \mathbb{N}^d\) such that for every \(n\in \{0,\ldots,r\}\) and for every \({\mathbf{a}}\in{\mathbf{\Delta}}_n\), the following property holds: \[{\mathbf{a}}+\underbrace{{\mathbf{I}}+\cdots+{\mathbf{I}}}_{\text{n times}} \quad \subseteq \quad {\mathbf{I}}\cup(\mathbb{Z}^d\setminus \mathbb{N}^d) \:.\] Notice that a set \({\mathbf{I}}\subseteq \mathbb{N}^d\) is an inductive invariant if, and only if, \({\mathbf{\Delta}}_0 \subseteq {\mathbf{I}}\) and \(\operatorname{Reach}_{}({\mathbf{I}}^+)\subseteq {\mathbf{I}}\). An immediate consequence of [fact:reach-shuffle] below is that the reachability set itself is an inductive invariant (in fact, \(\operatorname{Reach}_{}(\mathcal{S})\) is the \(\subseteq\)-least inductive invariant). It follows that \({\mathbf{c}}\not\in \operatorname{Reach}_{}(\mathcal{S})\) if, and only if, there exists an inductive invariant \({\mathbf{I}}\subseteq \mathbb{N}^d\) such that \({\mathbf{c}}\not\in{\mathbf{I}}\). We can effectively decide whether a given semilinear set is an inductive invariant. So the following theorem, applied with the semilinear set \({\mathbf{\Phi}}\mathrel{\vcenter{:}}=\mathbb{N}^d\setminus\{{\mathbf{c}}\}\), immediately entails that the BVAS reachability problem is decidable. This theorem is the main result of the paper.

Our definition of \(\operatorname{Reach}_{}(L)\) above is for arbitrary languages \(L\subseteq (\mathbb{N}^d)^+\), but we actually only care about reachability sets from commutative languages. Recall that a language \(L\) is commutative if \(uxyv \in L \Rightarrow uyxv \in L\) for every words \(u, v, x, y\). We also recall the definition of the shuffle operator, which provides an analogue of language concatenation in the commutative setting. The shuffle of two languages \(K\) and \(L\), written \(K \,{\shuffle}\, L\), is the set of words \(u_1 v_1 \cdots u_k v_k\) such that \(u_1 \cdots u_k \in K\) and \(v_1 \cdots v_k \in L\). Notice that \(K \,{\shuffle}\, L\) is commutative when \(K\) and \(L\) are commutative.

We prove 1 by iteratively transforming so-called safety witnesses. To define these safety witnesses, we need to introduce the notions of attractors and directed iruns. An attractor for an IBVAS \(\mathcal{S}= ({\mathbf{\Delta}}_0, \mathcal{B})\) is a set \({\mathbf{A}} \subseteq \mathbb{N}^d\) such that \(\operatorname{Reach}_{}({\mathbf{A}}^+ \,{\shuffle}\, {\mathbf{\Delta}}_0^*) \subseteq {\mathbf{A}}\). In particular, both \(\emptyset\) and \(\mathbb{N}^d\) are attractors. The notion of attractor is closely related to the notion of inductive invariant. Indeed, every inductive invariant is an attractor, and every attractor \({\mathbf{A}}\) that contains \({\mathbf{\Delta}}_0\) is an inductive invariant. Notice that, by [fact:reach-shuffle], a set \({\mathbf{A}} \subseteq \mathbb{N}^d\) is an attractor if, and only if, \(\operatorname{Reach}_{}({\mathbf{A}}^+ \,{\shuffle}\, \operatorname{Reach}_{}(\mathcal{S})^*) \subseteq {\mathbf{A}}\). It follows that \({\mathbf{A}} \cup \operatorname{Reach}_{}(\mathcal{S})\) is an inductive invariant for every attractor \({\mathbf{A}}\). The following lemma shows how to incrementally construct attractors.

The notion of directed iruns relies on cones (see 2) and on a wpo on iruns introduced in [22] with slightly different notations. Let us define the partial-order \(\sqsubseteq\) on runs of a BVAS \(\mathcal{B}\) inductively by \(\alpha \sqsubseteq \beta\) if \(\alpha = \beta\) or there exists \(j \in \{1, \ldots, \operatorname{arity}(\beta)\}\) such that \(\alpha \sqsubseteq \beta[j]\). We define the partial-order \(\trianglelefteq\) on runs of a BVAS \(\mathcal{B}\) inductively by \(\alpha \trianglelefteq \beta\) if there exists \(\beta' \sqsubseteq \beta\) such that \(\operatorname{tgt}(\alpha) \leq \operatorname{tgt}(\beta), \operatorname{tgt}(\beta')\), \(\operatorname{arity}(\alpha) = \operatorname{arity}(\beta')\), \(\operatorname{act}(\alpha) = \operatorname{act}(\beta')\), and \(\alpha[j] \trianglelefteq \beta'[j]\) for every \(j\).

Our approach crucially relies on the following lemma, which was proved in [22] with slightly different notations. For the sake of completeness, we reprove this lemma in 10.

Consider an IBVAS \(\mathcal{S}\). For each irun \(\rho\) of \(\mathcal{S}\), we let \({\mathbf{P}}_\rho\) denote the periodic subset of \(\mathbb{N}^d\) defined by \({\mathbf{P}}_\rho \mathrel{\vcenter{:}}= \{\operatorname{tgt}(\sigma) - \operatorname{tgt}(\rho) \mid \sigma \in \operatorname{IRuns}(\mathcal{S})\wedge \rho\trianglelefteq \sigma\}\). The fact that \({\mathbf{P}}_\rho\) is periodic immediately follows from the amalgamation property of \(\trianglelefteq\). A directed irun of \(\mathcal{S}\) is a pair \(w \mathrel{\vcenter{:}}= (\rho_w, {\mathbf{C}}_w)\) where \(\rho_w\) is an irun of \(\mathcal{S}\) and \({\mathbf{C}}_w \subseteq \mathbb{Q}_{\geq 0}^d\) is a finitely-generated cone. We let \(\operatorname{IRuns}(w)\) denote the set of iruns \(\sigma\) such that \(\rho_w \trianglelefteq \sigma\) and \(\operatorname{tgt}(\sigma) \in \operatorname{tgt}(\rho_w) + {\mathbf{C}}_w\). We also introduce, for each directed irun \(w \mathrel{\vcenter{:}}= (\rho_w, {\mathbf{C}}_w)\), the periodic sets \({\mathbf{P}}_w, {\mathbf{Q}}_w \subseteq \mathbb{N}^d\) defined by \({\mathbf{P}}_w \mathrel{\vcenter{:}}= {\mathbf{P}}_{\rho_w} \cap {\mathbf{C}}_w\) and \({\mathbf{Q}}_w \mathrel{\vcenter{:}}= \overline{\operatorname{Lin}}({\mathbf{P}}_w)\). Note that³ \(\operatorname{tgt}(\operatorname{IRuns}(w)) = \operatorname{tgt}(\rho_w) + {\mathbf{P}}_w\). The following lemma will be shown in 4.2.

We introduce a binary relation \(\twoheadrightarrow_{}\) on directed iruns of \(\mathcal{S}\), defined by \(u \twoheadrightarrow_{}v\) if \(\alpha \sqsubseteq \beta\) for some \(\alpha \in \operatorname{IRuns}(u)\) and \(\beta \in \operatorname{IRuns}(v)\). A set \(W\) of directed iruns induces a (directed) graph \((W, \twoheadrightarrow_{W})\), where \(\twoheadrightarrow_{W}\) is the intersection of \(\twoheadrightarrow_{}\) and \(W \times W\). Let \(\stackrel{*}{\twoheadrightarrow}_{W}\) denote the reflexive and transitive closure of \(\twoheadrightarrow_{W}\). We say that \(W\) is homogeneous when \({\mathbf{C}}_u = {\mathbf{C}}_v\) for every \(u, v \in W\) such that \(u \stackrel{*}{\twoheadrightarrow}_{W} v \stackrel{*}{\twoheadrightarrow}_{W} u\). In that case, we also have \({\mathbf{Q}}_u = {\mathbf{Q}}_v\) for every \(u, v \in W\) such that \(u \stackrel{*}{\twoheadrightarrow}_{W} v \stackrel{*}{\twoheadrightarrow}_{W} u\). This property is an immediate consequence of 3 below. Assuming that \(W\) is homogeneous, for each SCC \(\Gamma\) of the graph \((W, \twoheadrightarrow_{W})\), we let \({\mathbf{C}}_\Gamma\) and \({\mathbf{Q}}_\Gamma\) denote the common \({\mathbf{C}}_\gamma\) and \({\mathbf{Q}}_\gamma\) where \(\gamma\) ranges over \(\Gamma\).

Given an IBVAS \(\mathcal{S}\) and a semilinear set \({\mathbf{\Phi}} \subseteq \mathbb{N}^d\) such that \(\operatorname{Reach}_{}(\mathcal{S}) \subseteq {\mathbf{\Phi}}\), a safety witness for \(\mathcal{S}\) and \({\mathbf{\Phi}}\) is a pair \(({\mathbf{A}}, W)\) where \({\mathbf{A}} \subseteq {\mathbf{\Phi}}\) is a semilinear attractor for \(\mathcal{S}\) and \(W\) is an homogeneous finite set of directed iruns of \(\mathcal{S}\) such that for every irun \(\rho \in \operatorname{IRuns}(\mathcal{S})\), we have \(\operatorname{tgt}(\rho) \in {\mathbf{A}}\) or \(\rho \in \operatorname{IRuns}(w)\) for some \(w \in W\). One may wonder about the existence of safety witnesses. Consider the set \(W_{min}\) of directed iruns \((\rho, \mathbb{Q}_{\geq 0}^d)\) such that \(\rho \in \operatorname{Min}_{\trianglelefteq}(\operatorname{IRuns}(\mathcal{S}))\). The set \(W_{min}\) is finite by [lem:ibvas-wpo-and-amalgamation], hence, the pair \((\emptyset, W_{min})\) is a safety witness for \(\mathcal{S}\) and \({\mathbf{\Phi}}\).

To prove 1, we iteratively transform safety witnesses until we get a safety witness of the form \(({\mathbf{A}}, \emptyset)\), in which case the semilinear attractor \({\mathbf{A}} \subseteq {\mathbf{\Phi}}\) is an inductive invariant for \(\mathcal{S}\). More precisely, we show the key property that for every safety witness \(({\mathbf{A}}, W)\) with \(W \neq \emptyset\), there exists a safety witness \(({\mathbf{A}}', W')\) such that \(W'\) is smaller than \(W\) for a natural well-founded relation on finite sets of directed iruns. This entails that a safety witness of the form \(({\mathbf{A}}, \emptyset)\) exists, and concludes the proof of 1. The remainder of the paper is devoted to the proof of this key property. To give a taste of the proof, we conclude this section with an overview of the construction of \(({\mathbf{A}}', W')\) from \(({\mathbf{A}}, W)\). This overview will be reformulated with full details in 7.

Consider a safety witness \(({\mathbf{A}}, W)\) with \(W \neq \emptyset\). Pick an arbitrary bottom SCC \(\Gamma\) of the graph \((W, \twoheadrightarrow_{W})\). We introduce the finitary \({\mathbf{Q}}_\Gamma\)-cylindric set \({\mathbf{Y}}_\Gamma \mathrel{\vcenter{:}}= \{\operatorname{tgt}(\rho_\gamma) \mid \gamma \in \Gamma\} + {\mathbf{Q}}_\Gamma\). Our approach is decomposed into two main steps:

1. Using 1, we show how to construct a finitary \({\mathbf{Q}}_\Gamma\)-cylindric set \({\mathbf{X}} \subseteq {\mathbf{Y}}_{\Gamma}\) such that firstly \({\mathbf{A}}' \mathrel{\vcenter{:}}= {\mathbf{A}} \cup {\mathbf{X}}\) is an attractor contained in \({\mathbf{\Phi}}\), secondly \({\mathbf{Y}}_\Gamma \subseteq {\mathbf{X}} - {\mathbf{Q}}_\Gamma\), and thirdly \(\xrightarrow{\mathcal{S}}\) has an empty intersection with \({\mathbf{X}} \times ({\mathbf{Y}}_\Gamma \setminus {\mathbf{X}})\).

2. We show that there exist some finitely-generated cones \({\mathbf{C}}_1, \ldots, {\mathbf{C}}_n\) contained in \({\mathbf{C}}_\Gamma\) and a disjoint decomposition⁴ \({\mathbf{S}}_1, \ldots, {\mathbf{S}}_n\) of \({\mathbf{Y}}_\Gamma \setminus {\mathbf{X}}\) such that \(\operatorname{dim}({\mathbf{C}}_i-{\mathbf{C}}_i)<\operatorname{dim}({\mathbf{C}}_\Gamma-{\mathbf{C}}_\Gamma)\) and \({\mathbf{S}}_i\) is finitary \(({\mathbf{Q}}\cap{\mathbf{C}}_i)\)-cylindric for every \(1\leq i\leq n\). The homogeneous set \(W'\) of directed iruns is then defined as \(W' \mathrel{\vcenter{:}}= (W\setminus \Gamma)\cup (W_1\cup\ldots W_n)\) where each \(W_i\) is a finite set of directed iruns obtained from \({\mathbf{S}}_i\).

By construction, the pair \(({\mathbf{A}}', W')\) defined in this way is a safety witness and \(W'\) is smaller than \(W\).

The rest of the paper presents the details of our proof. 5 is devoted to the first step (construction of \({\mathbf{A}}'\)) and 6 is devoted to the second step (construction of \(W'\)). Before that, we provide in the next section some geometrical properties of periodic sets and their linearizations, and we prove 2 along the way.

4 Geometry of Branching VAS Reachability Sets↩︎

In [17], reachability sets of initialized VAS (a VAS is a BVAS \(({\mathbf{\Delta}}_1,\ldots,{\mathbf{\Delta}}_r\)) such that \(r=1\)) was proved to be almost semilinear, a class of sets extending the class of semilinear sets. This result was recently extended to the class of IBVAS in [22] by observing that IBVAS reachability sets are sections of initialized VAS reachability sets.

In 4.1, we recall the class of almost semilinear sets, based on the class of definable cones and asymptotically-definable periodic sets. We explain why the two linearization operators introduced in 2 provide ways to transfer properties from cones to periodic sets. In 4.2 we prove by structural induction on a irun \(\rho\) that the periodic set \({\mathbf{P}}_\rho \mathrel{\vcenter{:}}= \{\operatorname{tgt}(\sigma) - \operatorname{tgt}(\rho) \mid \sigma \in \operatorname{IRuns}(\mathcal{S})\wedge \rho\trianglelefteq \sigma\}\) is asymptotically-definable. From this property, we derive a proof of 2.

4.1 Some Geometric Properties of Periodic Sets and Their Linearizations↩︎

In 2, we introduced the linearization and the closed linearization of a periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\) respectively by \(\operatorname{Lin}({\mathbf{P}})\mathrel{\vcenter{:}}=({\mathbf{P}}-{\mathbf{P}})\cap\operatorname{Con}({\mathbf{P}})\) and \(\overline{\operatorname{Lin}}({\mathbf{P}})\mathrel{\vcenter{:}}=({\mathbf{P}}-{\mathbf{P}})\cap \overline{\operatorname{Con}({\mathbf{P}})}\). As \({\mathbf{P}}-{\mathbf{P}}\) is a group, it is finitely-generated. It follows that properties on cones \(\operatorname{Con}({\mathbf{P}})\) and \(\overline{\operatorname{Con}({\mathbf{P}})}\) can be transfered to properties on the full periodic sets \(\operatorname{Lin}({\mathbf{P}})\) and \(\overline{\operatorname{Lin}}({\mathbf{P}})\).

A cone \({\mathbf{C}}\subseteq\mathbb{Q}^d\) is said to be definable [17], [18] if it can be denoted by a formula in \(\textrm{FO}(\mathbb{Q},+,\leq)\). It follows that finitely-generated cones are definable, and the intersection as well as the sum of two definable cones are definable. Recall [17] that a cone \({\mathbf{C}}\subseteq \mathbb{Q}^d\) is definable if, and only if, \(\overline{{\mathbf{C}}\cap{\mathbf{V}}}\) is a finitely-generated cone for every vector space \({\mathbf{V}}\subseteq\mathbb{Q}^d\). A periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\) is said to be asymptotically-definable [17] if the cone \(\operatorname{Con}({\mathbf{P}})\) is definable. It follows that finitely-generated periodic sets are asymptotically-definable.

The following lemma shows that asymptotically-definable periodic sets are stable by intersection, sum, and projections.

As the intersection of a group (which is necessarily finitely-generated) with a definable cone is Presburger-definable, hence, semilinear, we easily derive that if \({\mathbf{P}}\subseteq\mathbb{Z}^d\) is a periodic set, then \(\operatorname{Lin}({\mathbf{P}})\) is semilinear, if and only if, \({\mathbf{P}}\) is asymptotically-definable. Moreover, as the intersection of a group with a finitely-generated cone is a finitely-generated periodic set, we also deduce that a periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\) is asymptotically-definable if, and only if, \(\overline{\operatorname{Lin}}({\mathbf{P}}\cap{\mathbf{V}})\) is a finitely-generated periodic set for every vector space \({\mathbf{V}}\subseteq\mathbb{Q}^d\). In particular, the following result holds.

An almost linear set is a set \({\mathbf{L}}\subseteq \mathbb{Z}^d\) of the form \({\mathbf{b}}+{\mathbf{P}}\) where \({\mathbf{b}}\in\mathbb{Z}^d\) and \({\mathbf{P}}\subseteq \mathbb{Z}^d\) is an asymptotically-definable periodic set. An almost semilinear set is a finite union of almost linear sets.

Let us recall from [22] that the intersection of IBVAS reachability sets with semilinear sets are almost semilinear. This result can be easily extended to the relation \(\xrightarrow{\mathcal{S}}\) of an IBVAS by using the doubling counter technique, well-known for VAS, and formally defined in the proof of the following lemma. Recall from 3 that \({\xrightarrow{\mathcal{S}}} \subseteq \mathbb{N}^d \times \mathbb{N}^d\) is defined by \({\mathbf{x}} \xrightarrow{\mathcal{S}} {\mathbf{y}}\) if \({\mathbf{y}} \in \operatorname{Reach}_{}({\mathbf{\Delta}}_0^* \, {\mathbf{x}} \, {\mathbf{\Delta}}_0^*)\).

Almost semilinear sets \({\mathbf{S}}\mathrel{\vcenter{:}}={\mathbf{b}}_1+{\mathbf{P}}_1\cup\ldots\cup{\mathbf{b}}_n+{\mathbf{P}}_n\) can be over-approximated by semilinear sets \({\mathbf{b}}_1+{\mathbf{Q}}_1\cup\ldots\cup{\mathbf{b}}_n+{\mathbf{Q}}_n\) obtained by replacing each asymptotically-definable periodic set \({\mathbf{P}}_i\) by the finitely-generated periodic set \({\mathbf{Q}}_i\mathrel{\vcenter{:}}=\overline{\operatorname{Lin}}({\mathbf{P}}_i)\). In order to recover from vectors in this over-approximation, vectors in \({\mathbf{S}}\), the following lemma will be central.

The previous lemma is a corollary of some geometrical results about the center of a periodic set \({\mathbf{P}}\subseteq \mathbb{Z}^d\), written \(\operatorname{Cent}({\mathbf{P}})\) and defined as the set of vectors \({\mathbf{v}}\in \mathbb{Z}^d\) such that for every \({\mathbf{g}}\in{\mathbf{P}}-{\mathbf{P}}\) there exists \(r\in\mathbb{N}\) satisfying \({\mathbf{g}}+(r+\mathbb{N}){\mathbf{v}}\subseteq {\mathbf{P}}\).

Finally, let us prove 8. Let \({\mathbf{P}} \subseteq \mathbb{N}^d\) be a periodic set and let \({\mathbf{Q}} \mathrel{\vcenter{:}}= \overline{\operatorname{Lin}}({\mathbf{P}})\). Let \({\mathbf{p}}\) be a vector obtained as a sum of vectors in \({\mathbf{P}}\) spanning the vector space \(\operatorname{Vec}({\mathbf{P}})\). Lemma 9 shows that \({\mathbf{p}}\in \operatorname{Cent}({\mathbf{P}})\). Let \({\mathbf{g}}\in{\mathbf{P}}-{\mathbf{P}}\) and \({\mathbf{x}}\in {\mathbf{p}}+{\mathbf{Q}}\). Lemma 10 shows that \({\mathbf{x}}\in\operatorname{Cent}({\mathbf{P}})\). It follows that there exists \(r\in\mathbb{N}\) such that \({\mathbf{g}}+(r+\mathbb{N}){\mathbf{x}}\subseteq {\mathbf{P}}\). We have proved the lemma.

4.2 Asymptotic Definability of the Periodic Sets Associated with Initialized Runs↩︎

It was shown in [22] that the reachability set of any IBVAS is almost semilinear.

In this section, we refine this result by exhibiting an almost semilinear decomposition. More precisely, we show that for every irun \(\rho\) of an IBVAS \(\mathcal{S}\), the periodic set⁶ \({\mathbf{P}}_\rho\) is asymptotically-definable. This property entails that the reachability set of \(\mathcal{S}\) is the almost semilinear set \(\bigcup_{\rho \in M} \operatorname{tgt}(\rho) + {\mathbf{P}}_\rho\) where \(M\) is the finite set \(M \mathrel{\vcenter{:}}= \operatorname{Min}_{\trianglelefteq}(\operatorname{IRuns}(\mathcal{S}))\). More importantly for us, the asymptotic definability of the periodic sets \({\mathbf{P}}_\rho\) will allow us to prove 2.

We introduce for a configurations \({\mathbf{c}}\in\mathbb{N}^d\) the so-called transformer relation [18] \(\stackrel{\mathcal{S},{\mathbf{c}}}{\curvearrowright}\) defined over \(\mathbb{N}^d\) by \({\mathbf{x}}\stackrel{\mathcal{S},{\mathbf{c}}}{\curvearrowright}{\mathbf{y}}\) if \({\mathbf{c}}+{\mathbf{x}}\xrightarrow{\mathcal{S}} {\mathbf{c}}+{\mathbf{y}}\).

We are now ready to prove the following lemma.

We conclude this subsection with the proof of 2. Recall that this lemma claims that the periodic set \({\mathbf{Q}}_w\) is finitely-generated for every directed irun \(w\) of an IBVAS \(\mathcal{S}\). Let us also recall that, by definition, \({\mathbf{P}}_w = {\mathbf{P}}_{\rho_w} \cap {\mathbf{C}}_w\) and \({\mathbf{Q}}_w = \overline{\operatorname{Lin}}({\mathbf{P}}_w)\). We derive that \(\operatorname{Con}({\mathbf{P}}_w) = \operatorname{Con}({\mathbf{P}}_{\rho_w}) \cap {\mathbf{C}}_w\) is definable, since \(\operatorname{Con}({\mathbf{P}}_{\rho_w})\) is definable and \({\mathbf{C}}_w\) is a finitely-generated cone. It follows from 5 that \({\mathbf{Q}}_w\) is finitely-generated. We also observe that \(\operatorname{tgt}(\operatorname{IRuns}(w)) = \operatorname{tgt}(\rho_w) + {\mathbf{P}}_w\) is almost linear.

5 Safe Linearization for Branching VAS↩︎

In this section, we present the main ingredient for the first step of our proof, namely the step where we expand the attractor (see the overview at the end of 3). This main ingredient is provided by the following technical lemma, that we call safe linearization lemma for BVAS.

The remainder of this section is devoted to the proof of 13. Apart from this lemma, the material presented in this section is not used in the sequel. Firstly, we introduce a natural extension of VAS, shortly called WSVAS, and prove a safe linearization lemma for this extension. Secondly, we show how to simulate BVAS runs with source in \({\mathbf{X}} \,{\shuffle}\, {\mathbf{I}}^*\), where \({\mathbf{X}} \subseteq \mathbb{N}^d\), by WSVAS runs with source in \({\mathbf{X}}\). Thirdly, we prove that \(\operatorname{Reach}_{}({\mathbf{X}} \,{\shuffle}\, {\mathbf{I}}^*) = \operatorname{Reach}_{}({\mathbf{X}}^+ \,{\shuffle}\, {\mathbf{I}}^*)\) under a suitable condition on \({\mathbf{X}} \subseteq \mathbb{N}^d\). Lastly, we combine these three results to prove 13.

5.1 Well-Structured VAS↩︎

In this subsection, we prove a safe linearization lemma for an extension of VAS that permits infinitely many actions. The definition of this extension relies on the notion of diamond maps. We call a map \(f\) from a qoset \((X, \preceq)\) to \((\mathbb{Z}^d, \leq)\) diamond⁷ when for every \(x, a, b \in X\) such that \(x \sqsubseteq a, b\), there exists \(y \in X\) such that \(a, b \sqsubseteq y\) and \(f(x) + f(y) = f(a) + f(b)\).

A well-structured VAS (or WSVAS for short) is a triple \(\mathcal{V}\mathrel{\vcenter{:}}=(T, \sqsubseteq, \delta)\) where \((T, \sqsubseteq)\) is a wqo and \(\delta\) is an order-preserving and diamond map from \((T, \sqsubseteq)\) to \((\mathbb{Z}^d, \leq)\). Elements of \(T\) are called transitions. Given a transition \(t \in T\), the vector \(\delta(t) \in \mathbb{Z}^d\) is called the action of \(t\). Notice that every plain VAS \({\mathbf{A}} \subseteq \mathbb{Z}^d\) can be viewed as a WSVAS \((T, \sqsubseteq, \delta)\) by letting \(T\) be the finite set \({\mathbf{A}}\), \(\sqsubseteq\) be the equality relation on \({\mathbf{A}}\), and \(\delta\) be the identity function on \({\mathbf{A}}\).

We extend to WSVAS the usual semantic notions associated with VAS. This extension is natural, but we provide the details for the sake of completeness. Let us consider a WSVAS \(\mathcal{V}\mathrel{\vcenter{:}}=(T, \sqsubseteq, \delta)\) for the rest of this subsection. A configuration of \(\mathcal{V}\) is (as usual) a vector in \(\mathbb{N}^d\). A run of \(\mathcal{V}\) is a finite, non-empty, alternating sequence \(\rho \mathrel{\vcenter{:}}=({\mathbf{c}}_0, t_1, {\mathbf{c}}_1, \ldots, t_k, {\mathbf{c}}_k)\) of configurations \({\mathbf{c}}_i\) and transitions \(t_i\), satisfying \({\mathbf{c}}_i = {\mathbf{c}}_{i-1} + \delta(t_i)\) for all \(i \in \{1, \ldots, k\}\). We call \(k\) the length of \(\rho\), \({\mathbf{c}}_0\) the source of \(\rho\), written \(\operatorname{src}(\rho)\), and \({\mathbf{c}}_k\) the target of \(\rho\), written \(\operatorname{tgt}(\rho)\). The direction of \(\rho\) is the pair \(\operatorname{dir}(\rho) \mathrel{\vcenter{:}}=(\operatorname{src}(\rho), \operatorname{tgt}(\rho))\). The set of runs of \(\mathcal{V}\) is written \(\operatorname{Runs}(\mathcal{V})\). Given a set \({\mathbf{X}} \subseteq \mathbb{N}^d\), we let \(\operatorname{Reach}_{}({\mathbf{X}})\) denote the set of targets of runs \(\rho\) such that \(\operatorname{src}(\rho) \in {\mathbf{X}}\).

It is well-known that VAS runs can be equipped with a well-quasi-order [17], [37] that satisfies the amalgamation property [13]. This well-quasi-order can be lifted to WSVAS as follows. We introduce the binary relation \(\trianglelefteq\) on runs of \(\mathcal{V}\) defined by \(\rho \trianglelefteq \sigma\) if \(\rho = ({\mathbf{c}}_0, t_1, {\mathbf{c}}_1, \ldots, t_k, {\mathbf{c}}_k)\) and \(\sigma = \sigma_0 u_1 \sigma_1 \cdots u_k \sigma_k\) for some configurations \({\mathbf{c}}_0, \ldots, {\mathbf{c}}_k \in \mathbb{N}^d\), some runs \(\sigma_0, \ldots, \sigma_k \in \operatorname{Runs}(\mathcal{V})\) and some transitions \(t_1, \ldots, t_k, u_1, \ldots, u_k \in T\) such that \({\mathbf{c}}_i \leq \operatorname{src}(\sigma_i), \operatorname{tgt}(\sigma_i)\) for all \(i \in \{0, \ldots, k\}\) and \(t_i \sqsubseteq u_i\) for all \(i \in \{1, \ldots, k\}\). By lifting to WSVAS the proof arguments for VAS [13], [17], [37], we obtain that \(\trianglelefteq\) is a well-quasi-order that satisfies the amalgamation property, see [lem:wsvas-wqo-and-amalgamation] for the precise statement. The detailed proof of this lemma is deferred to 11 to avoid disrupting the flow of the paper.

Notice that \(\operatorname{dir}(\rho) \leq \operatorname{dir}(\sigma)\) for every runs \(\rho \trianglelefteq \sigma\). So an equivalent formulation of [lem:wsvas-wqo-and-amalgamation] is that the triple \((\operatorname{Runs}(\mathcal{V}), \trianglelefteq, \operatorname{dir}(\cdot))\) is itself a WSVAS (but of dimension \(2d\)). We conclude this subsection with a safe linearization lemma for WSVAS. This lemma will be used in 5.4 to prove our safe linearization lemma for BVAS.

5.2 From Branching VAS to Well-Structured VAS↩︎

This subsection shows how to simulate BVAS runs by WSVAS runs (see 16 below for a precise statement). We first introduce additional notations to clarify what we mean by simulation. The step relation of a WSVAS \(\mathcal{V}\mathrel{\vcenter{:}}=(T, \sqsubseteq, \delta)\) is the binary relation \(\xhookrightarrow{}_{\mathcal{V}}\) on \(\mathbb{N}^d\) defined by \({\mathbf{x}} \xhookrightarrow{}_{\mathcal{V}} {\mathbf{y}}\) if \({\mathbf{y}} = {\mathbf{x}} + \delta(t)\) for some \(t \in T\). Similarly, given a BVAS \(\mathcal{B}\mathrel{\vcenter{:}}=({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r)\) and a set \({\mathbf{I}}\subseteq \mathbb{N}^d\), the step relation of \(\mathcal{B}\) and \({\mathbf{I}}\) is the binary relation \(\xhookrightarrow{}_{\mathcal{B}, {\mathbf{I}}}\) on \(\mathbb{N}^d\) defined by \({\mathbf{x}} \xhookrightarrow{}_{\mathcal{B}, {\mathbf{I}}} {\mathbf{y}}\) if there exist \(n \in \{1, \ldots, r\}\) and \({\mathbf{a}} \in {\mathbf{\Delta}}_n\) such that \({\mathbf{y}} = {\mathbf{a}} + {\mathbf{x}} + \sum_{j=2}^n {\mathbf{c}}_j\) for some \({\mathbf{c}}_2, \ldots, {\mathbf{c}}_n \in {\mathbf{I}}\). We let \(\xhookrightarrow{*}_{\mathcal{V}}\) and \(\xhookrightarrow{*}_{\mathcal{B}, {\mathbf{I}}}\) denote the reflexive and transitive closure of \(\xhookrightarrow{}_{\mathcal{V}}\) and \(\xhookrightarrow{}_{\mathcal{B}, {\mathbf{I}}}\), respectively. Previously defined notations such as \(\operatorname{Reach}_{}(\cdot)\) and \(\trianglelefteq\) left the underlying system implicit. When the system under consideration is not clear from the context, we add it as a subscript to these notations to prevent confusion.

5.3 One Source Outside the Inductive Invariant Is Enough↩︎

In this subsection, we show that, under a technical condition, BVAS runs with multiple sources outside an inductive invariant are equivalent, reachability-wise, to runs with only one such source. This property is formally stated in 17 below. We consider a BVAS \(\mathcal{B}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r)\) for the rest of this subsection.

5.4 Proof of 13↩︎

We now have the required ingredients to prove 13. Consider an IBVAS \(\mathcal{S}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_0, \mathcal{B})\), two semilinear sets \({\mathbf{A}}, {\mathbf{T}} \subseteq \mathbb{N}^d\) and an almost linear set \({\mathbf{b}} + {\mathbf{P}} \subseteq \mathbb{N}^d\). Define \({\mathbf{I}}\mathrel{\vcenter{:}}= {\mathbf{A}} \cup \operatorname{Reach}_{}(\mathcal{S})\) and \({\mathbf{Q}} \mathrel{\vcenter{:}}= \overline{\operatorname{Lin}}({\mathbf{P}})\). Assume that \(\operatorname{Reach}_{\mathcal{B}}({\mathbf{I}}^+) \subseteq {\mathbf{I}}\) and that \(\operatorname{Reach}_{\mathcal{B}}(({\mathbf{b}} + {\mathbf{P}}) \,{\shuffle}\, {\mathbf{I}}^*) \subseteq {\mathbf{T}} \subseteq {\mathbf{I}}+ {\mathbf{Q}}\). To prove 13, we need to show that there exists \(p \in {\mathbf{P}}\) such that \(\operatorname{Reach}_{\mathcal{B}}(({\mathbf{b}} + {\mathbf{p}} + {\mathbf{Q}})^+ \,{\shuffle}\, {\mathbf{I}}^*) \subseteq {\mathbf{T}}\).

According to 16, there exists a WSVAS \(\mathcal{V}\) such that \(\xhookrightarrow{}_{\mathcal{B}, {\mathbf{I}}}\) and \(\xhookrightarrow{}_{\mathcal{V}}\) coincide. By 15, it holds that \(\operatorname{Reach}_{\mathcal{V}}({\mathbf{b}} + {\mathbf{P}}) = \operatorname{Reach}_{\mathcal{B}}(({\mathbf{b}} + {\mathbf{P}}) \,{\shuffle}\, {\mathbf{I}}^*) \subseteq {\mathbf{T}}\). We derive from 14 that there exists \({\mathbf{p}} \in {\mathbf{P}}\) satisfying \(\operatorname{Reach}_{\mathcal{V}}({\mathbf{b}} + {\mathbf{p}} + {\mathbf{Q}}) \subseteq {\mathbf{T}}\). Define \({\mathbf{X}} \mathrel{\vcenter{:}}={\mathbf{b}} + {\mathbf{p}} + {\mathbf{Q}}\). Using 15 once more, we get that \(\operatorname{Reach}_{\mathcal{B}}({\mathbf{X}} \,{\shuffle}\, {\mathbf{I}}^*) = \operatorname{Reach}_{\mathcal{V}}({\mathbf{X}}) \subseteq {\mathbf{T}}\). Note that \({\mathbf{X}} + {\mathbf{Q}} \subseteq {\mathbf{X}}\) and recall that \({\mathbf{T}} \subseteq {\mathbf{I}}+ {\mathbf{Q}}\). It follows from 17 that \(\operatorname{Reach}_{\mathcal{B}}({\mathbf{X}} \,{\shuffle}\, {\mathbf{I}}^*) = \operatorname{Reach}_{\mathcal{B}}({\mathbf{X}}^+ \,{\shuffle}\, {\mathbf{I}}^*)\), hence, \(\operatorname{Reach}_{\mathcal{B}}({\mathbf{X}}^+ \,{\shuffle}\, {\mathbf{I}}^*) = \operatorname{Reach}_{\mathcal{V}}({\mathbf{X}}) \subseteq {\mathbf{T}}\). This concludes the proof of 13.

6 Face-Stripping Theorem↩︎

Let \({\mathbf{Q}}\subseteq\mathbb{Z}^d\) be a full⁹ finitely-generated periodic set. In this section, we state and prove a way to decompose the difference of two finitary \({\mathbf{Q}}\)-cylindric sets \({\mathbf{X}}\subseteq{\mathbf{Y}}\subseteq \mathbb{Z}^d\). This decomposition, so-called the face-stripping theorem, is obtained by stripping \({\mathbf{Y}}\setminus {\mathbf{X}}\) following the faces (a classical notion recalled below) of the cone spanned by \({\mathbf{Q}}\). We first provide some definitions and then provide the statement of the main theorem and a central application of that result.

The orthogonal \({\mathbf{X}}^\perp\) of a set \({\mathbf{X}}\subseteq\mathbb{Q}^d\) is the set of vectors \({\mathbf{e}}\in\mathbb{Q}^d\) such that \({\mathbf{e}}\cdot{\mathbf{x}}=0\) for every \({\mathbf{x}}\in{\mathbf{X}}\) where \({\mathbf{e}}\cdot{\mathbf{x}}\) is the dot-product (see 2). Notice that \({\mathbf{X}}^\perp\) is a vector space. We say that a set \({\mathbf{F}}\subseteq \mathbb{Q}^d\) is a face of a finitely-generated cone \({\mathbf{C}}\subseteq\mathbb{Q}^d\) if \({\mathbf{F}}={\mathbf{C}}\cap{\mathbf{L}}^\perp\) for a finite set \({\mathbf{L}}\subseteq \mathbb{Q}^d\) of vectors \({\mathbf{e}}\in\mathbb{Q}^d\) satisfying \({\mathbf{e}}\cdot{\mathbf{c}}\geq 0\) for every \({\mathbf{c}}\in{\mathbf{C}}\). Since the intersection of a finitely-generated cone with a vector space is a finitely-generated cone, we deduce that a face is a finitely-generated cone. We denote by \(\mathcal{F}({\mathbf{C}})\) the set of faces of \({\mathbf{C}}\). Recall that \(\mathcal{F}({\mathbf{C}})\) is a finite set [39], \({\mathbf{C}}\in\mathcal{F}({\mathbf{C}})\) and for every face \({\mathbf{F}}\in \mathcal{F}({\mathbf{C}})\setminus\{{\mathbf{C}}\}\), we have \(\operatorname{dim}({\mathbf{F}}-{\mathbf{F}})<\operatorname{dim}({\mathbf{C}}-{\mathbf{C}})\)¹⁰.

Let \({\mathbf{Q}}\) be a full finitely-generated periodic set, let \({\mathbf{C}}\mathrel{\vcenter{:}}=\mathbb{Q}_{\geq 0}{\mathbf{Q}}\) be the finitely-generated cone spanned by \({\mathbf{Q}}\), and let \({\mathbf{F}}_1,\ldots,{\mathbf{F}}_n\) be a linearization of the set of faces of \({\mathbf{C}}\) with respect to \(\supseteq\). It follows that \(n=|\mathcal{F}({\mathbf{C}})|\), \(\mathcal{F}({\mathbf{C}})=\{{\mathbf{F}}_1,\ldots,{\mathbf{F}}_n\}\), \({\mathbf{F}}_1={\mathbf{C}}\), and \({\mathbf{F}}_i\supseteq {\mathbf{F}}_j\) implies \(i\leq j\).

We now prove the following central result satisfied by the decomposition given by the face-stripping theorem.

The remainder of this section is devoted to the proof of 2. Apart from this theorem and 18, the material presented in this section is not used in the sequel.

Let us fix a full finitely-generated periodic set \({\mathbf{Q}}\), and let \({\mathbf{C}}\mathrel{\vcenter{:}}=\mathbb{Q}_{\geq 0}{\mathbf{Q}}\) be the cone spanned by \({\mathbf{Q}}\). Since \({\mathbf{C}}\) is a finitely-generated cone, the Farkas-Minkowski-Weyl theorem [39] shows that there exists a finite set \({\mathbf{E}}\subseteq \mathbb{Z}^d\) satisfying the following equality. \[\label{eq:dual}{\mathbf{C}}=\{{\mathbf{c}}\in\mathbb{Q}^d \mid \bigwedge_{{\mathbf{e}}\in {\mathbf{E}}}{\mathbf{e}}\cdot{\mathbf{c}}\geq 0\}\tag{2}\] Recall from the Farkas lemma [39] that a set \({\mathbf{F}}\subseteq \mathbb{Q}^d\) is a face of \({\mathbf{C}}\) if, and only if, \({\mathbf{F}}={\mathbf{C}}\cap{\mathbf{L}}^\perp\) where \({\mathbf{L}}\mathrel{\vcenter{:}}={\mathbf{E}}\cap{\mathbf{F}}^\perp\). It follows that \(\mathcal{F}({\mathbf{C}})\) is finite since it contains at most \(2^{|{\mathbf{E}}|}\) faces, \({\mathbf{C}}\) is the \(\subseteq\)-maximal face of \({\mathbf{C}}\), and \({\mathbf{E}}^\perp\) is the \(\subseteq\)-minimal face of \({\mathbf{C}}\). Notice that the minimal face is a vector space.

We first introduce some folklore results.

Let \({\mathbf{X}}\subseteq {\mathbf{Y}}\subseteq \mathbb{Z}^d\) and \({\mathbf{F}}\) be a face of \({\mathbf{C}}\). We introduce the following \(({\mathbf{Q}}\cap{\mathbf{F}})\)-cylindric set: \[\operatorname{extract}_{{\mathbf{F}}}({\mathbf{X}},{\mathbf{Y}})\mathrel{\vcenter{:}}=\{{\mathbf{s}}\in\mathbb{Z}^d \mid {\mathbf{s}}+({\mathbf{Q}}\cap{\mathbf{F}})\subseteq {\mathbf{Y}}\setminus{\mathbf{X}}\}\]

Now, let \({\mathbf{F}}_1,\ldots,{\mathbf{F}}_n\) be a linearization of the set of faces of \({\mathbf{C}}\) with respect to \(\supseteq\). Let \({\mathbf{X}}\subseteq {\mathbf{Y}}\) be two finitary \({\mathbf{Q}}\)-cylindric subsets of \(\mathbb{Z}^d\), and let \({\mathbf{S}}_1,\ldots,{\mathbf{S}}_n\) be subsets of \(\mathbb{Z}^d\) defined inductively for every \(i\in \{1,\ldots,n\}\) as follows where \({\mathbf{S}}_{<i}\mathrel{\vcenter{:}}={\mathbf{S}}_1\cup\ldots\cup{\mathbf{S}}_{i-1}\): \[{\mathbf{S}}_i\mathrel{\vcenter{:}}=\operatorname{extract}_{{\mathbf{F}}_i}({\mathbf{Y}}\setminus {\mathbf{S}}_{<i},{\mathbf{X}})\]

We introduce the set \(\mathcal{M}_i\) of faces \({\mathbf{F}}\) such that \(\operatorname{extract}_{{\mathbf{F}}}({\mathbf{Y}}\setminus {\mathbf{S}}_{< i},{\mathbf{X}})\) is non-empty.

The \({\mathbf{Q}}\)-cylindric set \({\mathbf{Y}}\setminus {\mathbf{S}}_{< i}\) is finitary since it is included in the finitary \({\mathbf{Q}}\)-cylindric set \({\mathbf{Y}}\). Observe that if \({\mathbf{S}}_i\) is non-empty, since \(\mathcal{M}_{i}\subseteq \{{\mathbf{F}}_i,\ldots,{\mathbf{F}}_n\}\), we deduce that \({\mathbf{F}}_i\) is a \(\subseteq\)-maximal face such that \(\operatorname{extract}_{{\mathbf{F}}_i}({\mathbf{Y}}\setminus {\mathbf{S}}_{<i},{\mathbf{X}})\) is non-empty. 23 shows that \({\mathbf{S}}_i\) is a finitary \(({\mathbf{Q}}\cap{\mathbf{F}}_i)\)-cylindric set. Notice that this last property is also trivially true when \({\mathbf{S}}_i\) is empty. Clearly the sets \({\mathbf{S}}_1,\ldots,{\mathbf{S}}_n\) are pairwise-disjoint subsets of \({\mathbf{Y}}\setminus {\mathbf{X}}\). Moreover, since \(\mathcal{M}_{n+1}=\emptyset\), 22 shows that \(({\mathbf{Y}}\setminus{\mathbf{S}}_{< n+1})\setminus {\mathbf{X}}\) is empty. It follows that \({\mathbf{S}}_1,\ldots,{\mathbf{S}}_n\) is a disjoint decomposition of \({\mathbf{Y}}\setminus{\mathbf{X}}\).

Finally, assume that \({\mathbf{Y}}\subseteq {\mathbf{X}}-{\mathbf{Q}}\) and let us prove that \({\mathbf{S}}_1\) is empty. Recall that \({\mathbf{F}}_1={\mathbf{C}}\). It follows that if \({\mathbf{S}}_1\) is non-empty, there exists \({\mathbf{s}}\in\mathbb{Z}^d\) such that \({\mathbf{s}}+{\mathbf{Q}}\subseteq {\mathbf{Y}}\setminus{\mathbf{X}}\). As \({\mathbf{s}}\in{\mathbf{Y}}\subseteq {\mathbf{X}}-{\mathbf{Q}}\), there exists \({\mathbf{q}}\in{\mathbf{Q}}\) such that \({\mathbf{s}}+{\mathbf{q}}\in {\mathbf{X}}\). We get a contradiction. Hence \({\mathbf{S}}_1\) is empty.

We have proved 2.

7 From Safety Witnesses to Safe Semilinear Inductive Invariants↩︎

We are now equipped with the necessary ingredients to prove our main result, namely that every semilinear set \({\mathbf{\Phi}} \subseteq \mathbb{N}^d\) containing the reachability set of an IBVAS \(\mathcal{S}\) also contains a semilinear inductive invariant for \(\mathcal{S}\) (see 1). Let us consider, for the rest of this section, an IBVAS \(\mathcal{S}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_0, \mathcal{B})\) and a semilinear set \({\mathbf{\Phi}} \subseteq \mathbb{N}^d\) such that \(\operatorname{Reach}_{}(\mathcal{S}) \subseteq {\mathbf{\Phi}}\).

We first introduce a well-founded relation \(\Yleft\) on finite sets of directed iruns of \(\mathcal{S}\). The set \(\mathbb{N}^{d+1}\) is ordered by the strict lexicographic order \(<_{lex}\) defined by \((m_0, \ldots, m_d) <_{lex} (n_0, \ldots, n_d)\) if \((m_0, \ldots, m_d) \neq (n_0, \ldots, n_d)\) and the maximal¹² \(i\) such that \(m_i \neq n_i\) satisfies \(m_i < n_i\). We associate with a directed irun \(w \mathrel{\vcenter{:}}= (\rho_w, {\mathbf{C}}_w)\) the vector \(\operatorname{rank}(w) \mathrel{\vcenter{:}}= (n_0, \ldots, n_d) \in \mathbb{N}^{d+1}\) defined by \(n_j = 1\) if \(j = \operatorname{dim}({\mathbf{C}}_w - {\mathbf{C}}_w)\), and \(n_j = 0\) otherwise. For every finite set \(W\) of directed iruns, we let \(\operatorname{rank}(W) \mathrel{\vcenter{:}}= \sum_{w \in W} \operatorname{rank}(w)\). The binary relation \(\Yleft\) on finite sets of directed iruns is defined by \(V \Yleft W\) if \(\operatorname{rank}(V) <_{lex} \operatorname{rank}(W)\). It is readily seen that \(\Yleft\) is a well-founded relation (i.e., there is no infinite sequence \(W_0, W_1, W_2, \ldots\) with \(W_{i+1} \Yleft W_i\) for all \(i\)).

We observe that for every semilinear set \({\mathbf{A}} \subseteq \mathbb{N}^d\), the pair \(({\mathbf{A}}, \emptyset)\) is a safety witness for \(\mathcal{S}\) and \({\mathbf{\Phi}}\) if, and only if, the set \({\mathbf{A}}\) is an inductive invariant for \(\mathcal{S}\) such that \({\mathbf{A}} \subseteq {\mathbf{\Phi}}\). We have already shown in 3 that there exists a safety witness for \(\mathcal{S}\) and \({\mathbf{\Phi}}\). The remainder of this section proves the key property stated in 25 (and already mentioned in 3). As \(\Yleft\) is well-founded, this entails that a safety witness of the form \(({\mathbf{A}}, \emptyset)\) exists, and concludes the proof of 1.

As we hinted before, our proof of 25 uses 13 2. We also rely on the two following technical lemmas. The first one, 26, will help us show the premises of 13. The second one, 27, provides a sufficient condition for an attractor to “touch” a directed irun.

Let us now prove 25. Consider a safety witness \(({\mathbf{A}}, W)\) for \(\mathcal{S}\) and \({\mathbf{\Phi}}\), and assume that \(W \neq \emptyset\). As in the overview presented at the end of 3, we pick an arbitrary bottom SCC \(\Gamma\) of the graph \((W, \twoheadrightarrow_{W})\) and we introduce the finitary \({\mathbf{Q}}_\Gamma\)-cylindric set \({\mathbf{Y}}_\Gamma \mathrel{\vcenter{:}}= \{\operatorname{tgt}(\rho_\gamma) \mid \gamma \in \Gamma\} + {\mathbf{Q}}_\Gamma\). Put \({\mathbf{I}}\mathrel{\vcenter{:}}= {\mathbf{A}} \cup \operatorname{Reach}_{}(\mathcal{S})\) and \({\mathbf{T}} \mathrel{\vcenter{:}}={\mathbf{A}} \cup ({\mathbf{Y}}_\Gamma \cap {\mathbf{\Phi}})\). Observe that \({\mathbf{I}}\) is an inductive invariant for \(\mathcal{S}\) since \({\mathbf{A}}\) is an attractor for \(\mathcal{S}\), and that \({\mathbf{T}}\) is semilinear since \({\mathbf{A}}\), \({\mathbf{Y}}_\Gamma\) and \({\mathbf{\Phi}}\) are semilinear. Pick a directed irun \(w \in \Gamma\). We will apply 13 to the set \(\operatorname{tgt}(\operatorname{IRuns}(w)) = \operatorname{tgt}(\rho_w) + {\mathbf{P}}_w\), which is almost linear (see 4.2). To do so, we need to show that \(\operatorname{Reach}_{}(\operatorname{tgt}(\operatorname{IRuns}(w)) \,{\shuffle}\, {\mathbf{I}}^*) \subseteq {\mathbf{T}}\) and \({\mathbf{T}} \subseteq {\mathbf{I}}+ {\mathbf{Q}}_w\). The second inclusion follows from the observations that \({\mathbf{T}} \subseteq {\mathbf{A}} \cup {\mathbf{Y}}_\Gamma\), \({\mathbf{Y}}_\Gamma \subseteq \operatorname{Reach}_{}(\mathcal{S}) + {\mathbf{Q}}_\Gamma\) and \({\mathbf{Q}}_w = {\mathbf{Q}}_\Gamma\) since \(w \in \Gamma\). The first inclusion follows from the following relationships: \[\begin{align} \operatorname{Reach}_{}(\operatorname{tgt}(\operatorname{IRuns}(w)) \,{\shuffle}\, {\mathbf{I}}^*) & = \operatorname{Reach}_{}({\mathbf{A}}^* \,{\shuffle}\, \operatorname{tgt}(\operatorname{IRuns}(w)) \,{\shuffle}\, \operatorname{Reach}_{}(\mathcal{S})^*) & [{\mathbf{I}}= {\mathbf{A}} \cup \operatorname{Reach}_{}(\mathcal{S})] \\ & \subseteq {\mathbf{A}} \cup \operatorname{Reach}_{}(\operatorname{tgt}(\operatorname{IRuns}(w)) \,{\shuffle}\, \operatorname{Reach}_{}(\mathcal{S})^*) & [{\mathbf{A}} \text{ is an attractor}] \\ & \subseteq {\mathbf{A}} \cup \operatorname{Reach}_{}(\operatorname{tgt}(\operatorname{IRuns}(w)) \,{\shuffle}\, {\mathbf{\Delta}}_0^*) & [\text{\ref{fact:reach-shuffle}}] \\ & \subseteq {\mathbf{A}} \cup \bigcup_{\gamma \in \Gamma} \operatorname{tgt}(\operatorname{IRuns}(\gamma)) & [\text{\ref{lem:safety-witness-succ}}] \\ & \subseteq {\mathbf{A}} \cup ({\mathbf{Y}}_\Gamma \cap {\mathbf{\Phi}}) & [\text{see below}] \\ & = {\mathbf{T}} \end{align}\] The last inclusion holds because for every \(\gamma \in \Gamma\), we have \(\operatorname{tgt}(\operatorname{IRuns}(\gamma)) \subseteq \operatorname{Reach}_{}(\mathcal{S}) \subseteq {\mathbf{\Phi}}\) and \(\operatorname{tgt}(\operatorname{IRuns}(\gamma)) = \operatorname{tgt}(\rho_\gamma) + {\mathbf{P}}_\gamma \subseteq \operatorname{tgt}(\rho_\gamma) + {\mathbf{Q}}_\gamma \subseteq {\mathbf{Y}}_\Gamma\). According to 13, there exists \(p \in {\mathbf{P}}_w\) such that \(\operatorname{Reach}_{}((\operatorname{tgt}(\rho_w) + {\mathbf{p}} + {\mathbf{Q}}_w)^+ \,{\shuffle}\, {\mathbf{I}}^*) \subseteq {\mathbf{T}}\). We define \({\mathbf{R}} \mathrel{\vcenter{:}}= \operatorname{Reach}_{}((\operatorname{tgt}(\rho_w) + {\mathbf{p}} + {\mathbf{Q}}_w)^+ \,{\shuffle}\, {\mathbf{I}}^*)\) and \({\mathbf{X}} \mathrel{\vcenter{:}}= {\mathbf{R}} \cap {\mathbf{Y}}_\Gamma\). Let us show that the set \({\mathbf{X}}\) enjoys the properties claimed in the overview presented at the end of 3.

• By monotony of BVAS runs (see [fact:monotony]), the set \({\mathbf{R}}\) is \({\mathbf{Q}}_w\)-cylindric. Recall that \({\mathbf{Q}}_w = {\mathbf{Q}}_\Gamma\) since \(w \in \Gamma\). It follows that \({\mathbf{X}}\) is finitary \({\mathbf{Q}}_\Gamma\)-cylindric since it is the intersection of the \({\mathbf{Q}}_\Gamma\)-cylindric set \({\mathbf{R}}\) and the finitary \({\mathbf{Q}}_\Gamma\)-cylindric set \({\mathbf{Y}}_\Gamma\). This entails, in particular, that \({\mathbf{X}}\) is semilinear.

• We have \({\mathbf{X}} \subseteq {\mathbf{\Phi}}\) since \({\mathbf{X}} \subseteq {\mathbf{R}} \subseteq {\mathbf{T}} \subseteq {\mathbf{A}} \cup {\mathbf{\Phi}}\) and \({\mathbf{A}} \subseteq {\mathbf{\Phi}}\) as \(({\mathbf{A}}, W)\) is a safety witness.

• The set \({\mathbf{A}} \cup {\mathbf{R}}\) is an attractor for \(\mathcal{S}\) by 1. Since \({\mathbf{R}} \subseteq {\mathbf{T}} \subseteq {\mathbf{A}} \cup {\mathbf{Y}}_\Gamma\), we derive that \({\mathbf{A}} \cup {\mathbf{R}} = {\mathbf{A}} \cup ({\mathbf{R}} \cap {\mathbf{Y}}_\Gamma) = {\mathbf{A}} \cup {\mathbf{X}}\). Therefore, the set \({\mathbf{A}} \cup {\mathbf{X}}\) is an attractor for \(\mathcal{S}\).

• The set \({\mathbf{R}}\) is an attractor for \(\mathcal{S}\) by 1 (applied with \({\mathbf{A}} \mathrel{\vcenter{:}}= \emptyset\)). As mentioned above, \({\mathbf{R}}\) is \({\mathbf{Q}}_\Gamma\)-cylindric. Note that \({\mathbf{R}}\) intersects \(\operatorname{tgt}(\rho_w) + {\mathbf{Q}}_\Gamma\) since \({\mathbf{R}}\) contains \(\operatorname{tgt}(\rho_w) + {\mathbf{p}}\) and \({\mathbf{p}} \in {\mathbf{P}}_w \subseteq {\mathbf{Q}}_w = {\mathbf{Q}}_\Gamma\). It follows from 27 that \(\operatorname{tgt}(\rho_\gamma)\) is in \({\mathbf{R}} - {\mathbf{Q}}_\Gamma\) for every \(\gamma \in \Gamma\). We derive from \({\mathbf{R}} + {\mathbf{Q}}_\Gamma \subseteq {\mathbf{R}}\) and \({\mathbf{X}} = {\mathbf{R}} \cap {\mathbf{Y}}_\Gamma\) that \({\mathbf{Y}}_\Gamma \subseteq {\mathbf{X}} - {\mathbf{Q}}_\Gamma\).

• For every \({\mathbf{r}} \in {\mathbf{R}}\) and \({\mathbf{y}} \in \mathbb{N}^d\) such that \({\mathbf{r}} \xrightarrow{\mathcal{S}} {\mathbf{y}}\), we have \({\mathbf{y}} \in \operatorname{Reach}_{}({\mathbf{R}} \,{\shuffle}\, {\mathbf{\Delta}}_0^*)\), hence, \({\mathbf{y}} \in {\mathbf{R}}\) as \({\mathbf{R}}\) is an attractor (see above). Since \({\mathbf{X}} = {\mathbf{R}} \cap {\mathbf{Y}}_\Gamma\), we derive that the binary relation \(\xrightarrow{\mathcal{S}}\) has an empty intersection with \({\mathbf{X}} \times ({\mathbf{Y}}_\Gamma \setminus {\mathbf{X}})\).

To summarize what we have done so far, we have constructed a finitary \({\mathbf{Q}}_\Gamma\)-cylindric set \({\mathbf{X}} \subseteq {\mathbf{Y}}_{\Gamma}\) such that firstly \({\mathbf{A}}' \mathrel{\vcenter{:}}= {\mathbf{A}} \cup {\mathbf{X}}\) is a semilinear attractor for \(\mathcal{S}\) contained in \({\mathbf{\Phi}}\), secondly \({\mathbf{Y}}_\Gamma \subseteq {\mathbf{X}} - {\mathbf{Q}}_\Gamma\), and thirdly \(\xrightarrow{\mathcal{S}}\) has an empty intersection with \({\mathbf{X}} \times ({\mathbf{Y}}_\Gamma \setminus {\mathbf{X}})\).

Before introducing the set \(W'\) of directed iruns, we first prove the following lemma.

Let us recall that \({\mathbf{C}}_\Gamma\) is the finitely-generated cone satisfying \({\mathbf{C}}_\gamma={\mathbf{C}}_\Gamma\) for every \(\gamma\in \Gamma\). We introduce the finitely-generated cone \({\mathbf{C}}\mathrel{\vcenter{:}}=\operatorname{Con}({\mathbf{Q}}_\Gamma)\). From \({\mathbf{Q}}_\Gamma\subseteq {\mathbf{C}}_\Gamma\) we derive \({\mathbf{C}}\subseteq {\mathbf{C}}_\Gamma\). Let us fix a linearization \({\mathbf{F}}_1,\ldots,{\mathbf{F}}_n\) of the set of faces of \({\mathbf{C}}\) with respect to \(\supseteq\). It follows that \(n=|\mathcal{F}({\mathbf{C}})|\), \(\mathcal{F}({\mathbf{C}})=\{{\mathbf{F}}_1,\ldots,{\mathbf{F}}_n\}\), \({\mathbf{F}}_1={\mathbf{C}}\), and \({\mathbf{F}}_i\supseteq {\mathbf{F}}_j\) implies \(i\leq j\). We introduce the sequence \({\mathbf{S}}_1,\ldots,{\mathbf{S}}_n\) of subsets of \(\mathbb{Z}^d\) defined inductively for every \(i\in \{1,\ldots,n\}\) as follows where \({\mathbf{S}}_{<i}\mathrel{\vcenter{:}}={\mathbf{S}}_1\cup\ldots\cup{\mathbf{S}}_{i-1}\): \[{\mathbf{S}}_i\mathrel{\vcenter{:}}=\{{\mathbf{s}}\in\mathbb{Z}^d \mid {\mathbf{s}}+({\mathbf{Q}}\cap{\mathbf{F}}_i)\subseteq ({\mathbf{Y}}\setminus{\mathbf{S}}_{<i})\setminus {\mathbf{X}}\}\] Since \({\mathbf{X}} \subseteq {\mathbf{Y}}_{\Gamma}\) are finitary \({\mathbf{Q}}_\Gamma\)-cylindric, 2 shows that \({\mathbf{S}}_1,\ldots,{\mathbf{S}}_n\) is a disjoint decomposition of \({\mathbf{Y}}_\Gamma\setminus{\mathbf{X}}\) such that \({\mathbf{S}}_i\) is a finitary \(({\mathbf{Q}}\cap{\mathbf{F}}_i)\)-cylindric set for every \(1\leq i\leq n\). Moreover, since \({\mathbf{Y}}_\Gamma\subseteq{\mathbf{X}}-{\mathbf{Q}}_\Gamma\), we deduce that \({\mathbf{S}}_1\) is empty.

Let \(i\in\{2,\ldots,n\}\) and let us introduce the finitely-generated periodic set \({\mathbf{Q}}_i\mathrel{\vcenter{:}}={\mathbf{Q}}_\Gamma\cap {\mathbf{F}}_i\) and the set \(R_i\mathrel{\vcenter{:}}=\{\rho\in \operatorname{IRuns}(\Gamma)\mid \operatorname{tgt}(\rho)\in {\mathbf{S}}_i\}\). We denote by \(\leq_i\) the partial order \(\leq_{{\mathbf{Q}}_i}\). Since \({\mathbf{Q}}_i\) is a finitely-generated periodic set and \({\mathbf{S}}_i\) is a finitary \({\mathbf{Q}}_i\)-cylindric set, we deduce that \(\leq_i\) is a wpo on \({\mathbf{S}}_i\). We also introduce the partial order \(\trianglelefteq_i\) over \(R_i\) defined by \(\rho\trianglelefteq_i\sigma\) if \(\rho\trianglelefteq \sigma\) and \(\operatorname{tgt}(\rho)\leq_i\operatorname{tgt}(\sigma)\). Since \(\trianglelefteq\) is a wpo on \(\operatorname{IRuns}(\mathcal{S})\) and \(\leq_i\) is a wpo on \({\mathbf{S}}_i\), we deduce that \(\trianglelefteq_i\) is a wpo on \(R_i\). We introduce the finite set \(W_i\) of directed iruns \((\rho,F_i)\) where \(\rho\in\operatorname{Min}_{\trianglelefteq_i}(R_i)\). We are going to prove that the pair \(({\mathbf{A}}',W')\) is a safety witness satisfying 25 where \(W'\) is the following set of directed iruns. \[W'\mathrel{\vcenter{:}}= (W\setminus \Gamma)\cup \bigcup_{i=2}^n W_i\]

Let us first prove that \(W' \Yleft W\). We introduce \(i_\Gamma\mathrel{\vcenter{:}}=\operatorname{dim}({\mathbf{C}}_\Gamma-{\mathbf{C}}_\Gamma)\), and the natural numbers \(n_0,\ldots,n_d,n_0',\ldots,n_d'\) such that \(\operatorname{rank}(W)=(n_0,\ldots,n_d)\) and \(\operatorname{rank}(W')=(n_0',\ldots,n_d')\). Recall from 6 that \(\operatorname{dim}({\mathbf{F}}_i-{\mathbf{F}}_i)<\operatorname{dim}({\mathbf{C}}-{\mathbf{C}})\) for every \(i\in\{2,\ldots,n\}\). Moreover, since \({\mathbf{C}}\subseteq {\mathbf{C}}_\Gamma\), we deduce that \(\operatorname{dim}({\mathbf{F}}_i-{\mathbf{F}}_i)<i_\Gamma\). It follows that \(n'_{i_\Gamma}=n_{i_\Gamma}-|\Gamma|\) where \(|\Gamma|\) denotes the cardinal of \(\Gamma\), and \(n'_i=n_i\) for every \(i\in \{i_\Gamma+1,\ldots,d\}\). We deduce that \(\operatorname{rank}(W') <_{lex} \operatorname{rank}(W)\). Therefore \(W' \Yleft W\) as claimed.

Since \(W\) is homogeneous, we deduce from the following lemma that \(W'\) is homogeneous as well.

In order to prove that \(({\mathbf{A}}',W')\) is a safety witness for \(\mathcal{S}\) and \({\mathbf{\Phi}}\), it just remain to prove that for every irun \(\rho \in \operatorname{IRuns}(\mathcal{S})\), we have \(\operatorname{tgt}(\rho) \in {\mathbf{A}}'\) or \(\rho \in \operatorname{IRuns}(W')\). So, let \(\rho\in \operatorname{IRuns}(\mathcal{S})\) such that \(\operatorname{tgt}(\rho)\not\in {\mathbf{A}}'\). As \(({\mathbf{A}},W)\) is a safety witness and \(\operatorname{tgt}(\rho)\not\in{\mathbf{A}}\) we deduce that there exists \(w\in W\) such that \(\rho\in \operatorname{IRuns}(w)\). Clearly, if \(w\not\in \Gamma\) then \(w\in W'\) and in particular \(\rho\in \operatorname{IRuns}(W')\). So, let us assume that \(\rho\in \operatorname{IRuns}(\Gamma)\). It follows that \(\operatorname{tgt}(\rho)\in {\mathbf{Y}}_\Gamma\). If \(\operatorname{tgt}(\rho)\in {\mathbf{X}}\) then \(\operatorname{tgt}(\rho)\in{\mathbf{A}}'\), so we can assume that \(\operatorname{tgt}(\rho)\not\in {\mathbf{X}}\). Hence \(\operatorname{tgt}(\rho)\in {\mathbf{Y}}_\Gamma\setminus{\mathbf{X}}\). As \({\mathbf{S}}_2,\ldots,{\mathbf{S}}_n\) is a disjoint decomposition of \({\mathbf{Y}}_\Gamma\setminus {\mathbf{X}}\), there exists \(i\in\{2,\ldots,n\}\) such that \(\operatorname{tgt}(\rho)\in {\mathbf{S}}_i\). Hence \(\rho\in R_i\). We deduce that there exists \(u\in W_i\) such that \(\rho_u\trianglelefteq_i \rho\). In particular \(\rho_u\trianglelefteq \rho\) and \(\operatorname{tgt}(\rho)\in \operatorname{tgt}(\rho_u)+{\mathbf{F}}_i\). We deduce that \(\rho\in\operatorname{IRuns}(u)\subseteq \operatorname{IRuns}(W')\). We have proved that \(({\mathbf{A}}',W')\) is a safety witness for \(\mathcal{S}\) and \({\mathbf{\Phi}}\). We have proved 25.

8 Conclusion↩︎

We have established the decidability of reachability in branching vector addition systems, resolving a problem that has remained open for more than three decades.

Several questions remain open. First, our argument does not provide any complexity upper bound. For plain VAS, a complexity analysis of the invariant-based approach is known but it is based on the computational complexity of the KLM algorithm. Determining the complexity of BVAS reachability therefore appears to require new ideas, and perhaps fundamentally different algorithms. At present, even in dimension five, where decidability was previously established [22], no non-trivial complexity upper bound is known. Likewise, the best lower bound currently known is the Ackermann lower bound inherited from VAS reachability.

A second natural direction concerns extended BVAS (EBVAS), introduced in [5] as a counter automaton equivalent to two-variable first-order logic over data trees, and later connected in [9] to the observational equivalence problem for a finitary fragment of ML. The model of EBVAS enriches branching transitions with additional resource-transfer mechanisms, and is believed to be strictly more expressive than BVAS. The decidability of reachability for EBVAS remains open and, to the best of our knowledge, has not yet been systematically investigated. From the perspective of the present work, a first challenge would be to determine whether EBVAS have almost semilinear reachability set and whether this could be proved with the same approach as in [22].

9 Proof of [lem:fgper-wqo-on-Zd]↩︎

10 Well-Partial-Order on Iruns of an Initialized BVAS and Amalgamation Property↩︎

This appendix provides a detailed proof of [lem:ibvas-wpo-and-amalgamation]. As mentioned in 3, this lemma was proved in [22] with slightly different notations. We reprove it because our approach crucially relies on it.

Let us consider an IBVAS \(\mathcal{S}\mathrel{\vcenter{:}}=({\mathbf{\Delta}}_0, \mathcal{B})\) where \(\mathcal{B}\mathrel{\vcenter{:}}= ({\mathbf{\Delta}}_1, \ldots, {\mathbf{\Delta}}_r)\). To prove [lem:ibvas-wpo-and-amalgamation], we show that \((\operatorname{IRuns}(\mathcal{S}), \trianglelefteq)\) is a wpo (see 30) and that it satisfies the amalgamation property (see 31).

11 Well-Quasi-Order on Runs of a Well-Structured VAS and Amalgamation Property↩︎

This appendix provides the detailed proof of [lem:wsvas-wqo-and-amalgamation]. As mentioned in 5.1, we essentially lift to WSVAS existing proof arguments for VAS [13], [17], [37].

Let us consider a WSVAS \(\mathcal{V}\mathrel{\vcenter{:}}=(T, \sqsubseteq, \delta)\). To prove [lem:wsvas-wqo-and-amalgamation], we show that \((\operatorname{Runs}(\mathcal{V}), \trianglelefteq)\) is a wqo (see 3) and that it satisfies the amalgamation property (see 33).

The binary relation \(\trianglelefteq\) can be characterized in terms of subsequence embedding. Recall that for every qoset \((\Sigma, \preceq)\), the subsequence embedding is the quasi-order \(\preceq^*\) on \(\Sigma^*\) defined by \(u \preceq^* v\) if \(u = a_1 \cdots a_k\) and \(v = v_0 b_1 v_1 \cdots b_k v_k\) for some \(v_i \in \Sigma^*\) and \(a_i, b_i \in \Sigma\) such that \(a_i \preceq b_i\). To characterize \(\trianglelefteq\) in terms of \(\preceq^*\), we consider the alphabet \(\Sigma = \mathbb{N}^d \times T \times \mathbb{N}^d\) equipped with the quasi-order \(\preceq\) on \(\Sigma\) defined by \(({\mathbf{x}}, t, {\mathbf{y}}) \preceq ({\mathbf{x}}', t', {\mathbf{y}}')\) if \({\mathbf{x}} \leq {\mathbf{x}}'\), \(t \sqsubseteq t'\) and \({\mathbf{y}} \leq {\mathbf{y}}'\). The encoding of a run \(\rho \mathrel{\vcenter{:}}=({\mathbf{c}}_0, t_1, {\mathbf{c}}_1, \ldots, t_k, {\mathbf{c}}_k)\), written \(\langle \rho \rangle\), is the sequence in \(\Sigma^*\) defined by \(\langle \rho \rangle \mathrel{\vcenter{:}}=({\mathbf{c}}_0, t_1, {\mathbf{c}}_1) \cdots ({\mathbf{c}}_{k-1}, t_k, {\mathbf{c}}_k)\). Note that \(\langle \rho \rangle\) is the empty sequence if \(\rho\) has length zero.

References↩︎

---

1. Our definition of full periodic set slightly generalizes the one given in [36] since the cone \({\mathbf{C}}\) is not required to be finitely-generated in our case.↩︎

2. In the literature, BVAS runs are classically defined as unordered rooted trees whose nodes are labeled by configurations [2]. We choose an inductive, term-based definition as it simplifies some definitions and some proofs. Our term-based definition is clearly equivalent (for reachability) to the classical tree-based definition.↩︎

3. It is understood that \(\operatorname{tgt}(R)\mathrel{\vcenter{:}}=\{\operatorname{tgt}(\rho)\mid \rho\in R\}\) for every set of runs \(R\).↩︎

4. A disjoint decomposition of a set \(X\) is a partition of \(X\) that allows the emptyset, i.e., a finite sequence \(X_1,\ldots,X_n\) of subsets of \(X\) such that \(X=X_1\cup\cdots\cup X_n\) and \(X_i\cap X_j=\emptyset\) for every \(i\neq j\).↩︎

5. The same proof shows that \(\operatorname{Con}(\pi({\mathbf{R}}))=\pi(\operatorname{Con}({\mathbf{R}}))\) for any linear mapping \(\pi\).↩︎

6. Recall that by definition \({\mathbf{P}}_\rho = \{\operatorname{tgt}(\sigma) - \operatorname{tgt}(\rho) \mid \sigma \in \operatorname{IRuns}(\mathcal{S})\wedge \rho\trianglelefteq \sigma\}\).↩︎

7. The name diamond comes from the observation that if \(x \sqsubseteq a, b \sqsubseteq y\) and \(f(x) + f(y) = f(a) + f(b)\) then the differences \(d_{xa} = f(a) - f(x)\), \(d_{xb} = f(b) - f(x)\), \(d_{ay} = f(y) - f(a)\) and \(d_{by} = f(y) - f(b)\) satisfy \(d_{xa} = d_{by}\) and \(d_{xb} = d_{ay}\).↩︎

8. A binary relation \(R\) on a set \(X\) is almost-full [38] if for every infinite sequence \((x_n)_{n\in\mathbb{N}}\) of elements in \(X\), there exists \(m<n\) such that \((x_m, x_n) \in R\). Note that a qoset \((X, \preceq)\) is a wqo if, and only if, \(\preceq\) is almost-full.↩︎

9. See [rem:full] for details.↩︎

10. Since \({\mathbf{F}}={\mathbf{C}}\cap{\mathbf{L}}^\perp\) and \({\mathbf{F}}\not={\mathbf{C}}\) we deduce that the vector space \({\mathbf{V}}\mathrel{\vcenter{:}}={\mathbf{C}}-{\mathbf{C}}\) cannot be included in \({\mathbf{L}}^\perp\). In particular the vector space \({\mathbf{W}}\mathrel{\vcenter{:}}=({\mathbf{F}}-{\mathbf{F}})\cap{\mathbf{L}}^\perp\) is strictly included in \({\mathbf{V}}\). As \({\mathbf{W}}\subsetneq {\mathbf{V}}\) we deduce that \(\operatorname{dim}({\mathbf{W}})<\operatorname{dim}({\mathbf{V}})\).↩︎

11. See 2 for the definition.↩︎

12. In the usual definition of \(<_{lex}\), the condition \(m_i < n_i\) must hold for the minimal \(i\) such that \(m_i \neq n_i\). In our definition, we consider the maximal such \(i\), as it is more convenient for our purposes.↩︎

13. See [par:diagonal] for the definition of diagonal relations.↩︎