University of Warsaw, Polandhttps://orcid.org/0009-0004-1641-9049 Partially
supported by NCN grant 2017/27/B/ST6/02093. University of Warsaw,
Polandhttps://orcid.org/0000-0001-8674-4470 Partially supported by NCN grant
2017/27/B/ST6/02093 and by the ERC grant INFSYS, agreement no. 950398. Łukasz
Kamiński and Sławomir Lasota <ccs2012> <concept>
<concept_id>10003752.10003753.10003761.10003763</concept_id>
<concept_desc>Theory of computation Distributed computing
models</concept_desc> <concept_significance>500</concept_significance>
</concept> </ccs2012> [500]Theory of computation Distributed computing models

###### Acknowledgements.

We are grateful to Piotrek Hofman for inspiring discussions. 2 42 1

# Bi-reachability in Petri nets with data

Łukasz Kamiński  Sławomir Lasota

###### Abstract

We investigate Petri nets with data, an extension of plain Petri nets where
tokens carry values from an infinite data domain, and executability of
transitions is conditioned by equalities between data values. We provide a
decision procedure for the bi-reachability problem: given a Petri net and its
two configurations, we ask if each of the configurations is reachable from the
other. This pushes forward the decidability borderline, as the bi-reachability
problem subsumes the coverability problem (which is known to be decidable) and
is subsumed by the reachability problem (whose decidability status is
unknown).

###### keywords:

Petri nets, Petri nets with data, reachability, bi-reachability, orbit-finite
sets

##  1 Introduction

We investigate the model of Petri nets with data, where tokens carry values
from some fixed data domain, and executability of transitions is conditioned
by relations between data values involved. We study Petri nets with _equality_
data [17, 19, 25], i.e., an infinite data domain with equality as the only
relation. Other data domain have been also studied, for instance Petri nets
with _ordered_ data [19], i.e., an infinite countable, densely and totally
ordered data domain. This model clearly subsumes Petri nets with equality
data. One can also consider an abstract setting of Petri nets over an
arbitrary fixed data domain $\mathbb{A}$ [17].

As an illustrating example, consider a Petri net with equality data with two
places $p_{1},p_{2}$ and two transitions $t_{1},t_{2}$ depicted in Fig. 1.
Transition $t_{1}$ outputs two tokens with arbitrary but distinct data values
onto place $p_{1}$. Transition $t_{2}$ inputs two tokens with the same data
value, say $a$, one from $p_{1}$ and one from $p_{2}$, and outputs three
tokens: two tokens with arbitrary but equal data values $b$, where $b\neq a$,
one onto $p_{1}$ and the other onto $p_{2}$, plus one token with a data value
$c\neq a$ onto $p_{1}$. Note that transition $t_{2}$ does not specify whether
$b=c$ or not, and therefore both options are allowed.

$p_{1}$$p_{2}$$t_{1}$$x_{1},x_{2}$$t_{2}$$y_{1}$$y_{2}$$z_{1},z_{3}$$z_{2}$$x_{1}\neq
x_{2}$$z_{1}=z_{2}\neq y_{1}=y_{2}\neq z_{3}$ Figure 1: A Petri net with
equality data, with places $\left\\{p_{1},p_{2}\right\\}$ and transitions
$\left\\{t_{1},t_{2}\right\\}$. The shown configuration engages 5 tokens,
carrying 3 different data values, depicted through differently colors.

The most fundamental decision problem for Petri nets, the _reachability_
problem, asks, given a net together with source and target configurations, if
there is a run from source to target. It is well known that the reachability
problem is undecidable for Petri nets with ordered data [19], while the
decidability status of this problem for equality data still remains an
intriguing open question. On the other hand, the _coverability_ problem (where
we ask if there is a run from source to a configuration that possibly extends
target by some extra tokens) is decidable for both equality and ordered data
[17]. As widely known, coverability easily reduces to reachability.
Furthermore, the reachability problem is decidable, also for equality and
ordered data, in the special case of _reversible_ Petri nets (where
transitions are closed under reverse), as recently shown in [12].

In this paper we study a relevant decision problem, sandwiched between
reachability and the two latter decidable ones: the _bi-reachability_ problem.
It asks, for a net and two its configurations, if each of the configurations
is reachable from the other one. In other words, the problem asks if two given
configurations are in the same bi-reachability equivalence class. Here are all
know reductions, valid for Petri with with either equality or ordered data, as
well as for plain Petri nets (without data):

coverability  bi-reachability  reachability  reachability in reversible Petri
nets

As our main result we prove decidability of this problem for equality data
domain. This pushes further the decidability border for Petri nets with
equality data, subsuming decidability of coverability, and of reachability in
reversible Petri nets with equality data. Our approach is specific to equality
data, and thus we leave unresolved the status of bi-reachability in case of
ordered data.

The decision procedure for bi-reachability is inspired by the classical
decomposition approach used to decide reachability in plain Petri nets [15,
16, 24]. There, it is often more convenient to work with _vector addition
systems with states_ (vass) instead of Petri nets [15, 24]. Following this
line, for technical convenience we prefer to work with the model of _data
vass_ (dvass) [13] rather than with Petri nets. In short, our approach
consists of two ingredients. First, we provide a sufficient condition for a
dvass to admit bi-reachability (resembling $\Theta_{1}$ and $\Theta_{2}$
conditions of [15, 24]), which is effectively testable. Second, in case the
condition fails, we provide an effective way of reducing a dvass to an
equivalent one, with respect to bi-reachability, which has smaller _rank_. As
ranks are well founded, the reduction step guarantees correctness and
termination. Importantly, the decision procedure manipulates dvass, and does
not need to resort to manipulation of more general structures (like
generalised vass of [15, 24], or graph-transition sequences of [16], or
witness graph sequences of [22], or KLM sequences of [23]). This allows us to
avoid similar generalisations in the data setting, and allows to keep the
algorithm relatively simple.

Our work leaves two exciting open questions: can one extend our approach to
bi-reachability in case of ordered data, or to reachability in case of
equality data. Clearly, if attempting to solve the latter problem, one
unavoidably will be faced with some generalisation of the above-mentioned
structures to the data setting.

#### Related research.

Petri nets with data can be seen as a reinterpretation of the classical
definition of Petri nets with a relaxed notion of finiteness, namely orbit-
finiteness, where one allows for orbit-finite sets of places and transitions
instead of just finite ones; this is along the lines of [3, 2]. It is worth
recalling that similar net models have been proposed already in the early
80ies: high-level Petri nets [10] and colored Petri nets [14]. Since then,
similar formalisms seem to have been rediscovered, for instance constraint
multiset rewriting [4, 5, 6].

In plain Petri nets, bi-reachability is decidable as a consequence of
decidability of reachability [15, 16, 24]. The exact ExpSpace complexity was
established in [21]. In case of equality data, all the problems are Ackermann-
hard due to [20]. In another extension of Petri nets, namely in Petri nets
with pushdown, decidability of reachability in the reversible subclass has
been shown recently [9], while decidability status of bi-reachability is still
open.

##  2 Orbit-finite sets and vectors

In the sequel, let $\mathbb{A}$ denote a fixed countable infinite set of data
values (called also _atoms_). By $\text{Aut}(\mathbb{A})$ we denote the set of
all permutations of $\mathbb{A}$ (called also _automorphisms_). For a subset
$S\subseteq\mathbb{A}$ we define the subgroup
$\text{Aut}_{S}(\mathbb{A})=\left\\{\sigma\in\text{Aut}(\mathbb{A})\,\middle|\,\sigma(s)=s\mbox{
for all }s\in S\right\\}$. Permutations in $\text{Aut}_{S}(\mathbb{A})$ we
call _$S$ -automorphisms_.

#### Orbit-finite sets.

Consider a set $Z$ and an action of the group $\text{Aut}(\mathbb{A})$ on it:
$\iota:\text{Aut}(\mathbb{A})\times Z\to Z$. We write $\sigma(z)$ instead of
$\iota(\sigma,z)$ for $\sigma\in\text{Aut}(\mathbb{A})$ and $z\in Z$. In the
sequel we use the natural action of $\text{Aut}(\mathbb{A})$ on different sets
$Z$. Regardless of $Z$, the action renames atoms $a\in\mathbb{A}$ but leaves
other elements intact. Here are two specific examples useful later:

######  Example 2.1.

First, for finite sets $L$ and $\mathcal{R}$ of _locations_ and _register
names_ , respectively, the group $\text{Aut}(\mathbb{A})$ act naturally on
_states_ $Q=L\times\left(\mathcal{R}\to(\mathbb{A}\cup\\{\bot\\})\right)$,
namely for $\sigma\in\text{Aut}(\mathbb{A})$ and $q=(\ell,\nu)\in Q$, we
define $\sigma(q):=(\ell,\sigma(\nu))$ where $\sigma(\nu)(r)=\sigma(\nu(r))$
when $\nu(r)\in\mathbb{A}$, and $\sigma(\nu)(r)=\bot$ when $\nu(r)=\bot$.
Second, for two finite sets $H$, $P$ of plain _places_ and atom _places_ ,
respectivelty, the group $\text{Aut}(\mathbb{A})$ acts naturally on the
function space $H\cup P\times\mathbb{A}\to\mathbb{Z}$, namely given
$\sigma\in\text{Aut}(\mathbb{A})$ and $\mathbf{v}:H\cup
P\times\mathbb{A}\to\mathbb{Z}$ we define
$\sigma(\mathbf{v})(h)=\mathbf{v}(h)$ for $h\in H$ and
$\sigma(\mathbf{v})(p,\sigma(a)):=\mathbf{v}(p,a)$ for $p\in P$.
$\triangleleft$

Roughly speaking, a set is _orbit-finite_ if it has a finite number of
elements up to automorphisms of atoms. We define the  _orbit_ of an element
$z\in Z$:

$\displaystyle\text{\sc
Orbit}(z):=\left\\{\sigma(z)\,\middle|\,\sigma\in{\text{Aut}(\mathbb{A})}\right\\}.$

As different orbits are necessarily disjoint, $Z$ partitions uniquely into
orbits. A subset $X\subseteq Z$ is _orbit-finite_ if it is a finite union of
orbits. Clearly all orbits, and hence also all finite unions thereof, are
closed under the action of $\text{Aut}(\mathbb{A})$. Orbit-finite sets are
closed under finite unions and products [1, Lem. 3.24].

######  Example 2.2.

We continue Example 2.1. The whole set
$Q=L\times\left(\mathcal{R}\to(\mathbb{A}\cup\\{\bot\\})\right)$ is orbit-
finite, since the orbit of a state $q=(\ell,\nu)\in Q$ is determined by its
location $\ell$, the inverse image of $\bot$, namely
$\left\\{r\in\mathcal{R}\,\middle|\,\nu(r)=\bot\right\\}$, and the _equality
type_ of $\nu$, namely the set
$\left\\{(r,r^{\prime})\in\mathcal{R}^{2}\,\middle|\,\nu(r)=\nu(r^{\prime})\neq\bot\right\\}$.
Indeed, for every two states $q=(\ell,\nu)$ and
$q^{\prime}=(\ell^{\prime},\nu^{\prime})$ such that $\ell=\ell^{\prime}$, and
$\nu$ and $\nu^{\prime}$ have the same inverse image of $\bot$ and the same
equality type, there is an automorphism $\sigma\in\text{Aut}(\mathbb{A})$ such
that $\sigma(q)=q^{\prime}$.

On the other hand, the function space $(H\cup P\times\mathbb{A})\to\mathbb{Z}$
is orbit-infinite. $\triangleleft$

#### Vectors.

Given a set $X$, by ${X}\to_{\text{\tiny fin}}\mathbb{Z}$ we denote the
commutative group freely generated by $X$, and the group operation we denote
by $\oplus$. We write $\mathbf{v}\ominus\mathbf{w}$ instead of
$\mathbf{v}\oplus\mathbf{w}^{-1}$. Equivalently, ${X}\to_{\text{\tiny
fin}}\mathbb{Z}$ can be identified with the set of all functions
$\mathbf{v}:X\to\mathbb{Z}$ which map almost all elements of $X$ to 0, i.e.,
those functions where the set $\left\\{x\in X\,\middle|\,\mathbf{v}(x)\neq
0\right\\}$ is finite. Elements of ${X}\to_{\text{\tiny fin}}\mathbb{Z}$ we
call _$X$ -vectors_, or simply _vectors_ if the generating set $X$ is clear
from the context. The zero vector we denote by $\mathbf{0}$, irrespectively of
$X$, and a single-generator vector $x\in X$ we denote by $\mathbf{1}_{x}$.
Seen as a function $X\to\mathbb{Z}$, the vector $\mathbf{1}_{x}$ maps $x$ to 1
and all other elements of $X$ to 0. When $X$ is finite, we call $X$-vectors
finite as well. Nonnegative vectors, denoted ${X}\to_{\text{\tiny
fin}}\mathbb{N}$, are elements of the commutative monoid freely generated by
$X$, or functions $\mathbf{v}:X\to\mathbb{N}$ which map almost all elements of
$X$ to 0. We write $\oplus W$ to denote the sum of a finite set $W$ of
vectors.

In the sequel the generating set $X$ is most often of the form $H\cup
P{\times}\mathbb{A}$ for some finite sets $P$, $H$. Clearly, ${(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}$ is isomorphic to
$({H}\to_{\text{\tiny
fin}}\mathbb{Z})\times({P{\times}\mathbb{A}}\to_{\text{\tiny
fin}}\mathbb{Z})$, as every vector $\mathbf{v}:{(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}$ decomposes uniquely as
the sum $\mathbf{v}=\mathbf{u}\oplus\mathbf{w}$, where
$\mathbf{u}:{H}\to_{\text{\tiny fin}}\mathbb{Z}$,
$\mathbf{w}:{P{\times}\mathbb{A}}\to_{\text{\tiny fin}}\mathbb{Z}$. Given
$\mathbf{v}:{(H\cup P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}$, we
define its support $\text{\sc supp}(\mathbf{v})\subseteq\mathbb{A}$, as the
(necessarily finite) set of those atoms which are sent by $\mathbf{v}$ to a
nonzero value:

$\text{\sc supp}(\mathbf{v})=\left\\{a\in\mathbb{A}\,\middle|\,\exists p\in
P:\mathbf{v}(p,a)\neq 0\right\\}.$

Intuitively, $\text{\sc supp}(\mathbf{v})$ contains those atoms that ’appear’
in $\mathbf{v}$. The natural action of $\text{Aut}(\mathbb{A})$ given in
Example 2.1 restricts to the set of vectors ${(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}$, which is orbit-
infinite, and therefore we can consider orbit-finite subsets of vectors. We
also observe that $\sigma(\mathbf{v})=\mathbf{v}$ as long as $\sigma(a)=a$ for
all $a\in\text{\sc supp}(\mathbf{v})$.

######  Example 2.3.

Transitions $t_{1},t_{2}$ of Petri net in Figure 1 are semantically orbit-
finite sets of $(P{\times}\mathbb{A})$-vectors, where
$P=\left\\{p_{1},p_{2}\right\\}$ (i.e., $H=\emptyset$). Indeed, the effect of
firing $t_{1}$ amounts to adding two arbitrary but different atoms $a\neq b$
on place $p_{1}$, i.e., is described by an $X$-vector

$\mathbf{v}_{1}=(p_{1},a)\oplus(p_{1},b)\qquad\qquad(a\neq b).$

As the choice of atoms $a\neq b$ is arbitrary, all possible effects of firing
the transition span one orbit of vectors: $V_{1}=\text{\sc
Orbit}(\mathbf{v}_{1})$. The effect of firing $t_{2}$ amounts to removing some
arbitrary atom $a$ from both $p_{1}$ and $p_{2}$, and adding two further atoms
$b,c$ not equal to $a$: one of them, is added to both $p_{1}$ and $p_{2}$,
while the other one only to $p_{1}$. As it is not specified whether $b=c$ or
not, we describe $t_{2}$ by two $X$-vectors:

$\displaystyle\mathbf{v}_{2}=(p_{1},c)\oplus(p_{1},b)\oplus(p_{2},b)\ominus(p_{1},a)\ominus(p_{2},a)\qquad\qquad(a\neq
b\neq c\neq a)$ (1)
$\displaystyle\mathbf{v}^{\prime}_{2}=(p_{1},b)\oplus(p_{1},b)\oplus(p_{2},b)\ominus(p_{1},a)\ominus(p_{2},a)\qquad\qquad(a\neq
b).$ (2)

As before, the choice of atoms is arbitrary, and hence all possible effects of
firing $t_{2}$ span the union of two orbits of vectors: $V_{2}=\text{\sc
Orbit}(\mathbf{v}_{2})\cup\text{\sc Orbit}(\mathbf{v}^{\prime}_{2})$.
Intuitively, different orbits in $T_{2}$ correspond to different _equality
types_ of a tuple of atoms $(a,b,c)$: one defined by inequalities $a\neq b\neq
c\neq a$, and another defined by $a\neq b=c$. This example illustrates a
transformation of Petri nets to data vass, the model we work with in this
paper.111 As in a transformation from plain Petri nets to vass, in case of
Petri net with _tight loops_ , i.e., transitions that simultaneously input and
output the same atom from/to the same place, we would have to split every such
transition into input and output part.  $\triangleleft$

#### Multiset sum problem.

The following core decision problem will be useful later:

  * Multiset Sum

  * Input: an orbit-finite set $X$, an orbit-finite set $M$ of $X$-vectors, and an $X$-vector $\mathbf{b}$.

  * Question: is $\mathbf{b}$ equal to the sum of a finite multiset of vectors from $M$?

We assume that the orbit-finite set $A$ of vectors is represented by a finite
set of representatives, one per orbit.

######  Lemma 2.4 ([11, Thm. 17]).

Multiset Sum is decidable.

##  3 Data vector addition system with states

Classical Petri nets are equivalent, with respect to most decision problems,
to vector addition systems (vass). Likewise, we introduce here a formalism
equivalent to Petri nets with data, called data vector addition systems with
states (dvass). It is an extension of (stateless) data vector addition systems
(dvas) studied in [13].

#### Data vass.

A data vass (dvass) $\mathcal{V}=(L,\mathcal{R},H,P,T)$ consists of pairwise
disjoint finite sets of locations $L$, register names $\mathcal{R}$, plain
places $H$, atom places $P$, and an  _orbit-finite_ set

$T\subseteq Q\times\left({(H\cup P{\times}\mathbb{A})}\to_{\text{\tiny
fin}}\mathbb{Z}\right)\times Q$

of _transitions_ , where
$Q=L\times\left(\mathcal{R}\to(\mathbb{A}\cup\\{\bot\\})\right)$ is the set of
_states_. The set $T$ is thus assumed to be a finite union of orbits, under
the natural action of $\text{Aut}(\mathbb{A})$ on transitions that extends the
action on vectors and states given in Example 2.1: for
$t=(q,\mathbf{v},q^{\prime})\in T$ we put
$\sigma(t):=(\sigma(q),\sigma(\mathbf{v}),\sigma(q^{\prime}))$. In particular,
$T$ is closed under the action of $\text{Aut}(\mathbb{A})$. For a state
$(\ell,\nu)\in Q$, the function $\nu$ is called _register valuation_.
Intuitively, $\nu(r)=a$ is meaning that register $r$ contains atom $a$, while
$\nu(r)=\bot$ is meaning that $r$ is empty. The vector $\mathbf{v}$ is call
the _effect_ of transition $(s,\mathbf{v},s^{\prime})$.

The model of (plain) vass corresponds to the special case where
$\mathcal{R}=\emptyset$ and $P=\emptyset$. In this case, the set $T\subseteq
Q\times({H}\to_{\text{\tiny fin}}\mathbb{Z})\times Q$, being orbit-finite, is
necessarily finite. The model of dvas corresponds to the special case when
$Q=\left\\{*\right\\}$ is a singleton and $\mathcal{R}=\emptyset$ and
$H=\emptyset$.

A  _pseudo-configuration_ of $\mathcal{V}$ is a pair $(q,\mathbf{v})\in
Q\times({(H\cup P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z})$,
denoted also as $q(\mathbf{v})$. A  _pseudo-run_ from $q_{1}(\mathbf{v}_{0})$
to $q_{k}(\mathbf{v}_{k})$ is a sequence of pseudo-configurations
$\pi=q_{0}(\mathbf{v}_{0})\,q_{1}(\mathbf{v}_{1})\,\dots\,q_{k}(\mathbf{v}_{k})$
such that $t_{i}=(q_{i-1},\mathbf{v}_{i}-\mathbf{v}_{i-1},q_{i})\in T$ for
every $i=1,\dots,k$. We say that the pseudo-run $\pi$ _uses_ the transitions
$t_{1},\ldots,t_{k}\in T$. The support of a state $q=(\ell,\nu)$ is the set of
all atoms used in registers, i.e. $\text{\sc
supp}(q)=\nu(\mathcal{R})\cap\mathbb{A}.$ The support of a transition
$t=(q,\mathbf{v},q^{\prime})$ is $\text{\sc supp}(t)=\text{\sc
supp}(q)\cup\text{\sc supp}(\mathbf{v})\cup\text{\sc supp}(q^{\prime})$. We
also define the support of a pseudo-run as the union of supports of all its
pseudo-configurations: $\text{\sc supp}(\pi)=\text{\sc
supp}(q_{0})\cup\text{\sc supp}(\mathbf{v}_{0})\cup\text{\sc
supp}(q_{1})\cup\ldots\cup\text{\sc supp}(q_{k})\cup\text{\sc
supp}(\mathbf{v}_{k})$. We again extend the action of
$\text{Aut}(\mathbb{A})$, this time to pseudo-runs, in an expected way:

$\sigma\big{(}q_{0}(\mathbf{v}_{0})\,q_{1}(\mathbf{v}_{1})\,\dots\,q_{k}(\mathbf{v}_{k})\big{)}\
:=\ \sigma(q_{0})(\sigma(\mathbf{v}_{0}))\
\sigma(q_{1})(\sigma(\mathbf{v}_{1}))\ \dots\
\sigma(q_{k})(\sigma(\mathbf{v}_{k})).$

The set of pseudo-runs is closed under the action.

_Configurations_ are those pseudo-configurations $q(\mathbf{v})$ where
$\mathbf{v}$ is nonnegative, i.e., $\mathbf{v}:{(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{N}$. Let $\text{\sc
Conf}=Q\times\big{(}{(H\cup P{\times}\mathbb{A})}\to_{\text{\tiny
fin}}\mathbb{N}\big{)}$ denote the set of all configurations. A  _run_ is a
pseudo-run where every pseudo-configuration $q_{i}(\mathbf{v}_{i})$ is
actually a configuration. We write $q(\mathbf{v})\dashrightarrow
q^{\prime}(\mathbf{v}^{\prime})$ (resp. $q(\mathbf{v})\longrightarrow
q^{\prime}(\mathbf{v}^{\prime}))$ if there is a pseudo-run (resp. a run) from
$q(\mathbf{v})$ to $q^{\prime}(\mathbf{v}^{\prime})$.

######  Example 3.1.

Continuing Example 2.3, Petri net in Figure 1 is equivalent to dvas
$\mathcal{V}=(\left\\{*\right\\},\emptyset,\emptyset,\left\\{p_{1},p_{2}\right\\},T)$,
whose transitions are (as $\mathcal{R}=\emptyset$, we omit register
valuations)

$T=\left\\{*\right\\}\times(V_{1}\cup V_{2})\times\left\\{*\right\\}.$

The initial configuration shown in Figure 1 is $*(\mathbf{v})$ (we omit
register valuation as there are no registers), where
$\mathbf{v}=(p_{1},a)\oplus(p_{1},c)\oplus(p_{1},c)\oplus(p_{2},a)\oplus(p_{2},b)$
for some distinct atoms $a,b,c\in\mathbb{A}$. In order to illustrate dvass,
let’s drop the first inequality in the constraint on $t_{2}$, i.e., let’s
consider the relaxed constraint $z_{1}=z_{2}\land y_{1}=y_{2}\neq z_{3}$
instead. This adds a third orbit of possible effects of firing $t_{2}$, when
the atom $b$ added to places $p_{1}$ and $p_{2}$ is the same as the atom $a$
removed (c.f. (1) in Example 2.3):

$\displaystyle\mathbf{v}^{\prime\prime}_{2}=(p_{1},c)\oplus(p_{1},a)\oplus(p_{2},a)\ominus(p_{1},a)\ominus(p_{2},a)\qquad\qquad(a\neq
c).$

The so modified Petri net is equivalent to dvass
$\mathcal{V}^{\prime}=(L,\emptyset,\emptyset,P,T^{\prime})$ with two locations
$L=\left\\{\ell,\ell^{\prime}\right\\}$, still no registers, a larger set of
atom places $P=\left\\{p_{1},p_{2},\overline{p}\right\\}$, and transitions:

$T^{\prime}\ =\ \left\\{\ell\right\\}\times(V_{1}\cup
V_{2})\times\left\\{\ell\right\\}\ \ \cup\ \
\left\\{\ell\right\\}\times\text{\sc
Orbit}(\mathbf{w})\times\left\\{\ell^{\prime}\right\\}\ \ \cup\ \
\left\\{\ell^{\prime}\right\\}\times\text{\sc
Orbit}(\mathbf{w}^{\prime})\times\left\\{\ell\right\\},$

where vectors $\mathbf{w}$, $\mathbf{w}^{\prime}$ are splitting
$\mathbf{v}^{\prime\prime}_{2}$ into input and output part, using an auxiliary
place $\overline{p}$ to temporarily store atom $a$:

$\displaystyle\mathbf{w}=(\overline{p},a)\ominus(p_{1},a)\ominus(p_{2},a)\qquad\mathbf{w}^{\prime}=(p_{1},c)\oplus(p_{1},a)\oplus(p_{2},a)\ominus(\overline{p},a)\qquad(a\neq
c).$ (3)

Transitions in $T^{\prime}$ corresponding to $V_{1}\cup V_{2}$ go from $\ell$
to $\ell$, while the other transitions go from $\ell$ to $\ell^{\prime}$, or
from $\ell^{\prime}$ to $\ell$. The initial configuration of
$\mathcal{V}^{\prime}$ is $\ell(\mathbf{v})$. Instead of place $\overline{p}$
one could also use a single register $\mathcal{R}=\left\\{r\right\\}$, and
transitions of the form

$((\ell,\bot),\ \ominus(p_{1},a)\ominus(p_{2},a),\
(\ell^{\prime},a))\qquad((\ell^{\prime},a),\
(p_{1},c)\oplus(p_{1},a)\oplus(p_{2},a),\ (\ell,\bot))\qquad(a\neq c),$

to the same effect as in (3). The initial configuration would be then
$q(\mathbf{v})$, where $q=(\ell,\bot)$. $\triangleleft$

We define the _state graph_ $(Q,E)$ of a dvass $\mathcal{V}$, denoted
$\text{\sc Graph}(T)$. Its nodes are states $Q$, and its edges $E\subseteq
Q\times Q$ are pairs of states related by some transition of $\mathcal{V}$:

$E\ =\ \left\\{(q,q^{\prime})\in Q^{2}\,\middle|\,(q,\mathbf{v},q^{\prime})\in
T\text{ for some vector }\mathbf{v}:{(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}\right\\}.$

When $\mathcal{R}$ is non-empty, the sets of nodes and edges are infinite but
orbit-finite.

#### Bi-reachability problem.

We say that a configuration $q^{\prime}(\mathbf{v}^{\prime})$ is _reachable_
from $q(\mathbf{v})$ if there is a run $q(\mathbf{v})\longrightarrow
q^{\prime}(\mathbf{v}^{\prime})$. Two configurations $q(\mathbf{v})$,
$q^{\prime}(\mathbf{v}^{\prime})$ are _bi-reachable_ if each of them is
reachable from the other: $q(\mathbf{v})\longrightarrow
q^{\prime}(\mathbf{v}^{\prime})$ and $q(\mathbf{v})\longleftarrow
q^{\prime}(\mathbf{v}^{\prime})$.

  * dvass bi-reachability

  * Input: a dvass $(L,\mathcal{R},H,P,T)$ and two configurations, $q(\mathbf{v})$ and $q^{\prime}(\mathbf{v}^{\prime})$ .

  * Question: are $q(\mathbf{v})$, $q^{\prime}(\mathbf{v}^{\prime})$ bi-reachable?

As before, we assume that the orbit-finite set $T$ of transitions is
represented by a finite set of representatives, one per orbit. As our main
result we prove:

######  Theorem 3.2.

dvass bi-reachability problem is decidable.

As our model of dvass includes plain places, we can assume w.l.o.g. a
convenient form of source and target configuration that consists, essentially,
of just a location. Let $\bot\\!\\!\\!\\!\bot$ denote the empty register
valuation: $\bot\\!\\!\\!\\!\bot(r)=\bot$ for every $r\in\mathcal{R}$.

######  Lemma 3.3.

lem:wlog In dvass bi-reachability we may assume, w.l.o.g., that
$q=(\ell,\bot\\!\\!\\!\\!\bot)$,
$q^{\prime}=(\ell^{\prime},\bot\\!\\!\\!\\!\bot)$, and
$\mathbf{v}=\mathbf{v}^{\prime}=\mathbf{0}$.

######  Proof 3.4.

Consider a dvass $\mathcal{V}=(L,\mathcal{R},P,H,T)$ and two configurations
$q(\mathbf{v}),q^{\prime}(\mathbf{v}^{\prime})$.

We proceed in three steps. First, we argue that w.l.o.g. we can assume that
there are no registers, $\mathcal{R}=\emptyset$ (which implies
$q=(\ell,\bot\\!\\!\\!\\!\bot)$ and
$q^{\prime}=(\ell^{\prime},\bot\\!\\!\\!\\!\bot)$). Let $S=\text{\sc
supp}(\nu)\cup\text{\sc supp}(\nu^{\prime})$ be the set of those atoms which
appear in $\nu$ or $\nu^{\prime}$. Intuitively, we move the set $\mathcal{R}$
to atom places $P$. We take $P_{1}:=P\cup\mathcal{R}$ as atom places, and
locations $L_{1}:=L\times\mathcal{P}(\mathcal{R})$ to keep track of the subset
of currently empty registers. The new transitions $T_{1}$ treat registers as
atom places that store at most one token. For the formal definition of
$T_{1}$, we define a vector $\widehat{\mu}$ induced by a register valuation
$\mu$ as $\widehat{\mu}=\oplus\left\\{(r,a)\,\middle|\,\mu(r)=a\right\\}$.
Then every transition $((k,\mu),\mathbf{v},(k^{\prime},\mu^{\prime}))\in T$ of
$\mathcal{V}$ induces a transition

$\big{(}(k,\mu^{-1}(\bot)),\
\mathbf{v}\ominus\widehat{\mu}\oplus\widehat{\mu}^{\prime},\
(k^{\prime},(\mu^{\prime})^{-1}(\bot))\big{)}\in T_{1}.$

This yields a dvass $\mathcal{V}_{1}=(L_{1},\emptyset,H,P_{1},T_{1})$. Let
$\overline{\ell}=(\ell,\nu^{-1}(\bot))$,
$\overline{\ell}^{\prime}=(\ell^{\prime},(\nu^{\prime})^{-1}(\bot))\in L_{1}$,
and $\overline{\mathbf{v}}=\mathbf{v}\oplus\widehat{\nu}$,
$\overline{\mathbf{v}}^{\prime}=\mathbf{v}^{\prime}\oplus\widehat{\nu}^{\prime}:{H\cup
P_{1}{\times}\mathbb{A}}\to_{\text{\tiny fin}}\mathbb{N}$. In the sequel, when
writing configuration of register-less dvass we omit registers, e.g.,
$\overline{\ell}(\overline{\mathbf{v}})$.

######  Claim 1.

The configurations $q(\mathbf{v})$, $q^{\prime}(\mathbf{v}^{\prime})$ are bi-
reachable in $\mathcal{V}$ if and only if
$\overline{\ell}(\overline{\mathbf{v}})$,
$\overline{\ell}^{\prime}(\overline{\mathbf{v}}^{\prime})$ are bi-reachable in
$\mathcal{V}_{1}$.

Second, consider a register-less dvass $\mathcal{V}=(L,\emptyset,P,H,T)$ and
two configurations $\ell(\mathbf{v})=q(\mathbf{u}\oplus\mathbf{w})$ and
$\ell^{\prime}(\mathbf{v}^{\prime})=q^{\prime}(\mathbf{u}^{\prime}\oplus\mathbf{w}^{\prime})$,
where $\mathbf{u},\mathbf{u}^{\prime}:{H}\to_{\text{\tiny fin}}\mathbb{N}$ and
$\mathbf{w},\mathbf{w}^{\prime}:{P{\times}\mathbb{A}}\to_{\text{\tiny
fin}}\mathbb{N}$. We argue that w.l.o.g. we can assume
$\mathbf{w}=\mathbf{w}^{\prime}=\mathbf{0}$. Let $S=\text{\sc
supp}(\mathbf{v})\cup\text{\sc supp}(\mathbf{v}^{\prime})$ be the set of those
atoms which appear in $\mathbf{w}$ or $\mathbf{w}^{\prime}$. Intuitively, we
move the set $P\times S$ to plain places $H$. We take $H^{\prime}=H\cup
P{\times}S$ as plain places, and consider atoms
$\mathbb{A}^{\prime}=\mathbb{A}\setminus S$ instead of $\mathbb{A}$. Clearly,

$H\cup(P{\times}\mathbb{A})\ =\ H^{\prime}\cup(P{\times\mathbb{A}^{\prime}})$

and therefore we may take the same transitions $T$ as transitions of the new
dvass $\mathcal{V}_{2}=(L,\emptyset,H^{\prime},P,T^{\prime})$. As $S$ is
finite, the set $T^{\prime}$ is still orbit-finite with respect to
$\text{Aut}(\mathbb{A}^{\prime})$.

######  Claim 2.

The configurations $\ell({\mathbf{v}})$,
$\ell^{\prime}({\mathbf{v}}^{\prime})$ are bi-reachable in $\mathcal{V}$ if
and only if $\ell({\mathbf{u}})$, $\ell^{\prime}({\mathbf{u}}^{\prime})$ are
bi-reachable in $\mathcal{V}_{2}$.

In the last third step, consider a dvass $\mathcal{V}=(L,\emptyset,P,H,T)$
without registers and two configurations $\ell(\mathbf{u})$ and
$\ell^{\prime}(\mathbf{u}^{\prime})$, where
$\mathbf{u},\mathbf{u}^{\prime}:{H^{\prime}}\to_{\text{\tiny fin}}\mathbb{N}$.
We eliminate the initial and final values $\mathbf{u}$, $\mathbf{u}^{\prime}$
on plain places in a classical way, by introducing new initial and final
locations $\overline{\ell}$, $\overline{\ell}^{\prime}$ and adding to $T$ the
following four transitions, and thus defining
$\mathcal{V}_{3}=(L\cup\left\\{\overline{\ell},\overline{\ell}^{\prime}\right\\},\emptyset,H,P,T^{\prime})$:

$\displaystyle(\overline{\ell},\mathbf{u},\ell)\qquad(\ell^{\prime},-\mathbf{u}^{\prime},\
\overline{\ell}^{\prime})\qquad(\ell,-\mathbf{u},\
\overline{\ell})\qquad(\overline{\ell}^{\prime},\mathbf{u}^{\prime},\ell^{\prime}).$
(4)

######  Claim 3.

The configurations $\ell(\mathbf{u})$, $\ell^{\prime}(\mathbf{u}^{\prime})$
are bi-reachable in $\mathcal{V}$ if and only if
$\overline{\ell}(\mathbf{0})$, $\overline{\ell}^{\prime}(\mathbf{0})$ are bi-
reachable in $\mathcal{V}_{3}$.

Indeed, a run
$\ell(\mathbf{u})\longrightarrow\ell^{\prime}(\mathbf{u}^{\prime})$ in
$\mathcal{V}$ extended with the first two transitions in (4) yields a run
$\overline{\ell}(\mathbf{0})\longrightarrow\overline{\ell}^{\prime}(\mathbf{0})$
in $\mathcal{V}_{3}$, and likewise a run
$\ell^{\prime}(\mathbf{u}^{\prime})\longrightarrow\ell(\mathbf{u})$ in
$\mathcal{V}$ extended with the last two transitions in (4) yields a run
$\overline{\ell}^{\prime}(\mathbf{0})\longrightarrow\overline{\ell}(\mathbf{0})$
in $\mathcal{V}_{3}$. Conversely, consider a run
$\pi:\overline{\ell}(\mathbf{0})\longrightarrow\overline{\ell}^{\prime}(\mathbf{0})$
in $\mathcal{V}_{3}$. It necessarily starts with the first transition in (4),
and ends with the second one. If transitions (4) are used elsewhere in $\pi$,
they are necessarily used in pairs, namely the second one followed immediately
by the fourth one, or the third one is followed immediately by the first one.
Effects of each such pair cancel out, and thus each pair can be safely removed
from $\pi$. Finally, removing the first and the last transition makes $\pi$
into a run $\ell(\mathbf{u})\longrightarrow\ell^{\prime}(\mathbf{u}^{\prime})$
in $\mathcal{V}$, as required. Likewise we transform a run
$\overline{\ell}^{\prime}(\mathbf{0})\longrightarrow\overline{\ell}(\mathbf{0})$
in $\mathcal{V}_{3}$.

##  4 Toolset

Our decision procedure relies a number of existing tools. One of them is
solvability of Multiset sum (Lemma 2.4). Here we present two further tools: a
sufficient condition for vass reachability, and computability of coverability
sets in dvas.

#### Sufficient condition for vass reachability.

We recall a condition that guarantees existence of a run in a vass. It is a
simplification of the classical condition of [15, 16, 24] which guarantees
existence of a run in a _generalised_ vass. Consider a vass $\mathcal{V}$ with
plain places $H$. For $\mathbf{v}:{H}\to_{\text{\tiny fin}}\mathbb{N}$ we
write $\mathbf{v}\gg\mathbf{0}$ to mean that for every $h\in H$ we have
$\mathbf{v}(h)>0$.

  * •

$\Theta_{1}$: For every $m\in\mathbb{N}$, there is a pseudo-run
$q(\mathbf{0})\dashrightarrow q^{\prime}(\mathbf{0})$ using every transition
at least $m$ times.

  * •

$\Theta_{2}$: For some vectors
$\mathbf{\Delta},\mathbf{\Delta}^{\prime}\gg\mathbf{0}$, there are runs:
$q(\mathbf{0})\longrightarrow q(\mathbf{\Delta})$ and
$q^{\prime}(\mathbf{\Delta}^{\prime})\longrightarrow q^{\prime}(\mathbf{0})$.

######  Lemma 4.1 (Prop. 1 in [18]).

For every vass, $\Theta_{1}\land\Theta_{2}$ implies
$q(\mathbf{0})\longrightarrow q^{\prime}(\mathbf{0})$.

#### Coverability sets in dvass.

Let $\mathcal{V}=(L,\mathcal{R},H,P,T)$ be a dvass, and let
$X=H\cup(P{\times}\mathbb{A})$. We define the pointwise order on nonnegative
vectors ${X}\to_{\text{\tiny fin}}\mathbb{N}$:
$\mathbf{v}\leq\mathbf{v}^{\prime}$ if and only if for every $x\in X$ we have
$\mathbf{v}(x)\leq\mathbf{v}^{\prime}(x)$. We define a quasi-order by
relaxation of $\leq$, up to automorphisms:
$\mathbf{v}\sqsubseteq\mathbf{v}^{\prime}$ if
$\sigma(\mathbf{v})\leq\mathbf{v}^{\prime}$ for some
$\sigma\in\text{Aut}(\mathbb{A})$. We extend the relation $\sqsubseteq$ to
configurations in the expectable way: for states $q,q^{\prime}$ and vectors
$\mathbf{v},\mathbf{v}^{\prime}\in{X}\to_{\text{\tiny fin}}\mathbb{N}$ we
stipulate $q(\mathbf{v})\sqsubseteq q^{\prime}(\mathbf{v})$ if
$\sigma(q)=q^{\prime}$ and $\sigma(\mathbf{v})\leq\mathbf{v}^{\prime}$ for
some $\sigma\in\text{Aut}(\mathbb{A})$.

######  Lemma 4.2.

lem:wqo $\sqsubseteq$ is a wqo on configurations.

######  Proof 4.3.

Recall the sets of states
$Q=L\times(\mathcal{R}\to(\mathbb{A}\cup\left\\{\bot\right\\}))$ and
configurations $\text{\sc Conf}=Q\times\big{(}{(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{N}\big{)}$. The quasi-order
$\sqsubseteq$ is a wqo on the set of nonnegative vectors
${P{\times}\mathbb{A}}\to_{\text{\tiny fin}}\mathbb{N}$, as it is quasi-order-
isomorphic to multiset inclusion in $M({P}\to_{\text{\tiny fin}}\mathbb{Z})$,
the set of finite multisets of finite vectors from ${P}\to_{\text{\tiny
fin}}\mathbb{Z}$. Furthermore, $\sqsubseteq$ is a wqo on ${(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{N}$, as it is quasi-order-
isomorphic to the Cartesian product $({H}\to_{\text{\tiny
fin}}\mathbb{N})\times({P{\times}\mathbb{A}}\to_{\text{\tiny fin}}\mathbb{N})$
of two wqo’s, and Cartesian product preserves wqo.

Every register valuation $\nu:\mathcal{R}\to(\mathbb{A}\cup\\{\bot\\})$ may be
seen as an $\mathcal{R}^{\prime}$-vector, where
$\mathcal{R}^{\prime}=\nu^{-1}(\mathbb{A})$ is the set of non-empty registers,
namely
$\widehat{\nu}=\oplus\left\\{(r,a)\,\middle|\,\nu(r)=a\right\\}:{\mathcal{R}^{\prime}}\to_{\text{\tiny
fin}}\mathbb{N}$. We use this fact to argue that $\sqsubseteq$ is a wqo on
$Y=(\mathcal{R}\to(\mathbb{A}\cup\\{\bot\\}))\times({(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{N})$. Indeed, we split this
set into $2^{|\mathcal{R}|}$ subsets, determined by non-empty registers, i.e.,
for every subset $\mathcal{R}^{\prime}\subseteq\mathcal{R}$ we consider a
subset

$C_{\mathcal{R}^{\prime}}\ :=\
\left\\{(\nu,\mathbf{v})\,\middle|\,\nu^{-1}(\mathbb{A})=\mathcal{R}^{\prime}\right\\}\
\subseteq\ Y.$

For every fixed $\mathcal{R}^{\prime}$, the set $C_{\mathcal{R}^{\prime}}$ is
essentially a subset of
${(P\cup\mathcal{R}^{\prime})\times\mathbb{A}}\to_{\text{\tiny
fin}}\mathbb{N}$, due to the bijection
$(\nu,\mathbf{v})\mapsto\widehat{\nu}\oplus\mathbf{v}$, containing those
vectors which use exactly one generator from
$\mathcal{R}^{\prime}\times\mathbb{A}$. Therefore $C_{\mathcal{R}^{\prime}}$
is a wqo. In consequence, $Y$ is a wqo too, as finite sums preserve wqo.

Finally, the set $\text{\sc Conf}=Q\times Y$ is a wqo, as Cartesian product of
the finite discrete quasi-order $Q$ and a wqo.

The _coverability set_ of a configuration $q(\mathbf{v})$ is defined as the
downward closure, with respect to $\sqsubseteq$, of the reachability set:

$\text{\sc Cover}(q(\mathbf{v}),q^{\prime})\ =\
\left\\{\mathbf{v}^{\prime}\,\middle|\,\exists\mathbf{w}:\mathbf{v}^{\prime}\sqsubseteq\mathbf{w}\
\wedge\ q(\mathbf{v})\longrightarrow q^{\prime}(\mathbf{w})\right\\}.$

Is is known that the coverability set is representable by a finite union of
_ideals_ (downward closed directed sets) [7, 8]. Let’s complete $\mathbb{N}$
with a top element, $\mathbb{N}_{\omega}\stackrel{{\scriptstyle\text{\tiny
def}}}{{=}}\mathbb{N}\uplus\left\\{\omega\right\\}$, which is larger than all
numbers: $n<\omega$ for all $n\in\mathbb{N}$. Every function
$f:X\to\mathbb{N}_{\omega}$ with finite range determines a non-empty set of
nonnegative vectors (we extend $\sqsubseteq$ to all functions
$X\to\mathbb{N}_{\omega}$),

$f\\!\downarrow\ \ :=\ \left\\{\mathbf{v}:{X}\to_{\text{\tiny
fin}}\mathbb{N}\,\middle|\,\mathbf{v}\sqsubseteq f\right\\},$

which is downward closed (whenever $\mathbf{v}\in f\\!\downarrow\ $ and
$\mathbf{v}^{\prime}\sqsubseteq\mathbf{v}$ then $\mathbf{v}^{\prime}\in
f\\!\downarrow\ $ as well) and directed (for every two
$\mathbf{v},\mathbf{v}^{\prime}\in f\\!\downarrow\ $ there is $\mathbf{w}\in
f\\!\downarrow\ $ such that $\mathbf{v}\sqsubseteq\mathbf{w}$ and
$\mathbf{v}^{\prime}\sqsubseteq\mathbf{w}$). The set $f\\!\downarrow\ $ is
thus an _ideal_. We call the function _simple_ if for every $p\in P$, either
$f(p,a)=0$ for almost all $a\in\mathbb{A}$, or $f(a,p)=\omega$ for almost all
$a\in\mathbb{A}$. Ideals determined by simple functions we call simple too.

######  Example 4.4.

Consider again Petri net from Figure 1, its modification in Example 3.1 and
the equivalent dvass $\mathcal{V}^{\prime}$ defined therein. Due to transition
$t_{1}$, place $p_{1}$ can be filled up with arbitrary many tokens with any
atoms. On the other hand place $p_{2}$ has two tokens in the initial
configuration $\ell(\mathbf{v})$, and hence will invariantly have, in location
$\ell$, two tokens whose atoms may be equal or not. Therefore $\text{\sc
Cover}(\ell(\mathbf{v}),\ell)=f_{1}\\!\downarrow\ \cup\ f_{2}\\!\downarrow\ $,
where

$\displaystyle f_{1}(p_{1},c)=\omega$ $\displaystyle f_{2}(p_{1},c)=\omega$
$\displaystyle\text{ for every }c\in\mathbb{A},$ $\displaystyle
f_{1}(p_{2},a)=f_{1}(p_{2},b)=1$ $\displaystyle f_{2}(p_{2},a)=2$
$\displaystyle\text{ for some }a\neq b\in\mathbb{A},$

and all other arguments are mapped by $f_{1}$ and $f_{2}$ to 0. In location
$\ell^{\prime}$, places $p_{2}$ and $\overline{p}$ have always one token each,
with atoms equal or not. $\triangleleft$

Simple functions provide finite representations of simple ideals. Relying on
the result of [13], the coverability set in a dvas is a union of a finite set
of simple ideals, which is computable. We lift this result to the model of
dvass:

######  Lemma 4.5.

lem:cover Given a dvass, its configuration $q(\mathbf{v})$ and state
$q^{\prime}$, one can compute a finite set of simple functions
$\left\\{f_{1},\ldots,f_{n}\right\\}$ such that $\text{\sc
Cover}(q(\mathbf{v}),q^{\prime})=f_{1}\\!\downarrow\ \cup\ldots\cup
f_{n}\\!\downarrow\ $.

######  Proof 4.6.

Let $\mathcal{V}=(L,\mathcal{R},H,P,T)$ be a dvass, let $q(\mathbf{v})$ be its
configuration, where $q=(\ell,\nu)$, and let $q^{\prime}=(\ell,\nu^{\prime})$.
Theorem 3.5 in [13] proves the claim in the special case of dvas. We reduce
dvass to dvas in three steps. First, we get rid of registers, similarly to the
proof of Lemma LABEL:lem:wlog, by considering them as additional atom places,
and keeping track in location which registers are empty. We set
$P^{\prime}:=P\cup\mathcal{R}$ and
$L^{\prime}=L\times\mathcal{P}(\mathcal{R})$. We define the new set of
transitions as follows: any transition
$((\ell,\mu),\mathbf{v},(\ell^{\prime},\mu^{\prime}))\in T$ changes into
$((\ell,\mu^{-1}(\bot)),\mathbf{v}\ominus\widehat{\mu}\oplus\widehat{\mu}^{\prime},(\ell^{\prime},(\mu^{\prime})^{-1}(\bot)))\in
T^{\prime}$, where
$\widehat{\mu}=\oplus\left\\{(r,a)\,\middle|\,\mu(r)=a\right\\}$. This yields
a dvass $\mathcal{V}^{\prime}=(L^{\prime},\emptyset,H,P^{\prime},T^{\prime})$,
and the corresponding configuration $\ell(\mathbf{v}\oplus\widehat{\nu})$ such
that the coverability sets in $\mathcal{V}$ (on the left) and
$\mathcal{V}^{\prime}$ (on the right) essentially coincide:

$\text{\sc Cover}(q(\mathbf{v}),q^{\prime})\ =\
\left\\{\mathbf{v}^{\prime}\,\middle|\,\mathbf{v}^{\prime}\oplus\widehat{\nu}^{\prime}\in\text{\sc
Cover}((\ell,\nu^{-1}(\bot))(\mathbf{v}\oplus\widehat{\nu}),(\ell^{\prime},(\nu^{\prime})^{-1}(\bot)))\right\\}.$

As the second step, we dispose of locations $L^{\prime}$ by moving them to
plain places. We set $H^{\prime\prime}:=H\cup L^{\prime}$ and adapt
transitions accordingly:

$t=(\ell,\mathbf{v},\ell^{\prime})\quad\mapsto\quad(*,\mathbf{v}\ominus\ell\oplus\ell^{\prime},*).$

This yields a dvass
$\mathcal{V}^{\prime\prime}=(\left\\{*\right\\},\emptyset,H^{\prime\prime},P^{\prime},T^{\prime\prime})$,
and the corresponding configuration $*(\mathbf{v}\oplus\ell)$ such that the
coverability sets in $\mathcal{V}^{\prime}$ (on the left) and
$\mathcal{V}^{\prime\prime}$ (on the right) essentially coincide:

$\text{\sc Cover}(\ell(\mathbf{v}),\ell^{\prime})\ =\
\left\\{\mathbf{v}^{\prime}\,\middle|\,\mathbf{v}^{\prime}\oplus\ell^{\prime}\in\text{\sc
Cover}(*(\mathbf{v}\oplus\ell),*)\right\\}.$

Eventually, as the last step we get rid of plain places $H^{\prime\prime}$ by
moving them to atom ones, and considering atoms residing on these atom places
irrelevant. Let $P^{\prime\prime\prime}:=H^{\prime\prime}\cup P^{\prime}$. In
order to transfer transitions $T^{\prime\prime}$ from plain places to the new
atom places, we introduce the projection mapping $\pi:(H^{\prime\prime}\cup
P^{\prime}){\times}\mathbb{A}\to
H^{\prime\prime}\cup(P^{\prime}{\times}\mathbb{A})$ defined by

$(h,a)\mapsto h\qquad(p,a)\mapsto(p,a)\qquad\qquad(h\in H^{\prime\prime},p\in
P^{\prime},a\in\mathbb{A}).$

The projection forgets, intuitively speaking, about atoms on the new atom
places. It extends uniquely to a commutative group homomorphism $\pi$ from
${(H^{\prime\prime}\cup P^{\prime}){\times}\mathbb{A}}\to_{\text{\tiny
fin}}\mathbb{Z}$ to
${H^{\prime\prime}\cup(P^{\prime}{\times}\mathbb{A})}\to_{\text{\tiny
fin}}\mathbb{Z}$. We define transitions

$T^{\prime\prime\prime}:=\pi^{-1}(T^{\prime\prime})$

are the inverse image of $T^{\prime\prime}$ along $\pi$. This yields a dvas
$\mathcal{V}^{\prime\prime\prime}=(\left\\{*\right\\},\emptyset,\emptyset,P^{\prime\prime\prime},T^{\prime\prime\prime})$.
We observe that $\pi^{-1}(\mathbf{v})$ is orbit-finite for every vector
$\mathbf{v}$, and therefore $\pi^{-1}(T^{\prime\prime})$, being orbit-finite
union of orbit-finite sets, is itself orbit-finite [1, Ex. 62]. The
coverability set in $\mathcal{V}^{\prime\prime}$ (on the left) is easily
computed from the coverability set in $\mathcal{V}^{\prime\prime\prime}$ (on
the right), since coverability sets commute the the projection:

$\text{\sc Cover}(*(\pi(\mathbf{w})),*)\ =\ \pi(\text{\sc
Cover}(*(\mathbf{w}),*)).$

Therefore, in order to compute a representation $\text{\sc
Cover}(*(\pi(\mathbf{v})),*)\ =\ g_{1}\\!\downarrow\ \cup\ldots\cup
g_{n}\\!\downarrow\ $ in $\mathcal{V}^{\prime\prime}$, we take any
$\mathbf{w}$ with $\pi(\mathbf{w})=\mathbf{v}$, compute a representation
$\text{\sc Cover}(*(\mathbf{w}),*)\ =\ f_{1}\\!\downarrow\ \cup\ldots\cup
f_{n}\\!\downarrow\ $ in $\mathcal{V}^{\prime\prime\prime}$ using in [13, Thm.
3.5], and modify the functions $f_{i}$ by summing up, for every $h\in
H^{\prime\prime}$, namely (under the proviso that
$\omega+n=\omega+\omega=\omega$):

$g_{i}(h)\ :=\ \sum_{a\in\mathbb{A}}f_{i}(h,a)\qquad g_{i}(p,a)\ :=\
f_{i}(p,a)\qquad\qquad(h\in H^{\prime\prime},p\in P^{\prime},a\in\mathbb{A}).$

This completes the reduction.

##  5 Decidability

We are now proving Theorem 3.2. Throughout this section let
$\mathcal{V}=(L,\mathcal{R},H,P,T)$ be an input dvass. Relying on Lemma
LABEL:lem:wlog we investigate bi-reachability of $q(\mathbf{0})$ and
$q^{\prime}(\mathbf{0})$, for states $q=(\ell,\bot\\!\\!\\!\\!\bot)\in Q$ and
$q^{\prime}=(\ell^{\prime},\bot\\!\\!\\!\\!\bot^{\prime})\in Q$ with empty
register valuations.

The states $q,q^{\prime}$ are invariant under the action of
$\text{Aut}(\mathbb{A})$, which is crucial in the sequel:

######  Claim 4.

For every $\sigma\in\text{Aut}(\mathbb{A})$, we have $\sigma(q)=q$ and
$\sigma(q^{\prime})=q^{\prime}$.

#### Sufficient condition for dvass bi-reachability.

We start by formulating a sufficient condition for bi-reachability of
$q(\mathbf{0})$ and $q^{\prime}(\mathbf{0})$, by a natural generalisation of
the classical $\Theta_{1}$ and $\Theta_{2}$ conditions. In the context of bi-
reachability, it is enough to rely on a simplified version of these conditions
given by Lemma 4.1, see e.g. [18, Prop. 1]. We write below
$\mathbf{v}\gg\mathbf{0}$ to mean that $\mathbf{v}(h)>0$ for every $h\in H$,
and for every $p\in P$ there is some $a\in\mathbb{A}$ such that
$\mathbf{v}(p,a)>0$.

  * •

$\mathbf{\Phi}_{1}$: There are pseudo-runs, each of them using some transition
from every orbit in $T$:

$\displaystyle\begin{aligned} &q(\mathbf{0})\dashrightarrow
q^{\prime}(\mathbf{0})\qquad\qquad q(\mathbf{0})\dashleftarrow
q^{\prime}(\mathbf{0}).\end{aligned}$ (5)

  * •

$\mathbf{\Phi}_{2}$: For some vectors
$\mathbf{\Delta},\mathbf{\Delta}^{\prime},\mathbf{\Gamma},\mathbf{\Gamma}^{\prime}\gg\mathbf{0}$,
there are runs:

$\displaystyle\begin{aligned} &q(\mathbf{0})\longrightarrow
q(\mathbf{\Delta})\qquad\quad&&q^{\prime}(\mathbf{\Delta}^{\prime})\longrightarrow
q^{\prime}(\mathbf{0})\\\ &q(\mathbf{0})\longleftarrow
q(\mathbf{\Gamma})&&q^{\prime}(\mathbf{\Gamma}^{\prime})\longleftarrow
q^{\prime}(\mathbf{0}).\end{aligned}$ (6)

######  Lemma 5.1.

$\mathbf{\Phi}_{1}\land\mathbf{\Phi}_{2}$ implies
$q(\mathbf{0})\longrightarrow q^{\prime}(\mathbf{0})$ and
$q(\mathbf{0})\longleftarrow q^{\prime}(\mathbf{0})$.

######  Proof 5.2.

Assume $\mathcal{V}$ satisfies $\mathbf{\Phi}_{1}\land\mathbf{\Phi}_{2}$. Let
$S$ be the union of supports of the two pseudo-runs (LABEL:eq:psruns) and the
four runs (LABEL:eq:runs). Recall that $\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})\subseteq\text{Aut}(\mathbb{A})$ denotes the subset of those
automorphisms $\sigma$ that are identity outside of $S$: $\sigma(a)=a$ for
every $a\notin S$. When restricted to $S$, each such automorphism is a
permutation, i.e., $\sigma(S)=S$. In the sequel we will apply permutations
$\sigma\in\text{Aut}_{\mathbb{A}\setminus S}(\mathbb{A})$ to atoms from $S$
only, and therefore the value $\sigma(a)=a$, for $a\notin S$, will be
irrelevant. The set $\text{Aut}_{\mathbb{A}\setminus S}(\mathbb{A})$ is
finite, $|\text{Aut}_{\mathbb{A}\setminus S}(\mathbb{A})|=|S|!$

We define a (plain) vass $\mathcal{V}_{S}$ by, intuitively speaking,
restricting the set of atoms to the finite set $S$. The set of locations of
$\mathcal{V}_{S}$ is $L_{S}:=L\times(\mathcal{R}\to S\cup\\{\bot\\})$, its
places are $H_{S}:=H\cup P{\times}S$, and its transitions $T_{S}\subseteq T$
are all transitions of $\mathcal{V}$ that use only atoms from $S$. Formally,
$\mathcal{V}_{S}=(L_{S},\emptyset,H_{S},\emptyset,T_{S})$, where
$T_{S}:=\left\\{t\in T\,\middle|\,\text{\sc supp}(t)\subseteq S\right\\}.$ We
claim that the vass satisfies the conditions $\Theta_{1}$ and $\Theta_{2}$ of
Lemma 4.1.

We consider $\Theta_{1}$ first. Let $\pi:q(\mathbf{0})\dashrightarrow
q^{\prime}(\mathbf{0})$ and
$\pi^{\prime}:q^{\prime}(\mathbf{0})\dashrightarrow q(\mathbf{0})$ be the
pseudo-runs in (LABEL:eq:psruns). By applying all permutations
$\sigma\in\text{Aut}_{\mathbb{A}\setminus S}(\mathbb{A})$ to their
concatenation $\pi;\pi^{\prime}:q(\mathbf{0})\dashrightarrow
q^{\prime}(\mathbf{0})\dashrightarrow q(\mathbf{0})$ , and concatenating all
the $|S|!$ resulting cyclic pseudo-runs, we get a cyclic pseudo-run
$\delta:q(\mathbf{0})\dashrightarrow q(\mathbf{0})$. This pseudo-run uses
every transition from $T_{S}$ at least once, since $\pi$ uses a representative
of every orbit of $T$, and the following fact holds:

######  Claim 5.

Let $t,t^{\prime}\in T$ be two transitions in the same orbit such that
$\text{\sc supp}(t),\text{\sc supp}(t^{\prime})\subseteq S$. Then
$t^{\prime}=\sigma(t)$ for some $\sigma\in\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})$.

Likewise we get a cyclic pseudo-run
$\delta^{\prime}:q^{\prime}(\mathbf{0})\dashrightarrow q^{\prime}(\mathbf{0})$
that uses every transition from $T_{S}$ at least once. Furthermore, for every
$m\in\mathbb{N}$, the $m$-fold concatenation of $\delta$ or $\delta^{\prime}$
yields a cyclic pseudo-run that uses every transition from $T_{S}$ at least
$m$ times. We thus have two pseudo-runs

$\displaystyle\delta^{m};\pi\ :\ q(\mathbf{0})\dashrightarrow
q^{\prime}(\mathbf{0})\qquad\qquad\qquad(\delta^{\prime})^{m};\pi^{\prime}\ :\
q(\mathbf{0})\dashleftarrow q^{\prime}(\mathbf{0})$

each of them using every transition from $T_{S}$ at least $m$ times. Thus the
vass $\mathcal{V}_{S}$ satisfies two instances of $\Theta_{1}$, one towards a
run from $q(\mathbf{0})\longrightarrow q^{\prime}(\mathbf{0})$ and the other
one towards a run from $q^{\prime}(\mathbf{0})\longrightarrow q(\mathbf{0})$.

Now we concentrate on $\Theta_{2}$. We proceed similarly as before, namely
apply all automorphisms $\sigma\in\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})$ to $\mathbf{\Delta}$, and sum up all the resulting vectors:

$\mathbf{\Delta}_{S}\ :=\
\oplus\left\\{\sigma(\mathbf{\Delta})\,\middle|\,\sigma\in\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})\right\\}.$

Let $\overline{\mathbf{\Delta}}_{S}:{H\cup P{\times}S}\to_{\text{\tiny
fin}}\mathbb{N}$ be the restriction of $\mathbf{\Delta}_{S}$ to $H\cup
P{\times S}$. Knowing that $\mathbf{\Delta}\gg\mathbf{0}$, we deduce that
$\mathbf{\Delta}_{S}(h)>0$ for every $h\in H$, and
$\mathbf{\Delta}_{S}(p,a)>0$ for every $(p,a)\in P\times S$. In other words,
$\overline{\mathbf{\Delta}}_{S}\gg\mathbf{0}$. By applying all automorphisms
$\sigma\in\text{Aut}_{\mathbb{A}\setminus S}(\mathbb{A})$ to the run
$q(\mathbf{0})\longrightarrow q(\mathbf{\Delta})$ in $\mathbf{\Phi}_{2}$, and
concatenating all the resulting runs, we get a run
$q(\mathbf{0})\longrightarrow q(\mathbf{\Delta}_{S})$ in $\mathcal{V}$.
Clearly, only atoms from $S$ appear in this run, and therefore it is also a
run $q(\mathbf{0})\longrightarrow q(\overline{\mathbf{\Delta}}_{S})$ in
$\mathcal{V}_{S}$. In a similar way we define vectors
$\overline{\mathbf{\Delta}}_{S}^{\prime}$, $\overline{\mathbf{\Gamma}}_{S}$
and $\overline{\mathbf{\Gamma}}_{S}^{\prime}$, and the corresponding runs in
$\mathcal{V}_{S}$:

$\displaystyle q(\mathbf{0})\longrightarrow
q(\overline{\mathbf{\Delta}}_{S})\qquad\qquad
q^{\prime}(\overline{\mathbf{\Delta}}^{\prime}_{S})\longrightarrow
q^{\prime}(\mathbf{0})$ (7) $\displaystyle q(\mathbf{0})\longleftarrow
q(\overline{\mathbf{\Gamma}}_{S})\qquad\qquad
q^{\prime}(\overline{\mathbf{\Gamma}}^{\prime}_{S})\longleftarrow
q^{\prime}(\mathbf{0}).$ (8)

Therefore, the vass $\mathcal{V}_{S}$ satisfies two instances of $\Theta_{2}$,
one towards a run from $q(\mathbf{0})\longrightarrow q^{\prime}(\mathbf{0})$
and the other one towards a run $q^{\prime}(\mathbf{0})\longrightarrow
q(\mathbf{0})$.

Finally, using Lemma 4.1 we deduce two runs in $\mathcal{V}_{S}$. Both the
runs are automatically also runs in $\mathcal{V}$. This completes the proof.

###  5.1 Reduction algorithm

As the _rank_ of a well-supported dvass $\mathcal{V}=(L,\mathcal{R},H,P,T)$ we
take the triple $\text{\sc Rank}(\mathcal{V})=(|P|,|H|,||T||)$, consisting of
the number of atom places, the number of plain places, and the number of
orbits $||T||$ the set $T$ partitions into. Ranks are compared
lexicographically.

Given a well-supported dvass $\mathcal{V}$, the algorithm verifies the
conditions $\mathbf{\Phi}_{1}$ and $\mathbf{\Phi}_{2}$. If they are all
satisfied, it answers positively, relying on Lemma 5.1. Otherwise, depending
on which of the conditions is violated, the algorithm either immediately
answers negatively, or applies a reduction step, as outlined below. Each of
the steps produces a new dvass $\mathcal{V}^{\prime}$ which of strictly
smaller rank, which guarantees termination. Finally, when both $P$ and $H$ are
empty, the problem reduces to reachability from $q$ to $q^{\prime}$ in state
graph $\text{\sc Graph}(\mathcal{V})$, which is decidable due to:

######  Lemma 5.3.

For a set $E\subseteq Q\times Q$ of edges between states, given as a finite
union of orbits, and a pair $(s,s^{\prime})\in Q\times Q$, it is decidable if
there is a path from $s$ to $s^{\prime}$ in the graph $(Q,E)$.

######  Proof 5.4.

The orbit of an edge $((\ell,\nu),(\ell^{\prime},\nu^{\prime}))\in E$ is
determined by the following data: locations $\ell,\ell^{\prime}$; the inverse
images $\nu^{-1}(\bot),\ (\nu^{\prime})^{-1}(\bot);$ and the equality type of
the remaining entries in $\nu$ and $\nu^{\prime}$, that is:

$\left\\{(r,r^{\prime})\,\middle|\,\nu(r)=\nu(r^{\prime})\neq\bot\right\\}\quad\left\\{(r,r^{\prime})\,\middle|\,\nu^{\prime}(r)=\nu^{\prime}(r^{\prime})\neq\bot\right\\}\quad\left\\{(r,r^{\prime})\,\middle|\,\nu(r)=\nu^{\prime}(r^{\prime})\neq\bot\right\\}.$

Using equational reasoning, one computes the transitive closure $E^{*}$ of
$E$, by consecutively adding to $E^{*}$ every new orbit which is forced to be
included in $E^{*}$ by some two orbits already included in $E^{*}$, until
saturation. Termination is guaranteed as $Q\times Q$ is orbit-finite. The
transitive closure is thus forcedly a finite union of orbits. Finally, one
tests if the orbit of $(s,s^{\prime})$ is included in $E^{*}$.

For future use we note an immediate consequence of the above proof: for every
pair of states, if there is a path from one to the other, then there is also a
path of bounded length. This implies a bound on the number of atoms involved:

######  Corollary 5.5.

There is an effective bound $b(Q)\in\mathbb{N}$ such that whenever there is a
path from $s\in Q$ to $s^{\prime}\in Q$ in $(Q,E)$, then there is such a path
$\pi$ with $|\text{\sc supp}(\pi)|\leq b(Q)$.

Below we describe the two reduction steps, proving their progress property
(decreasing rank), correctness and effectiveness.

#### Violation of $\mathbf{\Phi}_{1}$.

Suppose $\mathcal{V}$ violates $\mathbf{\Phi}_{1}$. If states $q,q^{\prime}$
are not in the same strongly connected component of $\text{\sc Graph}(T)$,
which is testable using Lemma 5.3, then configurations $q(\mathbf{0})$,
$q^{\prime}(\mathbf{0})$ are clearly not bi-reachable and the algorithm
answers negatively. Otherwise, the algorithm constructs a dvass
$\mathcal{V}^{\prime}$ of smaller rank such that bi-reachability of
$q(\mathbf{0})$ and $q^{\prime}(\mathbf{0})$ in $\mathcal{V}$ is equivalent to
their bi-reachability in $\mathcal{V}^{\prime}$.

Let $\text{\sc Graph}(T)=(Q,E)$. Transitions witnessing bi-reachability of
$q(\mathbf{0})$ and $q^{\prime}(\mathbf{0})$, namely used in some cyclic run
$q(\mathbf{0})\longrightarrow q^{\prime}(\mathbf{0})\longrightarrow
q(\mathbf{0})$, form a cycle in $\text{\sc Graph}(T)$. In consequence, a
transition $(s,\mathbf{v},s^{\prime})\in T$ may be useful for bi-reachability
only if the edge $(s,s^{\prime})$ belongs to the strongly connected component
of $\text{\sc Graph}(T)$ containing $q$ and $q^{\prime}$. Therefore bi-
reachability of $q(\mathbf{0})$, $q^{\prime}(\mathbf{0})$ in $\mathcal{V}$
reduces to bi-reachability of $q(\mathbf{0})$, $q^{\prime}(\mathbf{0})$ in
$\mathcal{V}^{\prime}$ obtained by restriction to the strongly connected
component of $q$ and $q^{\prime}$. This component is computed by enumerating
all orbits included in $E$. For every orbit $o\subseteq E$ one chooses a
representative $(s,s^{\prime})\in o$, and uses Lemma 5.3 to test reachability,
in $\text{\sc Graph}(T)$, of the four pairs: $(q,s)$, $(q^{\prime},s)$,
$(s^{\prime},q)$ or $(q^{\prime},s^{\prime})$. Then one removes from $T$ all
orbits of transitions $(s,\mathbf{v},s^{\prime})$ such that reachability test
fails for any of the four pairs above. The resulting set of transitions is
still a finite union of orbits. Consequently, from now on we may assume,
w.l.o.g., that $\text{\sc Graph}(T)$ is strongly connected.

Call a transition _useful_ if it is used by some pseudo-run
$q(\mathbf{0})\dashrightarrow q^{\prime}(\mathbf{0})$, and also by some
pseudo-run $q^{\prime}(\mathbf{0})\dashrightarrow q(\mathbf{0})$. Note that
the set $U\subseteq T$ of useful transitions is closed under the action of
$\text{Aut}(\mathbb{A})$, since the sets of pseudo-runs of the above form are
so. Usefulness is thus a property of an orbit of transitions, and hence $U$ is
a union of orbits included in $T$.

######  Lemma 5.6.

$\mathbf{\Phi}_{1}$ holds if and only if all (orbits of) transitions are
useful.

######  Proof 5.7.

The two pseudo-runs (LABEL:eq:psruns) postulated by $\mathbf{\Phi}_{1}$ prove
usefulness of all orbits. In the opposite direction, assuming all orbits of
transitions are useful, from each such orbit in $T$ we pick a representative
transition, and choose two arbitrary pseudo-runs using this transition. By
concatenating all these runs we get $\mathbf{\Phi}_{1}$.

We define a dvass $\mathcal{V}^{\prime}$ by removing some useless orbit of
transitions, $\mathcal{V}^{\prime}=(L,\mathcal{R},H,P,T^{\prime})$. It has the
same locations, registers and places as $\mathcal{V}$.

######  Lemma 5.8 (Progress).

$||T^{\prime}||<||T||$, and hence $\text{\sc
Rank}(\mathcal{V}^{\prime})<\text{\sc Rank}(\mathcal{V})$.

######  Proof 5.9.

As some useless orbit of transitions is removed from $T^{\prime}$, we have
$||T^{\prime}||<||T||$, and therefore $\text{\sc
Rank}(\mathcal{V}^{\prime})=(|P|,|H|,||T^{\prime}||)<(|P|,|H|,||T||)=\text{\sc
Rank}(\mathcal{V})$.

######  Lemma 5.10 (Correctness).

The configurations $q(\mathbf{0})$, $q^{\prime}(\mathbf{0})$ are bi-reachable
in $\mathcal{V}$ if and only if they are bi-reachable in
$\mathcal{V}^{\prime}$.

######  Proof 5.11.

Indeed, useless transitions can not be used in runs between $q(\mathbf{0})$
and $q^{\prime}(\mathbf{0})$.

######  Lemma 5.12 (Effectiveness 1).

The condition $\mathbf{\Phi}_{1}$ is decidable.

######  Proof 5.13.

Aiming at reduction to Multiset sum (recall Lemma 2.4), we prove the following
characterisation: there are two pseudo-runs $q(\mathbf{0})\dashrightarrow
q^{\prime}(\mathbf{0})$ and $q^{\prime}(\mathbf{0})\dashrightarrow
q(\mathbf{0})$, each of them using some transition from every orbit in $T$,
exactly when there are two finite multisets
$\mathbf{f},\mathbf{f}^{\prime}:{T}\to_{\text{\tiny fin}}\mathbb{N}$ of
transitions such that $\mathbf{f}$ satisfies the following condition:

  1. (a)

the multiset contains at least one transition from every orbit in $T$.

plus the following conditions (b)–(e), to which we refer jointly as $\text{\sc
State-Eq}(q,q^{\prime})$:

  1. (b)

the sum of effects of all transitions is $\mathbf{0}$,

  2. (c)

for every state different than $q,q^{\prime}$, the number of incoming
transitions equals the number of outgoing ones,

  3. (d)

the number of transitions outgoing from $q$ exceeds by one the number of
incoming ones,

  4. (e)

the number of transitions incoming to $q^{\prime}$ exceeds by one the number
of outgoing ones;

and $\mathbf{f}^{\prime}$ satisfies (a) and $\text{\sc State-
Eq}(q^{\prime},q)$, i.e., the conditions (b), (c) plus the symmetric versions
of (d) and (e) with $q$ and $q^{\prime}$ swapped.

The only if direction of the characterisation is immediate, as the multiset of
transitions used in a pseudo-run $q(\mathbf{0})\dashrightarrow
q^{\prime}(\mathbf{0})$ necessarily satisfies all the conditions (a)–(e), and
likewise for a pseudo-run $q^{\prime}(\mathbf{0})\dashrightarrow
q(\mathbf{0})$. For the opposite direction, consider a finite multiset
$\mathbf{f}$ satisfying (a) and $\text{\sc State-Eq}(q,q^{\prime})$ and
$\mathbf{f}^{\prime}$ satisfying (a) and $\text{\sc State-Eq}(q^{\prime},q)$.
Let

$S\ :=\ \text{\sc supp}(\mathbf{f})\cup\text{\sc supp}(\mathbf{f}^{\prime})$

be the (finite) set of atoms used in all transitions involved. Similarly as in
the proof of Lemma 5.1 we use the subgroup $\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})\subseteq\text{Aut}(\mathbb{A})$ of automorphisms $\sigma$ of
$\mathbb{A}$ that are identity outside of $S$, and define a plain vass
$\mathcal{V}_{S}=(L_{S},\emptyset,H_{S},\emptyset,T_{S})$ by restricting the
set of atoms to $S$. Locations of $\mathcal{V}_{S}$ are
$L_{S}:=L\times(\mathcal{R}\to S\cup\\{\bot\\})$, its places are $H_{S}:=H\cup
P{\times}S$, and its transitions $T_{S}\subseteq T$ are all transitions of
$\mathcal{V}$ that use only atoms from $S$: $T_{S}=\left\\{t\in
T\,\middle|\,\text{\sc supp}(t)\subseteq S\right\\}.$ The state graph
$\text{\sc Graph}(T_{S})$ is an induced subgraph of $\text{\sc Graph}(T)$. As
$\text{\sc Graph}(T)$ is strongly connected, we use Corollary 5.5 to deduce
that, for sufficiently large $S$, the state graph $\text{\sc Graph}(T_{S})$ is
also strongly connected. Therefore we enlarge $S$, if necessary, to assure
that $\text{\sc Graph}(T_{S})$ is strongly connected.

As finite multisets $\mathbf{f},\mathbf{f}^{\prime}$ are just nonnegative
vectors ${T}\to_{\text{\tiny fin}}\mathbb{N}$, they inherit the natural
(pointwise) action of $\text{Aut}(\mathbb{A})$. Basing on $\mathbf{f}$,
$\mathbf{f}^{\prime}$ we define two larger multisets of transitions by
applying all automorphisms from $\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})$ to $\mathbf{f}$ and $\mathbf{f}^{\prime}$, respectively, and
summing up all the resulting multisets:

$\mathbf{g}\ :=\
\oplus\left\\{\sigma(\mathbf{f})\,\middle|\,\sigma\in\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})\right\\}\qquad\qquad\mathbf{g}^{\prime}\ :=\
\oplus\left\\{\sigma(\mathbf{f}^{\prime})\,\middle|\,\sigma\in\text{Aut}_{\mathbb{A}\setminus
S}(\mathbb{A})\right\\}.$

By condition (b) and Claim 5, each of $\mathbf{g},\mathbf{g}^{\prime}$
contains all transitions from $T_{S}$. Furthermore, the multiset
$\mathbf{h}=\mathbf{f}\oplus\mathbf{g}\oplus\mathbf{g}^{\prime}$ satisfies
$\text{\sc State-Eq}(\widehat{q},\widehat{q}^{\prime})$, where $\widehat{q}$,
$\widehat{q}^{\prime}$ are locations (=states) of $\mathcal{V}_{S}$
corresponding to $q$ and $q^{\prime}$ respectively. Likewise, the multiset
$\mathbf{h}^{\prime}=\mathbf{f}^{\prime}\oplus\mathbf{g}\oplus\mathbf{g}^{\prime}$
satisfies $\text{\sc State-Eq}(\widehat{q}^{\prime},\widehat{q})$. Using the
standard Euler argument in the (strongly) connected graph $\text{\sc
Graph}(T_{S})$, and relying on conditions (c)–(e), we deduce existence of a
pseudo-run in $\mathcal{V}_{S}$ that uses exactly transitions $\mathbf{h}$.
Due to condition (b), this is a pseudo-run
$\widehat{q}(\mathbf{0})\dashrightarrow\widehat{q}^{\prime}(\mathbf{0})$ in
$\mathcal{V}_{S}$. Likewise we deduce a pseudo-run
$\widehat{q}^{\prime}(\mathbf{0})\dashrightarrow\widehat{q}(\mathbf{0})$ in
$\mathcal{V}_{S}$. The pseudo-runs are essentially also pseudo-runs in
$\mathcal{V}$, both supported by $S$, and both using some transition from
every orbit in $T$. This completes the proof of the characterisation.

In order to check existence of a finite multiset $\mathbf{f}$ satisfying
conditions (a)–(e), we apply the algorithm for the Multiset Sum as follows,
cf. Lemma 2.4 (likewise we check existence of $\mathbf{f}^{\prime}$). Let
$X=H\cup P{\times}\mathbb{A}$ and $X^{\prime}=X\uplus Q\uplus O$, where
$O=\left\\{\text{\sc Orbit}(t)\,\middle|\,t\in T\right\\}$. The set
$X^{\prime}$ is orbit-finite. Let every transition
$t=(s,\mathbf{v},s^{\prime})$ determine two vectors
$\mathbf{x}_{t},\mathbf{y}_{t}:{X^{\prime}}\to_{\text{\tiny fin}}\mathbb{Z}$
that extend the vector $\mathbf{v}:{X}\to_{\text{\tiny fin}}\mathbb{Z}$ as
follows:

$\displaystyle\begin{aligned}
\mathbf{x}_{t}(s)=-1\qquad\qquad\mathbf{x}_{t}(s^{\prime})=1\qquad\qquad\mathbf{x}_{t}(\text{\sc
Orbit}(t))=1,\\\
\mathbf{y}_{t}(s)=-1\qquad\qquad\mathbf{y}_{t}(s^{\prime})=1\qquad\qquad\mathbf{y}_{t}(\text{\sc
Orbit}(t))=0,\end{aligned}$ (9)

and $\mathbf{x}_{t}(x)=\mathbf{y}_{t}(x)=0$ for other elements $x\in
X^{\prime}\setminus X$. Intuitively, the first two columns intend to track
contribution of $t$ to the number of transitions outgoing from $s$, or
incoming to $s^{\prime}$, while the latter one intends to track the number of
usages of $\text{\sc Orbit}(t)$. Likewise, we define a target vector
$\mathbf{b}:{X^{\prime}}\to_{\text{\tiny fin}}\mathbb{Z}$, by extending
$\mathbf{0}:{X}\to_{\text{\tiny fin}}\mathbb{Z}$ by

$\displaystyle\begin{aligned}
\mathbf{b}(q)=-1\qquad\qquad\mathbf{b}(q^{\prime})=1\qquad\qquad\mathbf{b}(o)=1\qquad(\text{for
every }o\in O),\end{aligned}$ (10)

and $\mathbf{b}(s)=0$ for other states $s\in
Q\setminus\left\\{q,q^{\prime}\right\\}$. Let
$M=\left\\{\mathbf{x}_{t},\mathbf{y}_{t}\,\middle|\,t\in T\right\\}$. It
remains to prove that the conditions (a)–(e) hold for some finite multiset
$\mathbf{f}$ of transitions from $T$ exactly when $(M,\mathbf{b})$ is a
positive instance of Multiset Sum, namely $\mathbf{b}$ is a sum of a finite
multiset of vectors from $M$. Indeed, consider such a sum:

$\displaystyle\mathbf{b}\ =\
\mathbf{x}_{t_{1}}+\ldots+\mathbf{x}_{t_{n}}+\mathbf{y}_{u_{1}}+\ldots+\mathbf{y}_{u_{m}}$
(11)

corresponding to the multiset of transitions
$\left\\{t_{1},\ldots,t_{n},u_{1},\ldots,u_{m}\right\\}$. As $\mathbf{b}(c)=0$
for all $c\in H\cup P{\times}\mathbb{A}$, the condition (b) is equivalent to
the equality (11) restricted to $H\cup P{\times}\mathbb{A}$. As
$\mathbf{b}(s)=0$ for $s\in Q\setminus\left\\{q,q^{\prime}\right\\}$,
condition (c) is equivalent to the equality (11) restricted to
$Q\setminus\left\\{q,q^{\prime}\right\\}$. By the first two columns in (9) and
(10), the conditions (d) and (e) are equivalent to the equality (11)
restricted to $\left\\{q,q^{\prime}\right\\}$. Finally, by the last column in
(9) and (10), the condition (a) holds exactly when each orbit in $T$ has
exactly one representative among $t_{1},\ldots,t_{n}$, which in turn is
equivalent to the equality (11) restricted to $O$.

######  Lemma 5.14 (Effectiveness 2).

When $\mathbf{\Phi}_{1}$ fails, some useless orbit of transitions is
computable.

######  Proof 5.15.

Suppose $\mathbf{\Phi}_{1}$ fails. Let $O=\left\\{\text{\sc
Orbit}(t)\,\middle|\,t\in T\right\\}$ be the set of all orbits in $T$. We call
an orbit $o\in O$ _good_ if there is a finite multiset of transitions
$\mathbf{f}$ that contains some transition from $o$ and safisfies $\text{\sc
State-Eq}(q,q^{\prime})$; and also there is a multiset $\mathbf{f}^{\prime}$
that contains some transition from $o$ and safisfies $\text{\sc State-
Eq}(q^{\prime},q)$. Otherwise we call $o$ _bad_.

######  Claim 6.

There is some bad orbit.

Suppose, contrarily, that all orbits are good. For each orbit $o$ there is
thus respective multisets $\mathbf{f}_{o},\mathbf{f}^{\prime}_{o}$. Let

$\mathbf{g}\ :=\ \oplus\left\\{\mathbf{f}_{o}\,\middle|\,o\in
O\right\\}\qquad\qquad\mathbf{g}^{\prime}\ :=\
\oplus\left\\{\mathbf{f}^{\prime}_{o}\,\middle|\,o\in O\right\\}.$

Then the multiset $\mathbf{f}\oplus\mathbf{g}\oplus\mathbf{g}^{\prime}$ would
satisfy (a) and $\text{\sc State-Eq}(q,q^{\prime})$, and the multiset
$\mathbf{f}^{\prime}\oplus\mathbf{g}\oplus\mathbf{g}^{\prime}$ would satisfy
(a) and $\text{\sc State-Eq}(q^{\prime},q)$, which would implies
$\mathbf{\Phi}_{1}$ according to the characterisation in the proof of Lemma
5.12.

Clearly, a bad orbit is useless. The algorithm test each orbit and returns any
bad one, which is doable due to:

######  Claim 7.

It is decidable if a given orbit $o\in O$ is good.

We reduce to Multiset sum (Lemma 2.4), by two slight adaptations of the
reduction in the proof of Lemma 5.12: first, the vectors $\mathbf{x}_{t}$ are
considered only for $t\in o$ (instead of all $t\in T$); second, we modify the
target vector by stipulating $\mathbf{b}(o)=1$ only for the orbit $o$, while
$\mathbf{b}(o^{\prime})=0$ for all other orbits $o^{\prime}\in O$.

#### Violation of $\mathbf{\Phi}_{2}$.

Suppose $\mathcal{V}$ violates $\mathbf{\Phi}_{2}$. We define a dvass
$\mathcal{V}^{\prime}$ of smaller rank such that bi-reachability of
$q(\mathbf{0})$ and $q^{\prime}(\mathbf{0})$ in $\mathcal{V}$ is equivalent to
their bi-reachability in $\mathcal{V}^{\prime}$.

Any run of the form $q(\mathbf{0})\longrightarrow q(\mathbf{\Delta})$ (resp.
$q(\mathbf{\Delta})\longrightarrow q(\mathbf{0})$) we call _forward_ (resp.
_backward_) _pump_ from $q$. Likewise we define forward (resp. backward) pumps
from $q^{\prime}$.

A plain place $h\in H$ (resp. an atom place $p\in P$) we call _forward
pumpable_ from $q(\mathbf{0})$ if there is a pump
$q(\mathbf{0})\longrightarrow q(\mathbf{\Delta})$ such that
$\mathbf{\Delta}(h)>0$ (resp. $\mathbf{\Delta}(p,a)>0$ for some atom
$a\in\mathbb{A}$). Symmetrically, a place $h\in H$ (resp. $p\in P$) we call
_backward pumpable_ from $q(\mathbf{0})$ if there is a pump
$q(\mathbf{\Delta})\longrightarrow q(\mathbf{0})$ such that
$\mathbf{\Delta}(h)>0$ (resp. $\mathbf{\Delta}(p,a)>0$ for some atom
$a\in\mathbb{A}$). Likewise we define places forward (resp. backward) pumpable
from $q^{\prime}(\mathbf{0})$. Finally, a (plain or atom) place is called
_pumpable_ if it is forward and backward pumpable both from $q(\mathbf{0})$
and from $q^{\prime}(\mathbf{0})$. Otherwise, the place is called
_unpumpable_.

######  Lemma 5.16.

$\mathbf{\Phi}_{2}$ holds if and only if all places are pumpable.

######  Proof 5.17.

In one direction, $\mathbf{\Phi}_{2}$ amount to _simultaneous_ (= using one
pump) forward and backward pumpability of all places, from both $q$ and
$q^{\prime}$. In the converse direction, suppose all places are forward and
backward pumpable from both $q$ and $q^{\prime}$. We observe that forward
(resp. backward) pumps from $q$ compose, and hence all places are
_simultaneously_ forward (resp. backward) pumpable from $q$. Likewise for
$q^{\prime}$.

We now introduce a suitable version of boundedness. In case of plain places
$h\in H$ boundedness applies, as expected, to the value $\mathbf{v}(h)$ in a
configuration $s(\mathbf{v})$. On the other hand in case of atom places $p\in
P$, boundedness applies to the number of tokens on a place. For uniformity we
define the size of a place $p\in P$ in a vector $\mathbf{v}$ as

$\mathbf{v}(p)=\sum\left\\{\mathbf{v}(p,a)\,\middle|\,a\in\mathbb{A},\
\mathbf{v}(p,a)>0\right\\}\in\mathbb{N}.$

For a family $\mathcal{F}$ of runs, we say that a place $c\in H\cup P$ is
_bounded on $\mathcal{F}$ by $B\in\mathbb{N}$_ if for every configuration
$s(\mathbf{v})$ appearing in every run in the family $\mathcal{F}$,
$\mathbf{v}(c)\leq B$. A place is _bounded on_ $\mathcal{F}$, if it is bounded
on $\mathcal{F}$ by some $B$. Otherwise, the place is called _unbounded_ on
$\mathcal{F}$.

As forward (resp. backward) pumps compose, every place which is forward (resp.
backward) pumpable from $q$ (resp. $q^{\prime}$) is necessarily unbounded on
respective pumps. We show the opposite implication, namely unpumpable places
are bounded on respective pumps:

######  Lemma 5.18.

A place which is not forward (resp. backward) pumpable from $q$ is bounded on
forward (resp. backward) pumps from $q$. Likewise for $q^{\prime}$.

######  Proof 5.19.

W.l.o.g. we focus on forward pumps from $q$ only. (Backward pumps are tackled
similarly as forward ones, but in the _reversed_ dvass, whose transitions
$\left\\{(s^{\prime},-\mathbf{v},s)\,\middle|\,(s,\mathbf{v},s^{\prime})\in
T\right\\}$ are inverses of transitions of $\mathcal{V}$.) Assuming that a
place $c\in H\cup P$ is unbounded on forward pumps from $q$, we show that $c$
is forward pumpable from $q$. Unboundedness of $c$ means that for every
$i\in\mathbb{N}$ there is a run

$\displaystyle q(\mathbf{0})\longrightarrow
s_{i}(\mathbf{v}_{i})\longrightarrow q(\mathbf{\Delta}_{i})$ (12)

such that $n_{i}:=\mathbf{v}_{i}(c)>i$. By choosing a subsequence of
$(n_{i})_{i}$ we may assume w.l.o.g. that this sequence is strictly
increasing. As $\sqsubseteq$ is a wqo, for some $j<i$ we have
$s_{j}(\mathbf{v}_{j})\sqsubseteq s_{i}(\mathbf{v}_{i})$, i.e., there is some
$\sigma\in\text{Aut}(\mathbb{A})$ such that $\sigma(s_{j})=s_{i}$ and
$\sigma(\mathbf{v}_{j})\leq\mathbf{v}_{i}$. Equivalently,
$\sigma(\mathbf{v}_{j})+\mathbf{\Delta}=\mathbf{v}_{i}$ for some nonnegative
vector $\mathbf{\Delta}$. Therefore, we can construct a new run, by first
using the first half of (12) to go from $p(\mathbf{0})$ to
$s_{i}(\mathbf{v}_{i})$, and then applying $\sigma$ to the second half
$s_{j}(\mathbf{v}_{j})\longrightarrow q(\mathbf{\Delta}_{j})$ to return back
from $\sigma(s_{j}(\mathbf{v}_{j}))$:

$q(\mathbf{0})\longrightarrow
s_{i}(\mathbf{v}_{i})=\sigma(s_{j})(\sigma(\mathbf{v}_{j})+\mathbf{\Delta})\longrightarrow
q(\sigma(\mathbf{\Delta}_{j})+\mathbf{\Delta}).$

By strict monotonicity of $(n_{i})_{i}$ we have $n_{j}<n_{i}$, which implies
$\mathbf{\Delta}(c)>0$. The place $c$ is thus forward pumpable from $q$, as
required.

Let $B\in\mathbb{N}$ be the universal bound for all unpumpable places on all
respective pumps. Formally, let’s assume that $B$ bounds every place which is
not forward (resp. backward) pumpable from $q$, on all forward (resp.
backward) pumps from $q$, and $B$ also bounds every place which is not forward
(resp. backward) pumpable from $q^{\prime}$, on all forward (resp. backward)
pumps from $q^{\prime}$. As $\mathcal{V}$ violates $\mathbf{\Phi}_{2}$, we
know by Lemma 5.16 that there are some unpumpable places. We define a dvass
$\mathcal{V}^{\prime}=(L,\mathcal{R}^{\prime},H^{\prime},P^{\prime},T^{\prime})$
by, intuitively speaking, removing some such place. Let $X=H\cup
P{\times}\mathbb{A}$.

#### Case 1: some plain place is unpumpable.

Let $P^{\prime}:=P$ and $\mathcal{R}^{\prime}=\mathcal{R}$. We choose an
arbitrary unpumpable $h\in H$, and let
$H^{\prime}:=H\setminus\left\\{h\right\\}$. We keep track of values on $h$ by
extending the locations $L^{\prime}:=L\times\left\\{0\ldots B\right\\}$.
Finally, transitions $T^{\prime}$ are obtained from transitions $T$ by
replacing each $t\ =\ ((\ell,\mu),\mathbf{v},(\ell^{\prime},\mu^{\prime}))\in
T$ by all the transitions of the form

$t^{\prime}\ =\
((\langle\ell,n\rangle,\mu),\mathbf{v}^{\prime},(\langle\ell^{\prime},n+\mathbf{v}(h)\rangle,\mu^{\prime})),$

where $\mathbf{v}^{\prime}$ is the restriction of $\mathbf{v}:{(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}$ to $H^{\prime}\cup
P{\times}\mathbb{A}$.

#### Case 2: some atom place is unpumpable.

Let $L^{\prime}:=L$ and $H^{\prime}:=H$. We choose an arbitrary unpumpable
$p\in P$, remove place $p$, namely $P^{\prime}:=P\setminus\left\\{p\right\\}$,
and add $B$ new registers, namely
$\mathcal{R}^{\prime}=\mathcal{R}\cup\\{r_{1},\dots,r_{B}\\}$, which store,
intuitively speaking, every possible content of place $p$. Using the new
registers the transitions $T^{\prime}$ track, intuitively speaking, the effect
of transitions from $T$ on the removed place $p$. Every register valuation
$\mu$ naturally induces a vector
$\widehat{\mu}:{P{\times}\mathbb{A}}\to_{\text{\tiny fin}}\mathbb{N}$:
$\widehat{\mu}\ :=\ \oplus\left\\{(p,a)\,\middle|\,\mu(r_{i})=a\neq\bot,\
i\in\left\\{1\ldots B\right\\}\right\\}.$ Using this notation we define the
transitions $T^{\prime}$ by replacing every transition
$((\ell,\nu),\mathbf{v},(\ell^{\prime},\nu^{\prime}))\in T$ by all the
transitions of the form

$((\ell,\nu\uplus\mu),\mathbf{v}^{\prime},(\ell^{\prime},\nu^{\prime}\uplus\mu^{\prime})),$

where $\mathbf{v}^{\prime}$ is the restriction of $\mathbf{v}:{(H\cup
P{\times}\mathbb{A})}\to_{\text{\tiny fin}}\mathbb{Z}$ to $H\cup
P^{\prime}{\times}\mathbb{A}$, and
$\mathbf{v}=\mathbf{v}^{\prime}\oplus\widehat{\mu}^{\prime}\ominus\widehat{\mu}$.

######  Lemma 5.20 (Progress).

$\text{\sc Rank}(\mathcal{V}^{\prime})<\text{\sc Rank}(\mathcal{V})$.

######  Proof 5.21.

In the former case $P^{\prime}=P$ and $|H^{\prime}|<|H|$, while in the latter
case $|P^{\prime}|<|P|$. In each case, $\text{\sc
Rank}(\mathcal{V}^{\prime})=(|P^{\prime}|,|H^{\prime}|,||T^{\prime}||)<(|P|,|H|,||T||)=\text{\sc
Rank}(\mathcal{V})$.

Denote by $\widehat{q},\widehat{q}^{\prime}$ the states $q,q^{\prime}$,
respectively, extended with empty valuation of all the new registers
$\\{r_{1},\dots,r_{B}\\}$.

######  Lemma 5.22 (Correctness).

The configurations $q(\mathbf{0})$, $q^{\prime}(\mathbf{0})$ are bi-reachable
in $\mathcal{V}$ if and only if $\widehat{q}(\mathbf{0})$,
$\widehat{q}^{\prime}(\mathbf{0})$ are bi-reachable in $\mathcal{V}^{\prime}$.

######  Proof 5.23.

As $\mathcal{V}^{\prime}$ is obtained from $\mathcal{V}$ by restricting values
in configurations on some places, each run in $\mathcal{V}^{\prime}$ is
automatically a run in $\mathcal{V}$, and bi-reachability in
$\mathcal{V}^{\prime}$ implies bi-reachability in $\mathcal{V}$.

For the converse implication, suppose $q(\mathbf{0})$,
$q^{\prime}(\mathbf{0})$ are bi-reachable in $\mathcal{V}$, and fix two
arbitrary runs $\pi:q(\mathbf{0})\longrightarrow q^{\prime}(\mathbf{0})$ and
$\pi^{\prime}:q^{\prime}(\mathbf{0})\longrightarrow q(\mathbf{0})$. Consider
any unpumpable place $c\in H\cup P$ and suppose, w.l.o.g., that the place is
not forward pumpable from $q$. By Lemma 5.18 the place is bounded by $B$ on
all forward pumps from $q$. In particular, it is bounded by $B$ on the
composed run $\pi;\pi^{\prime}:q(\mathbf{0})\longrightarrow q(\mathbf{0})$,
i.e., on both $\pi$ and $\pi^{\prime}$. Therefore we know that in each
configurations $(s,\mathbf{v})$ in both runs, $\mathbf{v}(c)\leq B$. If $c\in
H$ we keep track of $\mathbf{(}c)$ in location; and if $c\in P$, we keep track
of all tokens on $c$ by storing their atoms in the new registers
$\\{r_{1},\dots,r_{B}\\}$. Therefore, both runs are realisable in
$\mathcal{V}^{\prime}$.

######  Lemma 5.24 (Effectiveness).

The set of pumpable places and the universal bound $B$ are computable (and
therefore the condition $\mathbf{\Phi}_{2}$ is decidable).

######  Proof 5.25.

Relying on Lemma 5.16, we test forward (resp. backward) pumpability of every
place from $q$ (and likewise from $q^{\prime}$). Specifically, to test if a
place is forward pumpable from $q$, we apply Lemma LABEL:lem:cover and compute
a simple-ideal representation of the coverability set $\text{\sc
Cover}(q(\mathbf{0}),q)$, given by simple functions
$\left\\{f_{1},\ldots,f_{n}\right\\}$. A plain place $h\in H$ is forward
pumpable from $q$ if $f_{i}(h)>0$ for some $i\in\left\\{1\ldots n\right\\}$;
and an atom place $p\in P$ is forward pumpable from $q$, if $f_{i}(p,a)>0$ for
some $i\in\left\\{1\ldots n\right\\}$ and $a\in\mathbb{A}$. Likewise we test
if a place is backward pumpable from $q$ (using the reverse dvass), or forward
(resp. backward) pumpable from $q^{\prime}$.

If there is some unpumpable place $c$, we apply Lemma LABEL:lem:cover again to
compute a simple-function representation
$G=\left\\{g_{1},\ldots,g_{m}\right\\}$ of the union of all coverability sets

$\displaystyle\bigcup_{s\in Q}\text{\sc Cover}(q(\mathbf{0}),s).$ (13)

This requires a finite number of invocations of the decision procedure of
Lemma LABEL:lem:cover, one per each orbit of the pair $(q,s)\in Q\times Q$ of
states. For a simple function $g\in G$ and an atom place $p\in P$ we define,
for uniformity, $g(p)\ :=\ \sum\left\\{g(p,a),\
g(p,a)>0\,\middle|\,a\in\mathbb{A}\right\\}$ (under the proviso that
$\omega+n=\omega+\omega=\omega$, and every infinite sum of non-zeros is
$\omega$). We claim that the bound $B$ is computed, be place $c$ a plain or
atom one, as the maximum

$B\ :=\ \max\left\\{g(c)\,\middle|\,g\in G,\ g(c)<\omega\right\\}.$

By Lemma 5.18, the place is bounded on all forward pumps from $q$, but may be
a priori unbounded on some other run, and therefore it may happen that
$g(c)=\omega$ for some $g\in G$. We claim however that $B$ is large enough as
a bound on pumps:

######  Claim 8.

The place $c$ is bounded on all forward pumps from $q$ by $B$.

We consider an atom place $p\in P$ (the argument for plain places is similar
but simpler). Suppose, towards contradiction, that some configuration
$s(\mathbf{v})$ on some forward pump from $q$ satisfies $\mathbf{v}(p)>B$. We
have thus two runs:

$\pi\ :\ q(\mathbf{0})\longrightarrow
s(\mathbf{v})\qquad\qquad\rho:s(\mathbf{v})\longrightarrow q(\mathbf{w})$

for some nonnegative vector $\mathbf{w}$. We have $\mathbf{v}\sqsubseteq g$
for some $g\in G$. As $\mathbf{v}(p)$ is larger than $g^{\prime}(p)<\omega$,
for all $g^{\prime}\in G$, we deduce that $g(p)=\omega$. As $g\\!\downarrow\ $
is included in the union of coverability sets (13), there is a configuration
$s(\overline{\mathbf{v}})$ reachable from $q(\mathbf{0})$ which is strictly
larger than $s(\mathbf{v})$ on place $p$:

$\overline{\pi}\ :\
q(\mathbf{0})\longrightarrow\overline{s}(\overline{\mathbf{v}})\qquad\qquad\mathbf{v}\sqsubset\overline{\mathbf{v}}\qquad\qquad\mathbf{v}(p)<\overline{\mathbf{v}}(p)$

which means that for some automorphism $\sigma$ and atom $a\in\mathbb{A}$ we
have

$\sigma(s)=\overline{s}\qquad\qquad\sigma(\mathbf{v})\leq\overline{\mathbf{v}}\qquad\qquad\sigma(\mathbf{v})(p,a)<\overline{\mathbf{v}}(p,a).$

Therefore, by composing runs $\overline{\pi}$ and $\sigma(\rho)$ we get a run

$\overline{\pi};\sigma(\rho)\ :\ q(\mathbf{0})\longrightarrow
q(\overline{\mathbf{w}})$

where $\overline{\mathbf{w}}(p,a)>0$, i.e., $p$ is forward pumpable from $q$,
which yields a contradiction. This completes the proof of the Lemma 5.24.

## References

  * [1] Mikołaj Bojańczyk.  Slightly infinite sets.  2019\.  URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  * [2] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota.  Automata theory in nominal sets.  Logical Methods in Computer Science, 10(3:4):paper 4, 2014.
  * [3] Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota, and Szymon Toruńczyk.  Turing machines with atoms.  In LICS, pages 183–192, 2013.
  * [4] Iliano Cervesato, Nancy A. Durgin, Patrick Lincoln, John C. Mitchell, and Andre Scedrov.  A meta-notation for protocol analysis.  In Proc. CSFW 1999, pages 55–69, 1999.
  * [5] Giorgio Delzanno.  An overview of MSR(C): A clp-based framework for the symbolic verification of parameterized concurrent systems.  Electr. Notes Theor. Comput. Sci., 76:65–82, 2002.
  * [6] Giorgio Delzanno.  Constraint multiset rewriting.  Technical Report DISI-TR-05-08, DISI, Universitá di Genova, 2005.
  * [7] Alain Finkel and Jean Goubault-Larrecq.  Forward analysis for wsts, part I: completions.  In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs, pages 433–444. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009.
  * [8] Alain Finkel and Jean Goubault-Larrecq.  Forward analysis for wsts, part II: complete WSTS.  Log. Methods Comput. Sci., 8(3), 2012.
  * [9] Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche.  Reachability in bidirected pushdown VASS.  In Proc. ICALP 2022, volume 229 of LIPIcs, pages 124:1–124:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
  * [10] Hartmann J. Genrich and Kurt Lautenbach.  System modelling with high-level Petri nets.  Theor. Comput. Sci., 13:109–136, 1981.
  * [11] A. Ghosh, P. Hofman, and S. Lasota.  Orbit-finite linear programming.  In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14, 2023.
  * [12] Arka Ghosh and Slawomir Lasota.  Equivariant ideals of polynomials.  CoRR, abs/2402.17604, 2024.  URL: https://doi.org/10.48550/arXiv.2402.17604, doi:10.48550/ARXIV.2402.17604.
  * [13] Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke.  Coverability trees for petri nets with unordered data.  In Bart Jacobs and Christof Löding, editors, Proc. FOSSACS 2016, volume 9634 of Lecture Notes in Computer Science, pages 445–461. Springer, 2016.
  * [14] Kurt Jensen.  Coloured Petri nets and the invariant-method.  Theor. Comput. Sci., 14:317–336, 1981.
  * [15] S. Rao Kosaraju.  Decidability of reachability in vector addition systems (preliminary version).  In Proc. STOC 1982, pages 267–281, 1982.
  * [16] Jean-Luc Lambert.  A structure to decide reachability in Petri nets.  Theor. Comput. Sci., 99(1):79–104, 1992.
  * [17] Slawomir Lasota.  Decidability border for Petri nets with data: WQO dichotomy conjecture.  In Proc. Petri Nets 2016, volume 9698 of Lecture Notes in Computer Science, pages 20–36. Springer, 2016.
  * [18] Slawomir Lasota.  VASS reachability in three steps.  CoRR, abs/1812.11966, 2018.  URL: http://arxiv.org/abs/1812.11966, arXiv:1812.11966.
  * [19] Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell.  Nets with tokens which carry data.  In Proc. ICATPN 2007, volume 4546 of Lecture Notes in Computer Science, pages 301–320. Springer, 2007.
  * [20] Ranko Lazic and Patrick Totzke.  What makes petri nets harder to verify: Stack or data?  In Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, volume 10160 of Lecture Notes in Computer Science, pages 144–161. Springer, 2017.
  * [21] Jérôme Leroux.  Vector addition system reversible reachability problem.  Log. Methods Comput. Sci., 9(1), 2013.
  * [22] Jérôme Leroux and Sylvain Schmitz.  Demystifying reachability in vector addition systems.  In Proc. LICS 2015, pages 56–67. IEEE Computer Society, 2015.
  * [23] Jérôme Leroux and Sylvain Schmitz.  Reachability in vector addition systems is primitive-recursive in fixed dimension.  In Proc. LICS 2019, pages 1–13. IEEE, 2019.
  * [24] Ernst W. Mayr.  An algorithm for the general Petri net reachability problem.  In Proc. STOC 1981, pages 238–246, 1981.
  * [25] Fernando Rosa-Velardo and David de Frutos-Escrig.  Decidability and complexity of Petri nets with unordered data.  Theor. Comput. Sci., 412(34):4439–4451, 2011.