[a] [a,b] [a,c]

# Branch-Well-Structured Transition Systems and Extensions

Benedikt Bollig0000-0003-0985-6115  ,  Alain Finkel0000-0003-0702-3232  and
Amrita Suresh0000-0001-6819-9093  Université Paris-Saclay, ENS Paris-Saclay,
CNRS, LMF, 91190, Gif-sur-Yvette, France  {benedikt.bollig, alain.finkel,
<EMAIL_ADDRESS>Institut Universitaire de France
University of Oxford, UK<EMAIL_ADDRESS>
###### Abstract.

We propose a relaxation to the definition of well-structured transition
systems (WSTS) while retaining the decidability of boundedness and non-
termination. In our class, we ease the well-quasi-ordered (wqo) condition to
be applicable only between states that are reachable one from another.
Furthermore, we also relax the monotony condition in the same way. While this
retains the decidability of non-termination and boundedness, it appears that
the coverability problem is undecidable. To this end, we define a new notion
of monotony, called cover-monotony, which is strictly more general than the
usual monotony and still allows us to decide a restricted form of the
coverability problem.

###### Key words and phrases:

verification and decidability and coverability and termination and well-quasi-
ordering

##  1\. Introduction

A well-structured transition system (WSTS), initially called structured
transition system in [Fin87, Fin90], is a mathematical framework used to model
and analyse the behaviour of concurrent and reactive systems. It provides a
formal representation of the system’s states, and the transitions between
them. The key characteristic of a WSTS is that it exhibits certain properties
that enable algorithmic verification of important system characteristics, such
as non-termination, boundedness, and coverability.

In a WSTS, the system is represented as a (potentially infinite) set of
_states_ , denoted by $X$ equipped with a _transition relation_
${\rightarrow}\subseteq X\times X$. $X$ may represent different
configurations, states of a computation, or states of a concurrent program,
depending on the specific context of the system being modelled. Furthermore,
the states in $X$ are partially ordered by a quasi-ordering relation, denoted
by $\leq$, and $\rightarrow$ fulfils one of various possible monotonies with
respect to $\leq$. To be considered a well-structured transition system, the
partial order $\leq$ on the set of states $X$ must be _well_ , i.e. well-
founded with no infinite antichains (Section 2 formally defines these
notions).

The theory of WSTS, although initially formulated in the late ’80s [Fin87], is
still being widely explored (refer to [FS01, ACJT00] for surveys). Some
notable recent developments in the theory include handling infinite branching
[BFM18], ideal abstraction [ZWH12], extensions over tree behaviours [Sch21,
LS15], etc. Because they provide a powerful framework for reasoning about
infinite-state systems and enable the development of effective algorithms for
automatic verification, WSTS have found applications in various areas,
including classically, Petri Nets and Lossy Channel Systems, but also recent
explorations in graph transformation systems [Öz22], program verification
[FP20], $\mu$-calculus [SG07, KSS04, BS13], cryptographic protocols [DS20],
Presburger counter machines [FG19], among others.

Since its development, a number of relaxations and extensions of the two core
assumptions of WSTS have been studied. Notably, with regards to the monotony,
the notion of transitive, stuttering monotonies has been studied [FS01]. With
regards to the well-quasi-order assumption, [BFM17] has shown that
coverability is still decidable without the assumption of wellness, with only
the absence of infinite antichains. They refer to this class as _well behaved
transition systems_ (WBTS). However, in the same paper, they also show that
this relaxation is too broad for the decidability of boundedness and non-
termination, and show classes of WBTS with undecidable boundedness and non-
termination properties.

In this work, we look at relaxing both the well-quasi-order and the monotony
assumptions, while still ensuring decidable non-termination and boundedness.
More precisely, we introduce the notion of _branch-well-quasi-order_ , which
is only applicable to states that are reachable one from another.
Interestingly, branch-wqo share many of the closure properties that wqo enjoy.
Similarly, we also relax the notion of monotony to _branch-monotony_ , which
requires only that the same sequence of actions can be repeated from two
states ordered by $\leq$. We call the systems which satisfy these two
conditions _branch-WSTS_. Branch-WSTS, though a strict superclass of WSTS,
still has decidable boundedness and non-termination, under the same
effectivity conditions.

We show examples of classes of systems studied in the literature, which are
not WSTS, but are branch-WSTS. Notably, there are non-trivial subclasses in
both counter machines and FIFO automata, two classes which are well-known to
be Turing-hard, which are branch-WSTS. Moreover, we show that coverability is,
in fact, undecidable for general branch-WSTS. This shows that WBTS and branch-
WSTS are incomparable. Furthermore, we show that the ideas of branch-monotony
can be verified along a single run in order to show non-termination and
unboundedness. This provides an algorithm to verify these properties for a
large subclass of counter machines and branch-wqo FIFO machines. Moreover, we
see that for FIFO machines and the prefix-ordering, the conditions that relate
to validity of branch-monotony along a single run imply infinite iterability,
as defined in [FP20].

The other major contribution of this work deals with coverability. Contrary to
[BFM17], we relax the notion of monotony, which we call _cover-monotony_ ,
while maintaining the well-quasi-order assumption, such that the resulting
class of systems have decidable coverability. For this class, which we refer
to as _cover-WSTS_ , we show that a restricted version of the coverability
problem is decidable, even in the absence of strong (or strict or transitive
or reflexive) monotony.

A preliminary version of this work has been presented at the 42nd
International Conference on Formal Techniques for Distributed Objects,
Components, and Systems (FORTE 2022). The contributions in this work extend
the conference version as follows:

This work further investigates the classes of branch-WSTS. We explicitly prove
that counter machines with restricted zero tests are branch-monotone.
Furthermore, in this work, we prove the conjecture we had stated in the
conference version claiming normalized input-bounded FIFO machines are branch-
WSTS. We also provide a sufficient condition for boundedness and non-
termination for a large subclass of counter machines and FIFO machines, which
strictly include branch-WSTS. Apart from this, we also provide explicit proofs
and examples of systems which we did not include in the conference version,
along with some additional properties, notably for branch-wqos.

Outline. Section 2 introduces terminology and some well-known results
concerning well-quasi-orderings and well-structured transition systems.
Section 3 defines branch-WSTS, and shows that both the boundedness and the
non-termination problems are decidable for such systems. Section 4 provides
some examples of branch-WSTS as well as provides a sufficient condition for
unboundedness and non-termination for a large class of counter and FIFO
machines (strictly including branch-WSTS). Section 5 investigates the
coverability problem for WSTS with relaxed conditions. We conclude in Section
6.

##  2\. Preliminaries

We denote the set of natural numbers as ${\rm Nature}$. We denote the standard
ordering on ${\rm Nature}$ by $\leq$. Given a set $A$, we denote by $|A|$ the
number of distinct elements in $A$.

Let $\Sigma$ be a finite alphabet, and $\Sigma^{*}$ be the set of finite words
over $\Sigma$. We denote the empty word by $\varepsilon$. The concatenation of
two words $u,v\in\Sigma$ is denoted by $u\cdot v$, or $u.v$, or simply $uv$.
Given $a\in\Sigma$ and $w\in\Sigma^{*}$, we let $|w|_{a}$ denote the number of
occurrences of $a$ in $w$. With this, we let
$\mathit{Alph}(w)=\\{a\in\Sigma\mid|w|_{a}\geq 1\\}$. A word $u\in\Sigma^{*}$
is a prefix (resp. suffix) of $w\in\Sigma^{*}$ if $w=u\cdot v$ (resp.
$w=v\cdot u$) for some $v\in\Sigma^{*}$. The sets of prefixes and suffixes of
$w\in\Sigma^{*}$ are denoted by $\mathit{Pref}(w)$ and $\mathit{Suf}(w)$
respectively. We denote the prefix ordering on words over an alphabet $\Sigma$
by $\preceq$. More specifically, for two words $u,w\in\Sigma^{*}$, we say
$u\preceq w$ if $u$ is a prefix of $w$.

###  2.1. Well-structured transition systems

We define some preliminary notions associated with well-structured transition
systems.

Quasi-orderings. Let $X$ be a set and ${\leq}\subseteq X\times X$ be a binary
relation over $X$, which we also write as $(X,\leq)$. We call $\leq$ a _quasi
ordering (qo)_ if it is reflexive and transitive. As usual, we call $\leq$ a
_partial ordering_ if it is a quasi-ordering and anti-symmetric (if $x\leq y$
and $y\leq x$, then $x=y$). We write $x<y$ if $x\leq y$ and $y\not\leq x$. If
$\leq$ is a partial ordering, $x<y$ is then equivalent to $x\leq y$ and $x\neq
y$.

To any $x\in X$, we associate the sets
$\mathord{\uparrow}x\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\\{y\mid
x\leq y\\}$ and
$\mathord{\downarrow}x\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\\{y\mid
y\leq x\\}$. Moreover, for $A\subseteq X$, we let
$\mathord{\uparrow}A\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\bigcup_{x\in
A}\mathord{\uparrow}x$ and
$\mathord{\downarrow}A\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}\bigcup_{x\in
A}\mathord{\downarrow}x$. We say that a set $A$ is _upward closed_ if
$A=\mathord{\uparrow}A$. Similarly, $A$ is _downward closed_ if
$A=\mathord{\downarrow}A$. A _basis_ of an upward-closed set $A$ is a set
$B\subseteq X$ such that $A=\mathord{\uparrow}B$.

We say $(X,\leq)$ is _well-founded_ if there is no infinite strictly
decreasing sequence of elements of $X$. An _antichain_ is a subset $A\subseteq
X$ such that any two distinct elements in the subset are incomparable, i.e.,
for every distinct $x,y\in A$, we have $x\not\leq y$ and $y\not\leq x$. For
example, consider the alphabet $\Sigma=\\{a,b\\}$. There exists an infinite
antichain $\\{b,ab,aab,...\\}$ with respect to the prefix ordering over
$\Sigma^{\ast}$.

An _ideal_ is a downward-closed set $I\subseteq X$ that is also _directed_ ,
i.e., it is non-empty and, for every $x,y\in I$, there exists $z\in I$ such
that $x\leq z$ and $y\leq z$. The set of ideals is denoted by
$\textsf{Ideals}(X)$.

Well-quasi-orderings. For the following definitions, we fix a qo $(X,\leq)$.
When a qo satisfies some additional property, we call it a well-quasi-
ordering:

A _well-quasi-ordering (wqo)_ is a qo $(X,\leq)$ such that every infinite
sequence $x_{0},x_{1},x_{2},\ldots$ over $X$ contains an _increasing pair_ ,
i.e., there are $i<j$ such that $x_{i}\leq x_{j}$.

For example, the set of natural numbers ${\rm Nature}$, along with the
standard ordering $\leq$ is a wqo. Moreover, $({\rm Nature}^{k},\leq)$, i.e.
the set of vectors of $k\geq 1$ natural numbers with component-wise ordering,
is a wqo [Dic13]. On the other hand, the prefix ordering on words over an
alphabet $\Sigma$ is not a wqo (if $|\Sigma|>1$) since it contains infinite
antichains: in the infinite sequence $b,ab,a^{2}b,a^{3}b,...a^{n}b,...$, we
have $a^{i}b\not\preceq a^{j}b$ for all $i<j$ and $i,j\in{\rm Nature}$.

In general, for a qo, upward-closed sets do not necessarily have a _finite_
basis. However, from [Hig52], we know that every upward-closed set in a wqo
has a finite basis.

We have the following equivalent characterization of wqos.

######  Proposition 1 ([ER56, SS12]).

The following are equivalent, given a qo $(X,\leq)$:

  1. (1)

$(X,\leq)$ is a wqo.

  2. (2)

Every infinite sequence in $X$ has an infinite increasing subsequence with
respect to $leq$.

  3. (3)

Every upward-closed non-empty subset in $X$ has a finite basis.

  4. (4)

$(X,\leq)$ is well-founded and contains no infinite antichain.

On the other hand, downward-closed subsets of qos enjoy the following
property:

######  Proposition 2 ([ER56]).

A qo $(X,\leq)$ contains no infinite antichain iff every downward-closed set
decomposes into a finite union of ideals.

The above proposition is useful to design the forward coverability algorithm
that will be described in Section 2.2.

Next, we introduce transition systems:

Transition systems. A _transition system_ is a pair
$\mathcal{S}=(X,\xrightarrow{})$ where $X$ is the set of states and
${\xrightarrow{}}\subseteq X\times X$ is the transition relation. We write
$x\xrightarrow{}{}y$ for $(x,y)\in{\xrightarrow{}}$. Moreover, we let
$\xrightarrow{*}$ be the transitive and reflexive closure of the relation
$\xrightarrow{}$, and $\xrightarrow{+}$ be the transitive closure of
$\xrightarrow{}$.

Given a state $x\in X$, we write $\textsf{Post}_{\mathcal{S}}(x)=\\{y\in X\mid
x\xrightarrow{}{}y\\}$ for the set of immediate successors of $x$. Similarly,
$\textsf{Pre}_{\mathcal{S}}(x)=\\{y\in X\mid y\xrightarrow{}{}x\\}$ denotes
the set of its immediate predecessors.

We call $\mathcal{S}$ _finitely branching_ if, for all $x\in X$, the set
$\textsf{Post}_{\mathcal{S}}(x)$ is finite. The _reachability set_ of
$\mathcal{S}$ from $x\in X$ is defined as
$\textsf{Post}_{\mathcal{S}}^{*}(x)=\\{y\in X\mid x\xrightarrow{*}y\\}$. Note
that, when $\mathcal{S}$ is clear from the context, we may drop the subscript
and write, e.g., $\textsf{Post}^{*}(x)$. We say that a state $y$ is reachable
from $x$ if $y\in\textsf{Post}^{*}(x)$.

We recall that the _reachability tree_ from an initial state $x_{0}$ in
$\mathcal{S}$ is a tree with a root node labelled by $x_{0}$. Then, for all
$y$ such that $x_{0}\xrightarrow{}y$, we add a vertex labelled with $y$ and
add an edge from the root node to the node labelled with $y$. We then compute
$\textsf{Post}(y)$ and once again add vertices labelled with each state in
$\textsf{Post}(y)$. We repeat this for every vertex along the tree. Note that
we can have multiple vertices labelled with the same state, and moreover, the
reachability tree can be infinite even if the reachability set from the
initial state is not.

A _(well-)ordered transition system_ is a triple
$\mathcal{S}=(X,\xrightarrow{},\leq)$ consisting of a transition system
$(X,\xrightarrow{})$ equipped with a qo (resp., wqo) $(X,\leq)$. An ordered
transition system $\mathcal{S}=(X,\xrightarrow{},\leq)$ is _effective_ if
$\leq$ and $\xrightarrow{}$ are decidable. We say that a state $y$ is
_coverable_ from $x$ if $y\in\mathord{\downarrow}\textsf{Post}^{*}(x)$.

[[Fin90]] A _well-structured transition system (WSTS)_ is a well-ordered
transition system $\mathcal{S}=(X,\xrightarrow{},\leq)$ that satisfies
(general) _monotony_ : for all $x,y,x^{\prime}\in X$, we have: $x\leq y\land
x\xrightarrow{}x^{\prime}\implies\exists y^{\prime}\in X\textup{:
}x^{\prime}\leq y^{\prime}\land y\xrightarrow{*}y^{\prime}.$

We define other types of monotony. We say that a well-ordered transition
system $\mathcal{S}=(X,\xrightarrow{},\leq)$ satisfies _strong monotony_
(resp., _transitive monotony_) if, for all $x,y,x^{\prime}\in X$ such that
$x\leq y$ and $x\xrightarrow{}x^{\prime}$, there is $y^{\prime}\in X$ such
that $x^{\prime}\leq y^{\prime}$ and $y\xrightarrow{}y^{\prime}$ (resp.,
$y\xrightarrow{+}y^{\prime}$). The transition system $\mathcal{S}$ satisfies
_strict monotony_ if, for all $x,y,x^{\prime}\in X$ such that $x<y$ and
$x\xrightarrow{}x^{\prime}$, there is $y^{\prime}\in X$ such that
$x^{\prime}<y^{\prime}$ and $y\xrightarrow{}y^{\prime}$.

###  2.2. Decision problems for transition systems.

We recall the following well-known decision problems.

Given an ordered transition system $\mathcal{S}=(X,\xrightarrow{},\leq)$ and
an initial state $x_{0}\in X$:

  * •

_The non-termination problem_ : Is there an infinite sequence of states
$x_{1},x_{2},\ldots$ such that
$x_{0}\xrightarrow{}x_{1}\xrightarrow{}x_{2}\xrightarrow{}\ldots$ ?

  * •

_The boundedness problem_ : Is $\textsf{Post}^{*}_{\mathcal{S}}(x_{0})$
finite?

  * •

_The coverability problem_ : Given a state $y\in X$, is $y$ coverable from
$x_{0}$?

It is folklore [Fin90, FS01] that non-termination is decidable for finitely
branching WSTS with transitive monotony and that boundedness is decidable for
finitely branching WSTS $\mathcal{S}=(X,\xrightarrow{},\leq)$ where $\leq$ is
a partial ordering and $\xrightarrow{}$ is strictly monotone. In both cases,
we suppose that the WSTS are effective and that $\textsf{Post}(x)$ is
computable, for all $x\in X$.

Coverability problem.We recall that coverability is decidable for a large
class of WSTS:

######  Theorem 3 ([FS01, ACJT00]).

The coverability problem is decidable for effective WSTS
$\mathcal{S}=(X,\xrightarrow{},\leq)$ equipped with an algorithm that, for all
finite subsets $I\subseteq X$, computes a finite basis $\textsf{pb}(I)$ of
$\mathord{\uparrow}\textsf{Pre}(\mathord{\uparrow}I)$.

Assume $\mathcal{S}=(X,\xrightarrow{},\leq)$ is a WSTS and $x\in X$ is a
state. The _backward coverability algorithm_ involves computing (a finite
basis of) $\textsf{Pre}^{*}(\mathord{\uparrow}x)$ as the limit of the infinite
increasing sequence
$\mathord{\uparrow}I_{0}\subseteq\mathord{\uparrow}I_{1}\subseteq\ldots$ where
$I_{0}=\\{x\\}$ and
$I_{n+1}\stackrel{{\scriptstyle\scriptscriptstyle\text{def}}}{{=}}I_{n}\cup\textsf{pb}(I_{n})$.
Since there exists an integer $k$ such that
$\mathord{\uparrow}I_{k+1}=\mathord{\uparrow}I_{k}$, the finite set $I_{k}$ is
computable (one may test, for all $n$, whether
$\mathord{\uparrow}I_{n+1}=\mathord{\uparrow}I_{n}$) and $I_{k}$ is then a
finite basis of $\textsf{Pre}^{*}(\mathord{\uparrow}x)$ so one deduces that
coverability is decidable.

Coverability can be also decided by using the _forward coverability algorithm_
that relies on two semi-decision procedures (as described below). It relies on
Proposition 2, and enumerates finite unions of ideals composing inductive
invariants. It shows that the “no infinite antichain” property is sufficient
to decide coverability, hence the wqo hypothesis is not necessary. It applies
to the class of _well behaved transition systems_ , which are more general
than WSTS. A well behaved transition system (WBTS) is an ordered transition
system $\mathcal{S}=(X,\xrightarrow{},\leq)$ with monotony such that
$(X,\leq)$ contains no infinite antichain. We describe effectiveness
hypotheses that allow manipulating downward-closed sets in WBTS.

[[BFM17]] A class $C$ of WBTS is _ideally effective_ if, given
$\mathcal{S}=(X,\xrightarrow{}{},\leq)\in C$,

  * •

the set of encodings of $\textsf{Ideals}(X)$ is recursive,

  * •

the function mapping the encoding of a state $x\in X$ to the encoding of the
ideal $\mathord{\downarrow}{x}\in\textsf{Ideals}(X)$ is computable;

  * •

inclusion of ideals of $X$ is decidable;

  * •

the downward closure $\mathord{\downarrow}{\textsf{Post}(I)}$ expressed as a
finite union of ideals is computable from the ideal $I\in\textsf{Ideals}(X)$.

######  Theorem 4 ([BFM17]).

The coverability problem is decidable for ideally effective WBTS.

The result is derived from the design of two semi-decision procedures where
downward-closed sets are represented by their finite decomposition in ideals
and this is effective. Procedure 1 checks for coverability of $y$ from
$x_{0}$, by recursively computing $\mathord{\downarrow}x_{0}$,
$\mathord{\downarrow}(\mathord{\downarrow}x_{0}\cup\textsf{Post}(\mathord{\downarrow}x_{0}))$
and so on. This procedure terminates only if $y$ belongs to one of these sets,
hence it terminates if $y$ is coverable.

Procedure 1 : Checks for coverability

input: $\mathcal{S}=(X,\xrightarrow{},\leq)$ and $x_{0},y$

$D:=\mathord{\downarrow}x_{0}$

while $y\notin D$ do

$D:=\mathord{\downarrow}(D\cup\textsf{Post}_{\mathcal{S}}(D))$

end while

return “$y$ is coverable from $x_{0}$”

Hence, we deduce:

######  Proposition 5 ([BFM17]).

For an ideally effective WBTS $\mathcal{S}=(X,\xrightarrow{},\leq)$, an
initial state $x_{0}$, and a state $y$, Procedure 1 terminates iff $y$ is
coverable from $x_{0}$.

Procedure 2 enumerates all downward-closed subsets (by means of their finite
decomposition in ideals) in some fixed order $D_{1},D_{2},\ldots$ We remark
that this enumeration is effective since $\mathcal{S}$ is ideally effective.
Furthermore, it checks for all $i$, $D_{i}\subseteq X$ and
$\mathord{\downarrow}\textsf{Post}(D_{i})\subseteq D_{i}$, and if such a set
$D_{i}$ contains $x_{0}$ but not $y$. If it does contain $x_{0}$, it is an
over-approximation of $\textsf{Post}^{*}(x_{0})$. Hence, if there is such a
set $D_{i}$ with $x_{0}\in D_{i}$ but $y\notin D_{i}$, it is a certificate of
non-coverability. Moreover, this procedure terminates if $y$ is non-coverable
because $\mathord{\downarrow}\textsf{Post}^{*}(x_{0})$ is such a set, and
hence, will eventually be found.

Procedure 2 : Checks for non-coverability

input: $\mathcal{S}=(X,\xrightarrow{},\leq)$ and $x_{0},y$

$\textbf{enumerate}\text{ downward-closed sets }D_{1},D_{2},\ldots$

$i:=1$

while $\neg(\mathord{\downarrow}\textsf{Post}(D_{i})\subseteq D_{i}\text{
}\and\text{ }x_{0}\in D_{i}\text{ }\and\text{ }y\notin D_{i})$ do

$i:=i+1$

end while

return false

Therefore, we have:

######  Proposition 6 ([BFM17]).

For a WBTS $\mathcal{S}=(X,\xrightarrow{},\leq)$, an initial state $x_{0}$ and
a state $y$, Procedure 2 terminates iff $y$ is not coverable from $x_{0}$.

###  2.3. Labelled transition systems

Next, we define labelled transition systems, which are transition systems
where the transitions are equipped with labels.

A _labelled transition system (LTS)_ is a tuple
$\mathcal{S}={(X,\Sigma,\xrightarrow{},x_{0})}$ where $X$ is the set of
states, $\Sigma$ is the finite action alphabet,
${\xrightarrow{}}\subseteq{X\times\Sigma\times X}$ is the transition relation,
and $x_{0}\in X$ is the initial state.

A _quasi-ordered labelled transition system (OLTS)_ is defined as a tuple
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ where
$(X,\Sigma,\xrightarrow{},x_{0})$ is an LTS and $(X,\leq)$ is a qo.

In the case of an LTS or OLTS, we write $x\xrightarrow{a}x^{\prime}$ instead
of $(x,a,x^{\prime})\in{\to}$. For $\sigma\in\Sigma^{\ast}$,
$x\xrightarrow{\sigma}x^{\prime}$ is defined as expected. We also let
$x\xrightarrow{}x^{\prime}$ if $(x,a,x^{\prime})\in{\to}$ for some
$a\in\Sigma$, with closures $\xrightarrow{*}$ and $\xrightarrow{+}$. We let
$\textsf{Traces}(\mathcal{S})=\\{w\in\Sigma\mid x_{0}\xrightarrow{w}x\text{
for some }x\in X\\}$ be the set of traces.

We call an OLTS $\mathcal{S}$ _effective_ if $\leq$ and, for all $a\in\Sigma$,
$\xrightarrow{a}$ are decidable.

######  Remark 7.

We can similarly define a labelled WSTS as an OLTS such that the ordering is
well and it satisfies the general monotony condition (canonically adapted to
take care of the transition labels). Moreover, we lift the decision problems
from Definition 2.2 to OLTS in the obvious way.

###  2.4. Classes of labelled transition systems

In this paper, we mainly study subclasses of two well-known classes of
transition systems, namely counter machines, and FIFO machines. Both these
classes are known to simulate Turing machines, and hence, have undecidable
boundedness and non-termination.

Counter machines. Counter machines, also known as Minsky machines, are finite-
state machines that manipulate counters, which are variables that store non-
negative integers. Transitions of a counter machine, besides changing control-
states, perform a specified operation on a counter: increment by one,
decrement by one, along with a set of counters to be tested for zero. We
define formally a counter machine below.

A _counter machine_ (with zero tests) is a tuple $\mathcal{C}=(Q,V,T,q_{0})$.
Here, $Q$ is the finite set of _control-states_ and $q_{0}\in Q$ is the
_initial control-state_. Moreover, $V$ is a finite set of _counters_ and
$T\subseteq Q\times\textsf{Act}_{\mathcal{C}}\times Q$ is the transition
relation where
$\textsf{Act}_{\mathcal{C}}=\\{\textsf{inc}(v),\textsf{dec}(v),\textsf{noop}\mid
v\in V\\}\times 2^{V}$ (an element of $2^{V}$ will indicate the set of
counters to be tested to $0$).

The counter machine $\mathcal{C}$ induces an LTS
$\mathcal{S}_{\mathcal{C}}=(X_{\mathcal{C}},\textsf{Act}_{\mathcal{C}},\xrightarrow{}_{\mathcal{C}},x_{0})$
with set of states $X_{\mathcal{C}}=Q\times\mathbb{N}^{V}$. In $(q,\ell)\in
X_{\mathcal{C}}$, the first component $q$ is the current control-state and
$\ell=(\ell_{v})_{v\in V}$ represents the counter values. The initial state is
then $x_{0}=(q_{0},\ell_{0})$ with $\ell_{0}=(0,0,\ldots,0)$. For
$op\in\\{\mathsf{inc},\mathsf{dec}\\}$, $v\in V$, and $Z\subseteq V$ ($Z$ is
the set of counters tested for zero), there is a transition
$(q,\ell)\xrightarrow{op(v),Z}_{\mathcal{C}}(q^{\prime},m)$ if
$(q,(op(v),Z),q^{\prime})\in T$, $\ell_{v^{\prime}}=0$ for all $v^{\prime}\in
Z$, $m_{v}=\ell_{v}+1$ if $op=\mathsf{inc}$ and $m_{v}=\ell_{v}-1$ if
$op=\mathsf{dec}$, and $m_{v^{\prime}}=\ell_{v^{\prime}}$ for all
$v^{\prime}\in V\setminus\\{v\\}$.

For $op=\textsf{noop}$, and $Z\subseteq V$, there is a transition
$(q,\ell)\xrightarrow{op,Z}_{\mathcal{C}}(q^{\prime},m)$ if
$(q,(op,Z),q^{\prime})\in T$, $\ell_{v^{\prime}}=0$ for all $v^{\prime}\in Z$
(applies the zero tests), and $m_{v}=\ell_{v}$ for all $v\in V$. We sometimes
omit writing noop and label the transition with only the set of counters to be
tested to zero, or we write $\textsf{zero}(Z)$. Similarly, we omit $Z$ if
$Z=\emptyset$.

FIFO machines. Next, we study FIFO machines. FIFO machines can be viewed as a
finite state machine equipped with one or more (potentially unbounded)
channels, where messages can be sent to and received from. [BZ83] showed that
general FIFO machines can simulate Turing machines, and hence, it is
undecidable to verify boundedness. However, it is still a widely used model to
represent asynchronously communicating systems.

A FIFO machine $\mathcal{M}$ over the set of channels Ch is a tuple
$\mathcal{M}=(Q,A,T,q_{0})$ where $Q$ is a finite set of control-states, $A$
is the finite message alphabet, and $q_{0}\in Q$ is an initial control-state.
Moreover, $T\subseteq Q\times\textsf{Ch}\times\\{!,?\\}\times A\times Q$ is
the transition relation, where $\textsf{Ch}\times\\{!\\}\times A$ and
$\textsf{Ch}\times\\{?\\}\times A$ are the set of send and receive actions,
respectively.

The FIFO machine $\mathcal{M}$ induces the LTS
$\mathcal{S}_{\mathcal{M}}=(X_{\mathcal{M}},\Sigma_{\mathcal{M}},\xrightarrow{}_{\mathcal{M}},x_{0})$.
Its set of states is $X_{\mathcal{M}}=Q\times(A^{*})^{\textsf{Ch}}$. In
$(q,\mathbf{w})\in X_{\mathcal{M}}$, the first component $q$ denotes the
current control-state, and
$\mathbf{w}=(\mathbf{w}_{\textsf{c}})_{\textsf{c}\in\textsf{Ch}}$ denotes the
contents $\mathbf{w}_{c}\in A^{*}$ for every channel
$\textsf{c}\in\textsf{Ch}$. The initial state is
$x_{0}=(q_{0},\mathbf{\varepsilon})$, where $\mathbf{\varepsilon}$ denotes
that every channel is empty. Moreover,
$\Sigma_{\mathcal{M}}=\textsf{Ch}\times\\{!,?\\}\times A$. The transitions are
given as follows:

  * •

$(q,\mathbf{w})\xrightarrow{\textsf{c}!a}_{\mathcal{M}}(q^{\prime},\mathbf{w^{\prime}})$
if $(q,\textsf{c}!a,q^{\prime})\in T$,
$\mathbf{w^{\prime}}_{\textsf{c}}=\mathbf{w}_{\textsf{c}}\cdot a$, and
$\mathbf{w^{\prime}}_{\textsf{d}}=\mathbf{w}_{\textsf{d}}$ for all
$\textsf{d}\in\textsf{Ch}\setminus\\{\textsf{c}\\}$.

  * •

$(q,w)\xrightarrow{\textsf{c}?a}_{\mathcal{M}}(q^{\prime},w^{\prime})$ if
$(q,\textsf{c}?a,q^{\prime})\in T$,
$\mathbf{w}_{\textsf{c}}=a\cdot\mathbf{w^{\prime}}_{\textsf{c}}$, and
$\mathbf{w^{\prime}}_{\textsf{d}}=\mathbf{w}_{\textsf{d}}$ for all
$\textsf{d}\in\textsf{Ch}\setminus\\{\textsf{c}\\}$.

The index $\mathcal{M}$ may be omitted whenever $\mathcal{M}$ is clear from
the context. When there is no ambiguity, we confuse machines and their
associated LTS.

Note that, in general, FIFO machines with a single channel are as powerful as
FIFO machines with multiple channels. When we denote FIFO machines with a
single channel, we omit specifying the set Ch, and hence, we denote the set of
labels as $\Sigma_{\mathcal{M}}=\\{!,?\\}\times A$.

For FIFO machines, we define the extended prefix ordering, denoted by
$\leq_{p}$ as follows:
$(q,\mathbf{w})\leq_{p}(q^{\prime},\mathbf{w^{\prime}})$ if $q=q^{\prime}$ and
for all $\textsf{c}\in\textsf{Ch}$, $\mathbf{w}_{\textsf{c}}$ is a prefix of
$\mathbf{w^{\prime}}_{\textsf{c}}$, i.e.,
$\mathbf{w}_{\textsf{c}}\preceq\mathbf{w^{\prime}}_{\textsf{c}}$.

##  3\. Branch-well-structured transition systems

In this section, we generalize wqo and monotony such that these properties
only consider states along a branch in the reachability tree. To define these
notions, we use labels on the transitions, hence, we consider labelled
transition systems.

###  3.1. Branch-wqo

Consider an OLTS $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$. A _run_
(or _branch_) of $\mathcal{S}$ is a finite or infinite sequence
$\rho=(x_{0}\xrightarrow{}x_{1})(x_{1}\xrightarrow{}x_{2})...$ simply written
$\rho=x_{0}\xrightarrow{}x_{1}\xrightarrow{}x_{2}\ldots$. We say that $\rho$
is _branch-wqo_ if the set of states $\\{x_{0},x_{1},x_{2},\ldots\\}$ visited
along $\rho$ is wqo w.r.t. $\leq$.

A _run_ (or _branch_) of $\mathcal{S}$ is a finite or infinite sequence
$\rho=(x_{0}\xrightarrow{}x_{1})(x_{1}\xrightarrow{}x_{2})...$ simply written
$\rho=x_{0}\xrightarrow{}x_{1}\xrightarrow{}x_{2}\ldots$. We denote the set of
states visited along $\rho$ as $X_{\rho}=\\{x_{0},x_{1},x_{2},\ldots\\}$. We
say that $\rho$ is _branch-wqo_ if $X_{\rho}$ is wqo w.r.t. $\leq$.

An OLTS $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ is _branch-wqo_ if
every run of $\mathcal{S}$ is branch-wqo.

Consider the FIFO machine $\mathcal{M}_{1}$ in Figure 1 with one FIFO channel.
In control-state $q_{0}$, it loops by sending letter $a$ to the channel. Then,
we may go, non-deterministically, to control-state $q_{1}$ by sending letter
$b$ once, and then we stop. Let us consider the set of states
$X_{1}=\\{q_{0},q_{1}\\}\times\\{a,b\\}^{*}$ together with the extended prefix
ordering $\leq_{p}$, i.e. $(q,u)\leq_{p}(q^{\prime},u^{\prime})$ if
$q=q^{\prime}$ and $u\preceq u^{\prime}$. The reachability set of
$\mathcal{M}_{1}$ from $(q_{0},\varepsilon)$ is equal to
$\textsf{Post}^{*}(q_{0},\varepsilon)=\\{(q_{0},w)\mid w\in
a^{*}\\}\cup\\{(q_{1},w^{\prime})\mid w^{\prime}\in a^{*}b\\}$. Note that
$\leq_{p}$ is not a wqo since elements of the set $\\{(q_{1},w^{\prime})\mid
w^{\prime}\in a^{*}b\\}$ form an infinite antichain for $\leq_{p}$. However,
the reachability tree of $\mathcal{M}_{1}$ is branch-wqo for the initial state
$(q_{0},\varepsilon)$ (every branch is either finite or branch-wqo). Hence,
there exist branch-wqo OLTS $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$
such that $(X,\leq)$ is not a wqo.

$q_{0}$$q_{1}$$!a$$!b$

$(q_{0},\varepsilon)$$(q_{1},b)$$(q_{0},a)$$(q_{0},aa)$$(q_{1},ab)$$...$$(q_{1},aab)$

Figure 1. The FIFO machine $\mathcal{M}_{1}$ (left) with initial state
$(q_{0},\varepsilon)$, and its corresponding (incomplete) infinite
reachability tree (right). We see that the induced transition system is
branch-wqo.

However, unlike wqo, the notion of branch-wqo depends on the initial state
considered. We will see below that there exists a system
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ and $x_{0}^{\prime}\in X$
such that $\mathcal{S}$ is branch-wqo but
$(X,\Sigma,\xrightarrow{},\leq,x_{0}^{\prime})$ is not branch-wqo.

$q_{0}$$q_{1}$$q_{2}$$!a$$!b$$?c$$!b$$?b$$?c$$!c$

$(q_{2},\varepsilon)$$(q_{2},c)$$(q_{2},cc)$$(q_{1},cb)$$...$$(q_{1},ccb)$$(q_{1},b)$$(q_{2},b)$$...$$...$$...$$...$$(q_{2},\varepsilon)$$(q_{2},c)$$(q_{2},cc)$$(q_{1},ccb)$$...$$...$$...$$...$$...$

Figure 2. The FIFO machine $\mathcal{M}_{2}$ (left) and the incomplete
reachability tree from $(q_{2},\varepsilon)$ (right).

Consider the FIFO machine $\mathcal{M}_{2}$ in Figure 2 with one FIFO channel.
If we start from $(q_{0},\varepsilon)$, it behaves exactly as the FIFO machine
$\mathcal{M}_{1}$. However, if we change the initial state to
$(q_{2},\varepsilon)$, then it could either loop by sending $c$, or non-
deterministically send a $b$ and go to control-state $q_{1}$. Then, if at
least one $c$ has been sent, it can either loop again receiving the letters
$c$, or once again non-deterministically come back to $q_{2}$ upon receiving
$c$.

There exists an infinite run $\rho$ with the prefix:
$(q_{2},\varepsilon)\xrightarrow{!c}(q_{2},c)\xrightarrow{!b}(q_{1},cb)\xrightarrow{?c}(q_{2},b)\xrightarrow{?b}(q_{2},\varepsilon)\xrightarrow{!c.!c.!b}(q_{1},ccb)\xrightarrow{}...$
such that all the elements of the infinite set
$B=\\{{(q_{1},cb)},{(q_{1},ccb)},\allowbreak\ldots,\allowbreak{(q_{1},c^{n}b)},\ldots\\}$
are visited along $\rho$, i.e $B\subseteq X_{\rho}$. Hence, we have an
infinite sequence of incomparable elements along $\rho$, i.e. $X_{\rho}$ is
not wqo, and therefore, the system is not branch-wqo.

We now show that branch-wqos enjoy some of the good properties of wqos. Let
$\mathcal{S}_{1}=(X_{1},\Sigma,\xrightarrow{}_{1},\leq_{1},x_{0,1})$ and
$\mathcal{S}_{2}=(X_{2},\Sigma,\xrightarrow{}_{2},\leq_{2},x_{0,2})$ be two
branch-wqos. We consider their product to be
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$, where $X=X_{1}\times
X_{2}$, and
$((x_{1},x_{2}),a,(x^{\prime}_{1},x^{\prime}_{2}))\in\xrightarrow{}$ if
$(x_{1},a,x^{\prime}_{1})\in\xrightarrow{}_{1}$ and
$(x_{2},a,x^{\prime}_{2})\in\xrightarrow{}_{2}$. Moreover, we consider the
ordering to be component-wise, i.e. we have
$(x_{1},x_{2})\leq(x^{\prime}_{1},x^{\prime}_{2})$ if
$x_{1}\leq_{1}x^{\prime}_{1}$ and $x_{2}\leq_{2}x^{\prime}_{2}$; finally
$x_{0}=(x_{0,1},x_{0,2})$.

######  Proposition 8.

The product of finitely many branch-wqos is branch-wqo.

######  Proof 3.1.

We show this for two branch-wqos, but this proof can be extended to finitely
many branch-wqos.

Let us consider an infinite run $\rho$ in the product branch-wqo
$\mathcal{S}$. If we consider the set $X_{\rho}$ along with the order
$\leq_{1}$, we can extract an infinite subsequence $B=(x_{n},y_{n})_{n\in{\rm
Nature}}\subseteq X_{\rho}$ such that $(x_{n})_{n\in{\rm Nature}}$ forms an
increasing sequence wrt. $\leq_{1}$ (since $(X_{1},\leq_{1})$ is branch-wqo).
Now, within this subsequence $B$, there exists an increasing subsequence
$(y_{n_{m}})_{m\in{\rm Nature}}$ (since the branch is also wqo wrt.
$\leq_{2}$). Hence, we have an infinitely long sequence
$(x_{n_{m_{k}}},y_{n_{m_{k}}})_{k\in{\rm Nature}}$.

We can similarly prove that the same holds true for disjoint unions and
intersection of branch-wqos.

###  3.2. Branch-monotony

Now that we have relaxed the notion of branch-wqo, we shall look at a
generalization of strong monotony, which we will refer to as branch-monotony.

An OLTS $\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$ is _branch-
monotone_ if, for all $x,x^{\prime}\in X$, $\sigma\in\Sigma^{*}$ such that
$x\xrightarrow{\sigma}x^{\prime}$ and $x\leq x^{\prime}$, there exists a state
$y$ such that $x^{\prime}\xrightarrow{\sigma}y$ and $x^{\prime}\leq y$.

######  Proposition 9.

Let $\mathcal{S}$ be a branch-monotone OLTS and let there be states
$x,x^{\prime}$ such that $x\xrightarrow{\sigma}x^{\prime}$ and $x\leq
x^{\prime}$, with $\sigma\in\Sigma^{*}$. Then, for any $n\geq 1$, there exists
$y_{n}\in X$ such that $x\xrightarrow{\sigma^{n}}y_{n}$ with $x\leq y_{n}$.

######  Proof 3.2.

We prove this by induction on $n$. Base case: Let $n=1$. From the hypothesis,
we immediately have a run $x\xrightarrow{\sigma}x^{\prime}$ such that $x\leq
x^{\prime}$. Hence, the property holds trivially for the base case, with
$y_{1}=x^{\prime}$.

Let us assume that it holds for $n$. We will now show that it also holds for
$n+1$. Let $x\xrightarrow{\sigma}x^{\prime}$ be a finite run satisfying $x\leq
x^{\prime}$. Furthermore, from the induction hypothesis, there exists a state
$y_{n}$ such that
$x\xrightarrow{\sigma}x^{\prime}\xrightarrow{\sigma^{n-1}}y_{n}$ such that
$x\leq y_{n}$. Moreover, by the definition of branch-monotony, there exists a
state $y$ such that $x^{\prime}\xrightarrow{\sigma}y$ and $x^{\prime}\leq y$.
Furthermore, if we consider the run $x^{\prime}\xrightarrow{\sigma}y$, again
by induction hypothesis, there exists a state $y^{\prime}_{n}$ such that
$x^{\prime}\xrightarrow{\sigma^{n}}y^{\prime}_{n}$ and $x\leq y^{\prime}_{n}$.
Hence, there exists a run
$x\xrightarrow{\sigma}x^{\prime}\xrightarrow{\sigma^{n}}y^{\prime}_{n}$, and
$x\leq x^{\prime}\leq y^{\prime}_{n}$, so by transitivity, $x\leq
y^{\prime}_{n}$. In other words, we have
$x\xrightarrow{\sigma^{n+1}}y^{\prime}_{n}=y_{n+1}$, and this completes our
proof.

As in the case of general monotony, _strict_ branch-monotony is defined using
strict inequalities in both cases.

Consider $\mathcal{M}_{1}$ from Figure 1 once again. Note $\mathcal{M}_{1}$
induces an OLTS by considering the actions on the edges to be the labels.
Moreover, $\mathcal{M}_{1}$ is branch-monotone. For every
$x\xrightarrow{\sigma}x^{\prime}$ such that $x\leq_{p}x^{\prime}$ and
$\sigma\in\Sigma^{*}$, the only case is that $x=(q_{0},a^{n})$,
$x^{\prime}=(q_{0},a^{n+k})$, for some $n,k\in\mathbb{N}$. Moreover,
$\sigma\in(!a)^{*}$. Hence, we can always repeat $\sigma$ from $x^{\prime}$
such that $x^{\prime}\xrightarrow{\sigma}y=(q_{0},a^{n+k+k})$. Therefore,
$x^{\prime}\leq_{p}y$. We deduce that $\mathcal{M}_{1}$ is branch-monotone.

###  3.3. Branch-WSTS

We are now ready to extend the definition of WSTS.

A _branch-WSTS_ is an OLTS $\mathcal{S}=(X,\Sigma,$
$\xrightarrow{},\leq,x_{0})$ that is finitely branching, branch-monotone, and
branch-wqo.

When we say, without ambiguity, that a machine $\mathcal{M}$ is branch-wqo,
WSTS, or branch-WSTS, we mean that the ordered transition system
$\mathcal{S}_{\mathcal{M}}$, induced by machine $\mathcal{M}$, is branch-wqo,
WSTS, or branch-WSTS, respectively. We will explicitly define the transition
system induced by FIFO machines in Section 4.2.

######  Remark 10.

Branch-WSTS is a strict superclass of labelled WSTS. For example, machine
$\mathcal{M}_{1}$ (seen in Figure 1) with initial state $(q_{0},\varepsilon)$
is branch-WSTS for the ordering $\leq_{p}$ but it is not WSTS for $\leq_{p}$
since $\leq_{p}$ is not a wqo on $\\{q_{0},q_{1}\\}\times\\{a,b\\}^{*}$ or on
the subset $\\{(q_{1},w)\mid w\in a^{*}b\\}$.

Let us recall the _Reduced Reachability Tree ( $\mathit{RRT}$)_, which was
defined as Finite Reachability Tree in [Fin90, FS01]. Suppose that
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ is an OLTS. Then, the
_Reduced Reachability Tree_ from $x_{0}$, denoted by
$\mathit{RRT}(\mathcal{S},x_{0})$, is a tree with root $n_{0}$ labelled
$x_{0}$ that is defined and built as follows. For every
$x\in\textsf{Post}(x_{0})$, we add a child vertex labelled $x$ to $n_{0}$. The
tree is then built in the following way. We pick an unmarked vertex $c$ which
is labelled with $x$:

  * •

if $n$ has an ancestor $n^{\prime}$ labelled with $x^{\prime}$ such that
$x^{\prime}\leq x$, we mark the vertex $n$ as _dead_ , and say $n^{\prime}$
_subsumes_ $n$.

  * •

otherwise, we mark $n$ as _live_ , and for every $y\in\textsf{Post}(x)$, we
add a child labelled $y$ to $n$.

$(q_{0},\varepsilon)$$(q_{1},b)$$(q_{0},a)$dead Figure 3. The Reduced
Reachability Tree of $\mathcal{M}_{1}$ from $(q_{0},\varepsilon)$. Note that
$(q_{0},a)$ is dead because it is subsumed by state $(q_{0},\varepsilon)$. As
a matter of fact, we have $(q_{0},\varepsilon)\xrightarrow{*}(q_{0},a)$ and
$(q_{0},\varepsilon)\leq_{p}(q_{0},a)$. State $(q_{1},b)$ is also dead but it
is not subsumed.

propfinite Let $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ be an OLTS
that is finitely branching and branch-wqo. Then,
$\mathit{RRT}(\mathcal{S},x_{0})$ is finite.

######  Proof 3.3.

Let us assume to the contrary that $\mathit{RRT}(\mathcal{S},x_{0})$ is
infinite. Since $\mathcal{S}$ is finitely branching and branch-wqo, there is
an infinite branch in the reachability tree. Since this branch is branch-wqo,
there exists a pair of states, say $x_{2}$ and $x_{3}$ visited along the
branch, such that $x_{0}\xrightarrow{}{*}x_{1}\xrightarrow{+}x_{2}$ and
$x_{1}\leq x_{2}$. However, since the run is infinite, there exists $x_{3}$
such that $x_{2}\xrightarrow{+}x_{3}$. We can represent the beginning of this
branch with the finite prefix
$n_{0}(x_{0})\xrightarrow{*}n_{1}(x_{1})\xrightarrow{+}n_{2}(x_{2})\xrightarrow{+}n_{3}(x_{3})$,
in $\mathit{RRT}(\mathcal{S},x_{0})$, such that nodes $n_{1},n_{2},n_{3}$ are
all different. However, since $x_{1}\leq x_{2}$, the node $n_{2}(x_{2})$ has
been marked as dead, and the tree need not be explored further.Thus, there is
a contradiction. Hence, $\mathit{RRT}(\mathcal{S},x_{0})$ is finite.

propboundedFRT Let $\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$ be a
branch-WSTS, equipped with strict branch-monotony and such that $\leq$ is a
partial ordering. The reachability set
$\textsf{Post}^{*}_{\mathcal{S}}(x_{0})$ is infinite iff there exists a branch
$n_{0}(x_{0})\xrightarrow{*}n_{1}(x_{1})\xrightarrow{+}n_{2}(x_{2})$ in
$\mathit{RRT}(\mathcal{S},x_{0})$ such that $x_{1}<x_{2}$.

######  Proof 3.4.

The following proof is an adaptation of the proof of boundedness for WSTS in
[FS01] to branch-WSTS.

First, let us assume $\mathcal{S}$ is unbounded, i.e.
$\textsf{Post}_{\mathcal{S}}^{*}(x_{0})$ is infinite. We will show that there
exists a branch
$n_{0}(x_{0})\xrightarrow{*}n_{1}(x_{1})\xrightarrow{+}n_{2}(x_{2})$ in
$\mathit{RRT}(\mathcal{S},x_{0})$ such that $x_{1}<x_{2}$. Since $\mathcal{S}$
is unbounded, there are an infinite number of distinct states which are
reachable from $x_{0}$. We first show that there exists a run starting from
$x_{0}$, without any loop, i.e. where all states are distinct. We consider the
finitely branching tree of all prefixes of runs, and prune this tree by
removing prefixes which contain a loop. Because any reachable state can be
reached without a loop, the pruned tree still contains an infinite number of
prefixes. By König’s lemma, there exists an infinite run with no loop. Any run
starting from $x_{0}$ has a finite prefix labelling a maximal path in
$\mathit{RRT}(\mathcal{S},x_{0})$. Hence, there must be a node $n_{2}(x_{2})$
which is subsumed by a node $n_{1}(x_{1})$ such that $x_{1}\neq x_{2}$ (since
we enforce that all nodes are distinct). Since we assumed $\leq$ to be a
partial ordering, we deduce from $x_{1}\neq x_{2}$, and $x_{1}\leq x_{2}$ that
$x_{1}<x_{2}$.

Conversely, let us assume that there exist two vertices $n_{1},n_{2}$ labelled
by $x_{1}$ and $x_{2}$ respectively, in $\mathit{RRT}(\mathcal{S},x_{0})$ such
that $n_{0}(x_{0})\xrightarrow{*}n_{1}(x_{1})\xrightarrow{+}n_{2}(x_{2})$ in
$\mathit{RRT}(\mathcal{S},x_{0})$ such that $x_{1}<x_{2}$. Let
$x_{1}\xrightarrow{a_{1}a_{2}...a_{n}}x_{2}$ and $x_{1}<x_{2}$. Hence, there
exist $y_{1},y_{2},...,y_{n}\in X$ such that
$x_{1}\xrightarrow{a_{1}}y_{1}\xrightarrow{a_{2}}y_{2}\xrightarrow{a_{3}}...\xrightarrow{a_{n}}y_{n}=x_{2}$.
Since the system is strictly branch-monotone, we can repeat this sequence,
i.e., there exist $n$ states $u_{1},u_{2},...,u_{n}$ such that
$x_{2}\xrightarrow{a_{1}}u_{1}\xrightarrow{a_{2}}u_{2}...\xrightarrow{a_{n}}u_{n}=x_{3}$
with $y_{n}<u_{n}$. By iterating this process, we construct an infinite
sequence of states $(x_{k})_{k\geq 0}$ such that for all $k\geq 1$, one has
$x_{k}\xrightarrow{a_{1}a_{2}...a_{n}}x_{k+1}$ and $x_{k}<x_{k+1}$. Then, we
deduce that all $x_{k}$ are different. Hence,
$\textsf{Post}_{\mathcal{S}}^{*}(x_{0})$ is infinite, and $\mathcal{S}$ is
unbounded.

We now need a notion of effectivity adapted to branch-WSTS.

A branch-WSTS $\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$ is
_branch-effective_ if $\mathcal{S}$ is effective and
$\textsf{Post}_{\mathcal{S}}(x)$ is a (finite) computable set, for all $x\in
X$.

######  Theorem 11.

Boundedness is decidable for branch-effective branch-WSTS
$\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$ with strict branch-
monotony such that $\leq$ is a partial ordering.

######  Proof 3.5.

Suppose $\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$ satisfies the
above conditions. From Proposition 3, we obtain that
${\mathit{RRT}(\mathcal{S},x_{0})}$ is finite. By hypothesis, $\mathcal{S}$ is
finitely branching and branch-effective. In particular, for all $x$,
$\textsf{Post}_{\mathcal{S}}(x)$ is a finite computable set. As $\leq$ is
decidable, we deduce that $\mathit{RRT}(\mathcal{S},x_{0})$ is effectively
computable. From Proposition 3.3, we know that
$\textsf{Post}^{*}_{\mathcal{S}}(x_{0})$ is infinite iff there exists a finite
branch $n_{0}(x_{0})\xrightarrow{*}n_{1}(x_{1})\xrightarrow{+}n_{2}(x_{2})$
such that $x_{1}<x_{2}$. This last property can be decided on
$\mathit{RRT}(\mathcal{S},x_{0})$, and so the boundedness property can be
decided, too.

We also generalize the decidability of non-termination for WSTS [FS01] to
branch-WSTS.

proptermFRT A branch-WSTS $\mathcal{S}=(X,\Sigma,$
$\xrightarrow{},\leq,x_{0})$ does not terminate from state $x_{0}$ iff there
exists a subsumed node in $\mathit{RRT}(\mathcal{S},x_{0})$.

######  Theorem 12.

Non-termination is decidable for branch-effective branch-WSTS.

######  Proof 3.6.

Given a branch-WSTS $\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$, we
apply Proposition 3.5 so that it is sufficient to build
$\mathit{RRT}(\mathcal{S},x_{0})$ and check if there exists a subsumed node.
Since $\mathcal{S}$ is branch-effective, we can effectively construct
$\mathit{RRT}(\mathcal{S},x_{0})$ and verify the existence of a subsumed node.

Note that the non-termination and boundedness problems for the example machine
$\mathcal{M}_{1}$ in Figure 1 are, therefore, decidable. Since there exist
nodes $n_{0}(x_{0})$ and $n_{1}(x_{1})$ in the $\mathit{RRT}$ such that
$x_{0}=(q_{0},\varepsilon)$ and $x_{1}=(q_{0},a)$ such that $x_{0}<x_{1}$ and
$x_{0}\xrightarrow{+}x_{1}$, the machine $\mathcal{M}_{1}$ is unbounded.
Furthermore, since all unbounded machines are non-terminating,
$\mathcal{M}_{1}$ is non-terminating.

On the other hand, boundedness becomes undecidable if we relax the strict
monotony condition to general monotony (even when we strengthen the order to
be wqo). This is because boundedness is undecidable for Reset Petri nets
[DFS98]. Reset Petri nets are effective WSTS $\mathcal{S}=(X,\Sigma,$
$\xrightarrow{},\leq,x_{0})$, hence branch-effective WSTS, where $\leq$ is the
wqo on vectors of integers. Hence, we deduce:

######  Proposition 13.

Boundedness is undecidable for branch-effective branch-WSTS
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ where $\leq$ is a wqo.

##  4\. Classes of branch-WSTS

We now study some classes of systems, namely, counter machines and FIFO
machines. Counter machines are wqo for the extended natural ordering; however,
due to the presence of zero-tests, general monotony fails, and hence, they are
not WSTS. We look at a subclass of counter machines, called counter machines
with restricted zero tests (CMRZ), where zero tests are present, but their
behaviour is controlled.

In [BZ83], the authors showed that general FIFO machines can simulate Turing
machines, and hence, it is undecidable to verify boundedness. However, it is
still a widely used model to represent asynchronously communicating systems.
Moreover, they are neither wqos nor monotone for the prefix ordering.
Secondly, in this section, we show that a subclass of FIFO machines, namely
input-bounded FIFO machines, are branch-WSTS under the prefix ordering.

Finally, we study more general counter machines and FIFO machines, and show
that we can decide non-termination and boundedness for a large subclass using
ideas from branch-well-structured behaviours.

###  4.1. Counter machines with restricted zero tests

We define _counter machines with restricted zero tests (CMRZ)_ imposing the
following requirement: Once a counter has been tested for zero, it cannot be
incremented or decremented any more. Formally, we say that $\mathcal{C}$ is a
counter machine with restricted zero tests if for all transition sequences of
the form
$q_{0}\xrightarrow{op(v_{1}),Z_{1}}q_{1}\xrightarrow{op(v_{2}),Z_{2}}\ldots\xrightarrow{op(v_{n-1}),Z_{n-1}}q_{n-1}\xrightarrow{op(v_{n}),Z_{n}}q_{n}$,
for every two positions $1\leq i\leq j\leq n$, we have $v_{j}\not\in Z_{i}$.

In [BFS20], it was shown that non-termination and boundedness are decidable
for this class of systems by reducing them to the (decidable) reachability
problem. However, using the alternative approach of branch-WSTS, we can verify
that non-termination and boundedness are decidable for this class without
reducing these problems to reachability.

Given a CMRZ $\mathcal{C}=(Q,V,T,q_{0})$, we consider the associated
transition system
$\mathcal{S}_{\mathcal{C}}=(X_{\mathcal{C}},\textsf{Act}_{\mathcal{C}},\xrightarrow{}_{\mathcal{C}},x_{0})$.
From this system, we construct an OLTS over the extended ordering $\leq$ such
that $(q,\mathbf{v})\leq(q^{\prime},\mathbf{v}^{\prime})$ iff $q=q^{\prime}$
and $\mathbf{v}\leq\mathbf{v}^{\prime}$ (component-wise). Note that
$(X_{\mathcal{C}},\leq)$ is a wqo. Moreover, this ordering is a partial
ordering.

We now show that CMRZ are branch-monotone for $\leq$. We drop the subscript
while denoting $X_{\mathcal{C}}$ for the remainder of this section, as it is
clear from context.

######  Proposition 14.

CMRZ are branch-monotone and strictly branch-monotone for the extended
ordering $\leq$.

######  Proof 4.1.

Consider the OLTS $\mathcal{S}=(X,\textsf{Act},\xrightarrow{},\leq,x_{0})$
associated to a CMRZ with states $x,x^{\prime}\in X$ such that $x\leq
x^{\prime}$ (resp. $x<x^{\prime}$) and
$x_{0}\xrightarrow{*}x\xrightarrow{\sigma}x^{\prime}$. We need to show that
there exists a state $y$ such that $x^{\prime}\xrightarrow{\sigma}y$ and
$x^{\prime}\leq y$ (resp. $x^{\prime}<y$).

We first prove the following claim:

_Claim:_ For states $x,x^{\prime}\in X$ such that
$x_{0}\xrightarrow{*}x\xrightarrow{\sigma}x^{\prime}$ where $x\leq x^{\prime}$
(resp. $x<x^{\prime}$) and $|\sigma|=n$, the following property holds: For all
$\nu\preceq\sigma$, we have $z,z^{\prime}\in X$ such that
$x\xrightarrow{\nu}z$ and $x^{\prime}\xrightarrow{\nu}z^{\prime}$ and $z\leq
z^{\prime}$ (resp. $z<z^{\prime}$). We prove this claim by induction on the
length of $\nu$.

For the base case, $|\nu|=0$. We have from the hypothesis, $x\leq x^{\prime}$,
hence the claim is trivially true.

Let us assume that the claim holds for $|\nu|=k$. We show that it holds for
$|\nu|=k+1$. From the induction hypothesis, we know that for
$\nu=\nu^{\prime}\cdot a$ where $a\in\textsf{Act}$, there exists
$z_{1},z^{\prime}_{1}$ such that $x\xrightarrow{\nu^{\prime}}z_{1}$ and
$x^{\prime}\xrightarrow{\nu^{\prime}}z^{\prime}_{1}$ and $z_{1}\leq
z^{\prime}_{1}$. Since $x\xrightarrow{\sigma}x^{\prime}$, we know that there
exists $z_{2}\in X$ such that
$x\xrightarrow{\nu^{\prime}}z_{1}\xrightarrow{a}z_{2}$. We can now be in one
of the following cases:

  1. Case i:

If $a$ is of the form noop and $Z=\emptyset$, then we can trivially execute
$a$ from $z^{\prime}_{1}$ and reach $z_{2}^{\prime}$ such that $z_{2}\leq
z_{2}^{\prime}$ (resp. $z_{2}<z_{2}^{\prime}$).

  2. Case ii:

The action $a$ is of the form $\textsf{inc}(v)$ or $\textsf{dec}(v)$, and the
set of counters to be tested for zero $Z=\emptyset$, i.e.
$z_{1}\xrightarrow{a}z_{2}$ only increments/decrements one counter and leaves
the others unchanged (and no counters are tested to zero). Since $z_{1}\leq
z^{\prime}_{1}$ (resp. $z_{1}<z^{\prime}_{1}$), we know that
$z_{1},z^{\prime}_{1}$ have the same control-state. Hence, this action is
enabled in $z^{\prime}_{1}$. Moreover, because of the CMRZ property, we know
that $v$ is not tested to zero even once until the state $z^{\prime}_{1}$ is
reached in this run. Therefore, we can execute the increment/decrement
operation on $v$. Furthermore, since $z_{1}\leq z^{\prime}_{1}$ (resp.
$z_{1}<z^{\prime}_{1}$), the value of $v$ in $z^{\prime}_{1}$ is greater than
or equal to (resp. strictly greater than) the value of $v$ in $z_{1}$. Hence,
we can execute $a$ from $z^{\prime}_{1}$ and reach a state $z_{2}^{\prime}$
such that $z_{2}\leq z_{2}^{\prime}$ (resp. $z_{2}<z_{2}^{\prime}$).

  3. Case iii:

$Z\neq\emptyset$ in the transition $z_{1}\xrightarrow{a}z_{2}$. Hence, there
are a set of counters $Z$ which are tested to zero. By the CMRZ property, we
know that all counters $v\in Z$, are never incremented or decremented further.
Hence, during the execution
$z_{1}\xrightarrow{a}z_{2}\xrightarrow{w}z^{\prime}_{1}$ where
$w\in\textsf{Act}^{*}$, we know that none of these counters are incremented or
decremented. Hence, the value of the counters in $z^{\prime}_{1}$ is also
equal to zero. Therefore, we can execute $a$ from $z^{\prime}_{1}$ to reach
$z_{2}^{\prime}$. Moreover, since $z_{1}\leq z^{\prime}_{1}$ (resp.
$z_{1}<z^{\prime}_{1}$), and none of these counters change value, we can
conclude that $z_{2}\leq z_{2}^{\prime}$ (resp. $z_{2}<z_{2}^{\prime}$).

Hence, as a special case of the claim where $\nu=\sigma$, we prove that CMRZ
are branch-monotone (resp. strictly branch-monotone).

######  Proposition 15.

CMRZs are branch-effective branch-WSTS.

######  Proof 4.2.

Given an OLTS $\mathcal{S}=(X,A,$ $\xrightarrow{},\leq,x_{0})$ associated to a
CMRZ, for any two states $x,x^{\prime}\in X$, we can decide if $x\leq
x^{\prime}$. Furthermore, $\xrightarrow{}$ is decidable from the underlying
finite automaton, and $\textsf{Post}_{\mathcal{S}}(x)$ is computable for all
$x\in X$. Hence, it is branch-effective.

Hence, we deduce:

######  Theorem 16.

Non-termination and boundedness are decidable for counter machines with
restricted zero tests.

###  4.2. Input-bounded FIFO machines

The FIFO machine $\mathcal{M}_{1}$ from Figure 1 is an example of a system
that is branch-WSTS but the underlying set of states is not well-quasi-
ordered. We first try to generalize a class of systems which are branch-wqo,
and which includes $\mathcal{M}_{1}$.

We consider a restriction that has been studied in [BFS20], which we go on to
prove is branch-wqo. These systems are known as input-bounded FIFO machines,
which we formally define below.

Consider a FIFO machine $\mathcal{M}=(Q,A,T,q_{0})$ over a set of channels Ch.
For $\textsf{c}\in\textsf{Ch}$, we let
${\mathit{proj}}_{\textsf{c}!}:\\{\textsf{Ch}\times\\{!,?\\}\times A\\}^{*}\to
A^{*}$ be the homomorphism defined by
$\mathit{proj}_{\textsf{c}!}(\textsf{c}!a)=a$ for all $a\in A$, and
$\mathit{proj}_{\textsf{c}!}(\alpha)=\varepsilon$ if $\alpha$ is not of the
form $\textsf{c}!a$ for some $a\in A$. Moreover,
$\mathit{proj}_{\textsf{c}!}(\tau_{1}\cdot\tau_{2})=\mathit{proj}_{\textsf{c}!}(\tau_{1})\cdot\mathit{proj}_{\textsf{c}!}(\tau_{2})$.
Similarly, for $\textsf{c}\in\textsf{Ch}$, we let
${\mathit{proj}}_{\textsf{c}?}:\\{\textsf{Ch}\times\\{!,?\\}\times A\\}^{*}\to
A^{*}$ be the homomorphism defined by
$\mathit{proj}_{\textsf{c}?}(\textsf{c}?a)=a$ for all $a\in A$, and
$\mathit{proj}_{\textsf{c}?}(\alpha)=\varepsilon$ if $\alpha$ is not of the
form $\textsf{c}?a$ for some $a\in A$. Moreover,
$\mathit{proj}_{\textsf{c}?}(\tau_{1}\cdot\tau_{2})=\mathit{proj}_{\textsf{c}?}(\tau_{1})\cdot\mathit{proj}_{\textsf{c}?}(\tau_{2})$.

We define the input-language of a FIFO channel c as the set of all words that
are sent into the channel, i.e.
$\mathit{proj}_{\textsf{c}!}(\textsf{Traces}(\mathcal{M}))$. We say that the
machine is _input-bounded_ if for each $\textsf{c}\in\textsf{Ch}$, there is a
regular bounded language $\mathcal{L}_{\textsf{c}}$ (i.e. language of the form
$w_{1}^{*}\ldots w_{n}^{*}$) such that
$\mathit{proj}_{\textsf{c}!}(\textsf{Traces}(\mathcal{M}))\subseteq\mathit{Pref}(\mathcal{L}_{\textsf{c}})$,
i.e. the send-projection of every run of the FIFO machine over each channel is
a prefix of an input-bounded language. We say that $\mathcal{L}_{\textsf{c}}$
is distinct-letter if $|w_{1}\ldots w_{n}|_{a}=1$ for all $a\in A$.

######  Proposition 17.

Input-bounded FIFO machines are branch-wqo for the prefix-ordering $\leq_{p}$.

######  Proof 4.3.

Let us consider the transition system
$\mathcal{S}_{\mathcal{M}}=(X_{\mathcal{M}},\Sigma_{\mathcal{M}},\xrightarrow{}_{\mathcal{M}},x_{0})$
associated an input-bounded FIFO machine $\mathcal{M}$ with a single channel
c, and an infinite run
$x_{0}\xrightarrow{}x_{1}\xrightarrow{}x_{2}\xrightarrow{}...x_{i}...$ with
$x_{i}=(q_{i},w_{i})\in X_{\mathcal{M}}$.

The infinite run is of the form
$x_{0}\xrightarrow{\sigma_{1}}x_{1}\xrightarrow{\sigma_{2}}x_{2}...x_{i-1}\xrightarrow{\sigma_{i}}x_{i}\xrightarrow{\sigma_{i+1}}\ldots$
and we denote
$\sigma[i]=\mathit{proj}_{\textsf{c}!}(\sigma_{1}\sigma_{2}\ldots\sigma_{i})$.
It can be observed that $\sigma[i]$ is a prefix of $\sigma[i+1]$ for all
$i\in\mathbb{N}$. Since $\sigma[i]$ is of the form
$v_{1}^{n_{1,i}}...v_{m}^{n_{m,i}}u_{m}$ for $u_{m}\preceq v_{m}$ and
$n_{1,i}...,n_{m,i}\geq 0$ and $1\leq m\leq k$, the infinite sequence
$(\sigma[i])_{i\in\mathbb{N}}$ satisfies two possible exclusive cases:

  1. Case i:

There exists an $i_{0}$ such that $\forall i\geq
i_{0},\mathit{proj}_{\textsf{c}!}(\sigma_{i})=\varepsilon$ so there exists
$i_{1}\geq i_{0}$ such that for all $i\geq i_{1},w_{i}=w_{i+1}$. Hence,
because there are finitely many control-states, we deduce that there exist
$i_{2},i_{3}\geq i_{1}$ such that $x_{i_{2}}\xrightarrow{+}x_{i_{3}}$ and
$x_{i_{2}}=x_{i_{3}}$ hence also in particular $x_{i_{2}}\leq_{p}x_{i_{3}}$.

  2. Case ii:

There are infinitely many indices $i$ such that
$\mathit{proj}_{\textsf{c}!}(\sigma_{i})\neq\varepsilon$, which means that the
infinite sequence $(\sigma[i])_{i\in\mathbb{N}}$ is not stationary. This
implies that the set $S_{\sigma}=\\{(n_{1,i},...,n_{k,i})\mid
i\in\mathbb{N}\\}$, associated with $\sigma$, is infinite. Hence, there exists
a least index $p$ such that the set $\\{n_{p,i}\\}_{i\in\mathbb{N}}$ is
infinite. Then the set $F=\\{(n_{1,i},...,n_{p-1,i})\mid i\in\mathbb{N}\\}$ is
finite.

We claim that for all indices $\ell\geq p+1$, $n_{\ell,i}=0$ for all $i$. Let
us assume to the contrary that there is some index $\ell\geq p+1$ and $i_{0}$
such that $n_{\ell,i_{0}}\neq 0$. This means that the word $v_{\ell}$ is in
the channel in state $x_{i_{0}}$, which means that the word $v_{\ell}$ was
sent to the channel before (or at) the step $i_{0}$, i.e,
$\sigma[i_{0}]=v_{1}^{n_{1,{i_{0}}}}...v_{p}^{n_{p,{i_{0}}}}...v_{m}^{n_{m,{i_{0}}}}u_{m}$
for some $u_{m}\preceq v_{m}$ and $n_{\ell,{i_{0}}}>0$ and $1\leq m\leq k$.
So, in particular, word $v_{p}$ cannot be sent after $i_{0}$, hence,
$n_{p,i}=n_{p,{i_{0}}}$ $\forall i>i_{0}.$ Hence,
$\\{n_{p,i}\\}_{i\in\mathbb{N}}$ is finite which is a contradiction to our
assumption that $\\{n_{p,i}\\}_{i\in\mathbb{N}}$ is infinite.

This means that after some state $x_{t}$, we only write word $v_{p}$ to the
channel. Since, the set $F=\\{(n_{1,j},...,n_{p-1,j})\mid j\in\mathbb{N}\\}$
is finite, we can extract an infinite subsequence $(q,w_{i})_{i\in
K\subseteq\mathbb{N}}$ where $w_{i}=uv_{p}^{n_{p,i}}$ with $u\in F$ and
$(n_{p,i})_{i\in K}$ is non-decreasing. Hence, there exist two indices $a,b>0$
such that $w_{a}=u.v_{p}^{n_{p,a}}$ and $w_{a+b}=u.v_{p}^{n_{p,a+b}}$ and
$n_{p,a}\leq n_{p,a+b}$ hence $w_{a+b}=w_{a}.v_{p}^{n_{p,a+b}-n_{p,a}}$ hence
$w_{a}\preceq w_{a+b}$. So we have found two states $x_{a},x_{a+b}$ such that
$x_{a}\leq_{p}x_{a+b}$. Hence, the machine is branch-wqo for the prefix
ordering.

Using the same argument for each channel, we can conclude that input-bounded
FIFO machines with multiple channels are branch-wqo for the extended prefix-
ordering $\leq_{p}$.

It is clear that $\mathcal{M}_{1}$ from Figure 1 belongs to this class of FIFO
machines. But, we see below that the class of input-bounded FIFO machines is
not branch-WSTS. Consider the FIFO machine $\mathcal{M}_{3}$ with a single
channel c in Figure 4 that is (distinct-letter) input-bounded for
$\mathcal{L}_{\textsf{c}}=(ab)^{*}$. We have
$(q_{0},\varepsilon)\xrightarrow{\sigma}(q_{0},b)$, where $\sigma=!a!b?a$.
Moreover, $(q_{0},\varepsilon)\leq_{p}(q_{0},b)$. However, we cannot repeat
$\sigma$ from $(q_{0},b)$, as it is not possible to execute
$(q_{2},bab)\xrightarrow{?a}$. Hence, the machine is not branch-monotone for
the prefix-ordering.

$q_{0}$$q_{1}$$q_{2}$$!a$$?a$$!b$ Figure 4. The FIFO machine $\mathcal{M}_{3}$

From the above counter-example, we see that the class of distinct-letter
input-bounded FIFO machines are not branch-WSTS. Hence, we impose another
restriction on such systems.

Consider an input-bounded FIFO machine
$\hat{\mathcal{M}}=(\hat{Q},A,\hat{T},q_{0})$ (over a set of channels Ch) with
a distinct-letter bounded input-language
$\mathcal{L}=(\mathcal{L}_{\textsf{c}})_{\textsf{c}\in\textsf{Ch}}$. We first
consider a deterministic finite automaton
$\mathcal{A}=(Q_{\mathcal{A}},\Sigma_{\mathcal{M}},\xrightarrow{}_{\mathcal{A}},q^{0}_{\mathcal{A}},F_{\mathcal{A}})$,
with set of final states $F_{\mathcal{A}}\subseteq Q_{\mathcal{A}}$, whose
language is
$L(\mathcal{A})=\mathcal{L}_{!}\mathrel{\cap}\mathit{Pref}(\mathcal{L}_{?})$,
where
$\mathcal{L}_{!}=\\{\sigma\mid\mathit{proj}_{\textsf{c}!}(\sigma)\in\mathcal{L}_{\textsf{c}}\text{
for all }\textsf{c}\in\textsf{Ch}\\}$ and
$\mathcal{L}_{?}=\\{\sigma\mid\mathit{proj}_{\textsf{c}?}(\sigma)\in\mathcal{L}_{\textsf{c}}\text{
for all }\textsf{c}\in\textsf{Ch}\\}$. With this, we define
$\bar{\mathcal{M}}_{\mathcal{L}}=(Q,A,T,q_{0})$ as the product of the FIFO
machine $\hat{\mathcal{M}}$ and $\mathcal{A}$ in the expected manner. In
particular, the set of control-states of $\bar{\mathcal{M}}_{\mathcal{L}}$ is
$Q=\hat{Q}\times Q_{\mathcal{A}}$, and its initial state is the pair
$q_{0}=(\hat{q_{0}},q^{0}_{\mathcal{A}})$.

We assume we are given an input-bounded FIFO machine $\hat{\mathcal{M}}$ and
its input language $\mathcal{L}$. Let $\bar{\mathcal{M}}_{\mathcal{L}}$ be the
FIFO machine constructed as above. Then:

######  Proposition 18.

The machine $\bar{\mathcal{M}}_{\mathcal{L}}$ is branch-monotone.

######  Proof 4.4.

We show this proof for a FIFO machine with a single channel c, but the same
argument can be extended to FIFO machines with multiple channels.

Let $\mathcal{L}=w_{1}^{*}\ldots w_{n}^{*}$. Let
$(q_{0},\varepsilon)\xrightarrow{\tau}(q,w)\xrightarrow{\sigma}(q,w^{\prime})$
such that $w\preceq w^{\prime}$. To prove branch-monotony, we need to show
that there exists $w^{\prime\prime}$ such that
$(q,w^{\prime})\xrightarrow{\sigma}(q,w^{\prime\prime})$ and
$w^{\prime}\preceq w^{\prime\prime}$.

Since $\mathcal{L}$ is a bounded language, we know that
$\mathit{proj}_{\textsf{c}!}(\tau)=w_{1}^{n_{1}}\ldots w_{i}^{n_{i}}.u_{i}$
where $u_{i}\preceq w_{i}$ and $1\leq i\leq n$ and $n_{p}\in\mathbb{N}$ for
all $1\leq p\leq i$. Moreover,
$\mathit{proj}_{\textsf{c}!}(\sigma)\in\mathit{Pref}(u^{\prime}_{i}\cdot
w_{i}^{n^{\prime}_{i}}\ldots w_{j}^{n_{j}})$ where
$u_{i}.u^{\prime}_{i}=w_{i}$ and $1\leq i\leq j\leq n$. Let us consider the
channel content $w$ now. From the characterization of $\tau$ above, we can
express $w=v_{\ell}\cdot w_{\ell}^{n_{\ell}}\ldots w_{i}^{n_{i}}.u_{i}$, where
$1\leq\ell\leq i$ and $v_{\ell}\in\mathit{Suf}(w_{\ell})$. Now, let us analyse
the cases based on the value of $\mathit{proj}_{\textsf{c}?}(\sigma)$:

  1. Case i:

$\mathit{proj}_{\textsf{c}?}(\sigma)=\varepsilon$. In other words, this means
that there are only send actions in $\sigma$. Hence, it is possible to repeat
the same sequence of moves as we are in the same control-state $q$. Therefore,
$(q,w^{\prime})\xrightarrow{\sigma}(q,w^{\prime\prime})$ for some value of
$w^{\prime\prime}$. Furthermore, since $\sigma$ has only send actions,
$w^{\prime}=w.v$ for some $v\in A^{*}$. Therefore, after we repeat $\sigma$
once again from $(q,w^{\prime})$, we reach $(q,w^{\prime\prime})$ such that
$w^{\prime\prime}=w^{\prime}.v=w.v.v$. Therefore,
$(q,w^{\prime})\leq_{p}(q,w^{\prime\prime})$ and we are done with this case.

  2. Case ii:

$\mathit{proj}_{\textsf{c}?}(\sigma)\neq\varepsilon$.

    1. Case a:

Let us first consider that $w\neq\varepsilon$.

Let us first assume $\exists p_{1},p_{2}\cdot~{}1\leq p_{1}<p_{2}\leq i$ such
that $w=v_{p_{1}}.v.u_{p_{2}}$ where $v_{p_{1}}\in\mathit{Suf}(w_{p_{1}})$,
$u_{p_{2}}\in\mathit{Pref}(w_{p_{2}})$, and
$v_{p_{1}},u_{p_{2}}\neq\varepsilon$ and $v\in A^{*}$. In other words, there
is a non-empty part of at least two distinct words in the channel contents
$w$. Since the FIFO machine is input-bounded, we can conclude that
$\mathit{proj}_{\textsf{c}!}(\sigma)$ does not contain any occurrences of
alphabets from the word $w_{p_{1}}$. Therefore, in order for the condition
$w\preceq w^{\prime}$ to be satisfied, it is necessary that
$\mathit{proj}_{\textsf{c}?}(\sigma)=\varepsilon$, which is a contradiction to
our assumption.

Therefore, if $w\neq\varepsilon$, then the only possibility is that
$w=v_{i}.w_{i}^{n_{i}}.u_{i}$ such that $v_{i}\in\mathit{Suf}(w_{i})$.
Therefore, $\mathit{proj}_{\textsf{c}?}(\sigma)$ only consists of letters from
words $w_{j}$ such that $j\geq i$. However, since $w\preceq w^{\prime}$, we
can be certain that it only consists of letters from the word $w_{i}$ (if the
head of the channel contains letters from a word $w_{j}$ where $j>i$ from the
channel, then there can be no occurrence of the word $w_{i}$ in the channel).
Therefore, $\mathit{proj}_{\textsf{c}?}(\sigma)$ consists of only letters
belonging to $w_{i}$. Moreover, since $\mathit{proj}_{\textsf{c}!}(\sigma)$ is
non-empty, there is at least one letter that is read from $w$. Therefore, the
first letter that is sent in the sequence $\sigma$ belongs to the word $w_{i}$
(to ensure $w\preceq w^{\prime}$).

Let us consider this subsequence $\sigma^{\prime}$ from $(q,w)$ to the first
send action. Let us say we have
$(q,w)\xrightarrow{\sigma^{\prime}}(q^{\prime},v^{\prime})$. Now, since the
subsequence $\sigma^{\prime}$ only consists of receptions from $(q,w)$, along
with the first send action, this subsequence is also possible from $(q,w.v)$
for all $v\in\Sigma^{*}$. Therefore, we can execute the same sequence from
$(q,w^{\prime})$. Hence,
$\mathit{proj}_{\textsf{c}!}(\tau.\sigma.\sigma^{\prime})\in\mathcal{L}$.
Therefore, since
$\mathit{Alph}(\mathit{proj}_{\textsf{c}!}(\sigma^{\prime}))\in\mathit{Alph}{(w_{i})}$,
we can be sure that
$\mathit{Alph}{(\mathit{proj}_{\textsf{c}!}(\sigma))}\in\mathit{Alph}{(w_{i})}$.
Therefore, $\sigma$ only sends and receives letters from a single word
$w_{i}$.

Moreover, since the system is input-bounded, and the first send action in
$\sigma^{\prime}$ matches the first send action in $\sigma$, we see that
$w^{\prime}=v_{i}.w_{i}^{n_{i}}.u_{i}.(v^{\prime}_{i}.w_{i}^{n^{\prime}_{i}}.u_{i})$
${=w.(v^{\prime}_{i}.w_{i}^{n^{\prime}_{i}}.u_{i})}$ such that
$u_{i}.v^{\prime}_{i}=w_{i}$. Therefore, we can repeat this sequence from
$(q,w^{\prime})$ and reach a state $(q,w^{\prime\prime})$ such that
$w^{\prime}\preceq w^{\prime\prime}$, and hence, it is branch-monotone for
this case.

    2. Case b:

The final case we need to consider is $w=\varepsilon$. In this case, it is
clear that $\sigma$ consists of at least one send action before the first
reception. Therefore, because of the input-bounded property and the fact that
this action can be executed at $(q,w^{\prime})$, we can once again see that
$\mathit{proj}_{\textsf{c}!}(\sigma)$ consists only sending only letters from
a single word. Moreover, since the same action can be executed, once again we
see that $\mathit{proj}_{\textsf{c}!}(\sigma)=v_{j}.w_{j}^{n_{j}}.u_{j}$ such
that $u_{j}.v_{j}=w_{j}$. Therefore,
$\mathit{proj}_{\textsf{c}?}(\sigma)\in\mathit{Pref}(v_{j}.w_{j}^{n_{j}}.u_{j})$.

Now let us consider the run $\tau.\sigma$ in the automaton $\mathcal{A}$ that
we constructed. Since $\tau.\sigma$ is a run in
$\bar{\mathcal{M}}_{\mathcal{L}}$, there is also a run in $\mathcal{A}$ such
that $q^{0}_{\mathcal{A}}\xrightarrow{\tau}q_{s}\xrightarrow{\sigma}q_{s}$.
Moreover, we can also repeat $\sigma$ to obtain
$q^{0}_{\mathcal{A}}\xrightarrow{\tau}q_{s}\xrightarrow{\sigma}q_{s}\xrightarrow{\sigma}q_{s}$.
Therefore, $\tau.\sigma.\sigma\in\mathit{Pref}(\mathcal{L}_{?})$. Moreover,
since $\mathit{proj}_{\textsf{c}?}(\sigma)\neq\varepsilon$,
$\mathit{proj}_{\textsf{c}?}(\sigma)=u^{\prime}_{j}.w_{j}^{n^{\prime}_{j}}.v^{\prime}_{j}$
such that $v^{\prime}_{j}.u^{\prime}_{j}=w_{j}$. Therefore, we can repeat
$\sigma$ from $(q,w^{\prime})$ in $\bar{\mathcal{M}}_{\mathcal{L}}$, and we
reach a state $(q,w^{\prime\prime})$ such that $w^{\prime}\preceq
w^{\prime\prime}$.

Hence, we see that for all cases, if
$(q_{0},\varepsilon)\xrightarrow{\tau}(q,w)\xrightarrow{\sigma}(q,w^{\prime})$
such that $w\preceq w^{\prime}$, then there exists $w^{\prime\prime}$ such
that $(q,w^{\prime})\xrightarrow{\sigma}(q,w^{\prime\prime})$ and
$w^{\prime}\preceq w^{\prime\prime}$.

If we have more than one channel, we can extend this argument to consider each
channel, and hence, $\bar{\mathcal{M}}_{\mathcal{L}}$ is branch-monotone.

Consider the FIFO machine $\mathcal{M}_{4}$ as in Figure 5 that is input-
bounded for $\mathcal{L}=(ab)^{*}$. As we saw in Example 4.2, it is not
branch-monotone. However, let us consider the product
$\bar{\mathcal{M}}_{4,\mathcal{L}}$ of $\mathcal{M}_{4}$ along with the finite
automaton $\mathcal{A}$ that recognizes
$\mathcal{L}_{!}\cap\mathit{Pref}(\mathcal{L}_{?})$. We depict only accessible
states of $\mathcal{M}_{4,\mathcal{L}}$, from which we can still complete the
word read so far to a word belonging to
$\mathcal{L}_{!}\cap\mathit{Pref}(\mathcal{L}_{?})$. Here, we see that the run
we had in counter-example previously no longer violates branch-monotony. In
fact, the loop that could not be realized has now been unfolded, and we can
see that the FIFO machine $\mathcal{M}_{4}$ has only a finite run. Trivially,
due to the absence of loops, we see that it is now branch-monotone for the
prefix-ordering.

$q_{0}$$q_{1}$$q_{2}$$!a$$?a$$!b$$\mathcal{M}_{4}$
$s_{0}$$s_{1}$$r_{0}$$r_{1}$$!a$$!b$$?a$$?b$$L(\mathcal{A}_{s})=\mathcal{L}_{!}$
$L(\mathcal{A}_{r})=\mathit{Pref}(\mathcal{L}_{?})$ $q_{0}$, $s_{0},r_{0}$
$q_{1}$, $s_{1},r_{0}$ $q_{2}$, $s_{0},r_{0}$ $q_{0}$, $s_{0},r_{1}$ $q_{1}$,
$s_{1},r_{1}$ $q_{1}$, $s_{1},r_{1}$
$!a$$!b$$?a$$!a$$!b$$\bar{\mathcal{M}}_{4,\mathcal{L}}$ Figure 5. The FIFO
machine $\mathcal{M}_{4}$ (right) and the automata $\mathcal{A}_{s}$ and
$\mathcal{A}_{r}$ (left) that recognize $\mathcal{L}_{!}$ and
$\mathit{Pref}(\mathcal{L}_{?})$ respectively intersect to give
$\bar{\mathcal{M}}_{4,\mathcal{L}}$(below) which is branch-monotone.

We remark here that in [BFS20], when the authors show that input-bounded
rational-reachability is decidable, they construct a “normalized” FIFO
machine, from the given FIFO machine and bounded language. Using the same
principles, we can modify every input-bounded FIFO machine into one that is
distinct-letter, and using the product construction from above, we have the
following proposition:

######  Proposition 19.

Normalized input-bounded FIFO machines are branch-effective branch-WSTS (for
the prefix ordering).

######  Proof 4.5.

Given an input-bounded FIFO machine $\mathcal{S}_{\mathcal{M}}$, for any two
states $x,x^{\prime}\in X$, we can decide if $x\leq_{p}x^{\prime}$.
Furthermore, $\xrightarrow{}$ is decidable, and
$\textsf{Post}_{\mathcal{S}}(x)$ is computable for all $x\in X$. Hence, it is
branch-effective.

Moreover, the extended prefix ordering is a partial ordering. Hence, we
deduce:

######  Theorem 20.

Non-termination and boundedness are decidable for input-bounded FIFO machines.

###  4.3. Verifying non-termination and boundedness for general counter
machines

We saw in Section 4.1 that non-termination and boundedness are decidable for
CMRZ. However, this class of counter machines is weak as every run in such a
machine has to maintain the restriction. In this section, we show that we can
study these problems for a larger class of counter machines, where the branch-
well-structured behaviour is only maintained for a single run.

We begin by constructing the labelled-$\mathit{RRT}$ (denoted by
$\mathit{l}\text{-}\mathit{RRT}$), which is a refinement of the
$\mathit{RRT}$, where we add an additional label, which we will call
_iterable_. We mark a dead vertex $n^{\prime}$ (labelled by $x^{\prime}$) as
_iterable_ if

  * •

it is subsumed by a node $n$ labelled by $x$, i.e. $x\leq x^{\prime}$ and
$\exists\sigma.x\xrightarrow{\sigma}x^{\prime}$, and

  * •

there exists a state $x^{\prime\prime}\in X$, such that,
$x^{\prime}\xrightarrow{\sigma}x^{\prime\prime}$ and $x^{\prime}\leq
x^{\prime\prime}$.

For counter machines, we show that the presence of an iterable node in the
$\mathit{l}\text{-}\mathit{RRT}$ is a sufficient condition for unboundedness
and non-termination.

######  Proposition 21.

A counter machine $\mathcal{S}=(X,\textsf{Act},\xrightarrow{},\leq,x_{0})$ is
non-terminating if $\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$ has at
least one iterable node.

######  Proof 4.6.

Let $\mathcal{S}=(X,\textsf{Act},\xrightarrow{},\leq,x_{0})$ be the OLTS
associated to a counter machine, and
$\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$ its labelled reduced
reachability tree. We show that if there exists an iterable node in
$\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$, then $\mathcal{S}$ is
non-terminating. Let us assume there is an iterable node labelled by $x_{1}$
in $\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$. By definition, this
means that there exists a run
$x_{0}\xrightarrow{*}x_{1}\xrightarrow{\sigma}x_{2}\xrightarrow{\sigma}x_{3}$.

Let $x_{i}=(q,{\ell}_{i})$ for $i\in\\{1,2,3\\}$, where
$\ell_{i}=(\ell_{i,v})_{v\in V}$ represents the counter values. Let
$\sigma=a_{1}a_{2}\ldots a_{n}$. Then we have,
$x_{1}\xrightarrow{a_{1}}u_{1}\xrightarrow{a_{2}}\ldots\xrightarrow{a_{n-1}}u_{n-1}\xrightarrow{a_{n}}x_{2}$
and
$x_{2}\xrightarrow{a_{1}}u_{1}^{\prime}\xrightarrow{a_{2}}\ldots\xrightarrow{a_{n-1}}u_{n-1}^{\prime}\xrightarrow{a_{n}}x_{3}$.
Let $u_{i}=(q_{i},{m}_{i})$, and $u_{i}^{\prime}=(q_{i},{m}^{\prime}_{i})$ for
$1\leq i<n$, where ${m}_{i}=({m}_{i,v})_{v\in V}$ and
${m}^{\prime}_{i}=({m}^{\prime}_{i,v})_{v\in V}$ represent the counter values.

Since $x_{1}\leq x_{2}$, for each counter $v\in V$, the following holds:
$\ell_{2,v}=\ell_{1,v}+k_{v}$, where $k\geq 0$. Moreover, because both runs
perform the same sequence of actions, we also have the following property: for
all $1\leq i\leq n$, ${m}^{\prime}_{i,v}={m}_{i,v}+k_{v}$.

Let us assume that there exists a transition
$u_{i-1}\xrightarrow{a_{i}}u_{i}$, such that $a_{i}=\textsf{op}(v_{i}),Z_{i}$,
for some $v_{i}\in V$, and where $Z_{i}\neq\emptyset$, then we also have
$u^{\prime}_{i-1}\xrightarrow{a_{i}}u^{\prime}_{i}$. Therefore, the set of
counters $Z_{i}$ to be tested to zero in $u_{i-1}$ is the same as the set of
counters to be tested to zero in $u^{\prime}_{i-1}$. And the action $a_{i}$ is
feasible from both $u_{i}$ and $u_{i}^{\prime}$. Therefore, for each counter
$v\in Z_{i}$, we have ${m}_{i,v}={m}^{\prime}_{i,v}$, i.e. $k_{v}=0$. In other
words, for each counter $v\in V$ that is tested to zero along $\sigma$,
$k_{v}=0$, i.e. the values of those counters are identical along both runs.

Let us now only consider the set of counters tested for zero along $\sigma$,
and call this set of counters $Z_{\sigma}$. The following property holds:
$\ell_{1,v}=\ell_{2,v}$ for all $v\in Z_{\sigma}$. Now, from $(q,\ell_{2})$,
upon executing the sequence of transitions $\sigma$, for every counter in
$Z_{\sigma}$, once again the values do not change. Therefore, we have the
following property: $\ell_{2,v}=\ell_{3,v}$ for all $v\in Z_{\sigma}$. For
counters $v\in V\setminus Z_{\sigma}$, $\ell_{2,v}=\ell_{1,v}+k_{v}$. However,
since there are no zero tests for these counters along $\sigma$, we can repeat
the same sequence of actions and obtain: $\ell_{3,v}=\ell_{2,v}+k_{v}$.

Therefore, from $x_{3}=(q,{\ell}_{3})$, once again we can repeat $\sigma$ in
order to reach a state $x_{4}=(q,{\ell}_{4})$ such that for all $v\in
Z_{\sigma}$, $\ell_{3,v}=\ell_{4,v}$ and for all counters $m\in V\setminus
Z_{\sigma}$, $\ell_{4,m}=\ell_{3,m}+k_{m}$. Therefore, we can repeat $\sigma$
infinitely many times. Hence, $\mathcal{S}$ is non-terminating.

###  4.4. Verifying non-termination and boundedness for FIFO machines

Now, we extend the same idea as above for branch-wqo FIFO machines.

Let us assume that given a FIFO machine, we have:
$(q,u)\xrightarrow{\sigma}(q,u.v)$, and $\exists w\in\Sigma^{*}$ such that
$(q,u.v)\xrightarrow{\sigma}(q,u.v.w)$. Then, for all
$\textsf{c}\in\textsf{Ch}$:

$\displaystyle
u_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma)=\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}$
(1) $\displaystyle
u_{\textsf{c}}.v_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma)=\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}.w_{\textsf{c}}$
(2)

From the above two equations, we have

$u_{\textsf{c}}.v_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma)=u_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma).w_{\textsf{c}}$
(3)

Hence, we have:

$v_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma)=\mathit{proj}_{\textsf{c}!}(\sigma).w_{\textsf{c}}$
(4)

Moreover,

$\displaystyle|\mathit{proj}_{\textsf{c}!}(\sigma)|=|\mathit{proj}_{\textsf{c}?}(\sigma)|+|v_{\textsf{c}}|$
(5)
$\displaystyle|\mathit{proj}_{\textsf{c}!}(\sigma)|=|\mathit{proj}_{\textsf{c}?}(\sigma)|+|w_{\textsf{c}}|$
(6)

Hence, the length of $\mathit{proj}_{\textsf{c}!}(\sigma)$ is at least as much
as that of $v_{\textsf{c}}$ and $w_{\textsf{c}}$. Moreover,

$|v_{\textsf{c}}|=|w_{\textsf{c}}|$ (7)

Moreover, from Equation 4.1, we see that $v_{\textsf{c}}$ is a suffix of
$\mathit{proj}_{\textsf{c}!}(\sigma)$. Similarly, from Equation 4.2, we see
that $w_{\textsf{c}}$ is a suffix of $\mathit{proj}_{\textsf{c}!}(\sigma)$.
Since $|v_{\textsf{c}}|=|w_{\textsf{c}}|$, we have
$v_{\textsf{c}}=w_{\textsf{c}}$. We can now rewrite Equation 4.4 as:

$v_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma)=\mathit{proj}_{\textsf{c}!}(\sigma).v_{\textsf{c}}$
(8)

The well-known Levi’s Lemma says that the words $u,v\in\Sigma^{*}$ that are
solutions of the equation $uv=vu$ satisfy $u,v\in z^{*}$ where
$z\in\Sigma^{*}$ is a primitive word.

For FIFO machines also, we show that an iterable node in the
$\mathit{l}\text{-}\mathit{RRT}$ can indicate the presence of a non-
terminating run. Before we prove that, we first restate a result from [FP20]
that we will use.

######  Proposition 22 ([FP20]).

Given a FIFO machine, the loop labelled by $\sigma$ is infinitely iterable
from a state $(q,\mathbf{w})$ iff for every channel
$\textsf{c}\in\textsf{Ch}$, either
$\mathit{proj}_{\textsf{c}?}(\sigma)=\varepsilon$, or the following three
conditions are true: $\sigma$ is fireable at least once from $(q,\mathbf{w})$,
$|\mathit{proj}_{\textsf{c}?}(\sigma)|\leq|\mathit{proj}_{\textsf{c}!}(\sigma)|$
and
$\mathbf{w}_{\textsf{c}}\cdot(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}=(\mathit{proj}_{\textsf{c}?}(\sigma))^{\omega}$.

Now, we will use the above result to provide a _sufficient_ condition for non-
termination in FIFO machines.

######  Proposition 23.

A FIFO machine $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq_{p},x_{0})$ is non-
terminating if $\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$ has at
least one iterable node.

######  Proof 4.7.

Let $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq_{p}x_{0})$ be a FIFO machine,
and $\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$ its labelled
reachability tree. Let us assume that there exists an iterable node
$n^{\prime}$ labelled by $x^{\prime}$ in
$\mathit{l}\text{-}\mathit{RRT}(\mathcal{S},x_{0})$. Then, by definition, we
have a run
$x_{0}\xrightarrow{*}x\xrightarrow{\sigma}x^{\prime}\xrightarrow{\sigma}x^{\prime\prime}$
such that $x\leq_{p}x^{\prime}\leq_{p}x^{\prime\prime}$. Let
$x=(q,\mathbf{w})$, $x^{\prime}=(q,\mathbf{w}^{\prime})$ and
$x^{\prime\prime}=(q,\mathbf{w}^{\prime\prime})$. From Equations 4.1 through
4.7, we know that for all $\textsf{c}\in\textsf{Ch}$, if
$\mathbf{w}_{\textsf{c}}=u_{\textsf{c}}$, then
$\mathbf{w}^{\prime}_{\textsf{c}}=u_{\textsf{c}}\cdot v_{\textsf{c}}$, and
$\mathbf{w}^{\prime\prime}_{\textsf{c}}=u_{\textsf{c}}\cdot
v_{\textsf{c}}\cdot v_{\textsf{c}}$, for some words
$u_{\textsf{c}},v_{\textsf{c}}\in\Sigma^{*}$.

In order to show that $\mathcal{S}$ is non-terminating, we will try to
demonstrate the criteria in Proposition 22. We will show that $\sigma$ is
infinitely iterable from $x=(q,\mathbf{w})$. For each
$\textsf{c}\in\textsf{Ch}$ such that
$\mathit{proj}_{\textsf{c}?}(\sigma)=\varepsilon$, the condition in the
proposition is true trivially. Hence, we only need to show that in cases when
$\mathit{proj}_{\textsf{c}?}(\sigma)\neq\varepsilon$, the three conditions
stated are met. We will consider a single channel, but the idea can be
extended to all channels.

Since we have a run $x_{0}\xrightarrow{*}x\xrightarrow{\sigma}x^{\prime}$, the
sequence of actions $\sigma$ is fireable at least once, so the first condition
holds. Moreover, since
$(q,\mathbf{w})\xrightarrow{\sigma}(q,\mathbf{w}^{\prime})$ and for every
$\textsf{c}\in\textsf{Ch}$,
$\mathbf{w}_{\textsf{c}}\preceq\mathbf{w}^{\prime}_{\textsf{c}}$, the net
effect of the loop is not decreasing in the length of the channel contents,
i.e.
$|\mathit{proj}_{\textsf{c}?}(\sigma)|\leq|\mathit{proj}_{\textsf{c}!}(\sigma)|$.
Hence, the second condition also holds true.

We only now need to show that for all $\textsf{c}\in\textsf{Ch}$, the
following holds:
$u_{\textsf{c}}\cdot(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}=(\mathit{proj}_{\textsf{c}?}(\sigma))^{\omega}$.
From Equation 4.1, we have:

$u_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma)=\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}$

Concatenating both sides with the infinite word
$\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$, we have:

$\displaystyle u_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
$\displaystyle=\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
(9)
$\displaystyle=\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma).(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
(10)

Moreover, from Equation 4.2, we now have:

$\displaystyle u_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
$\displaystyle=\mathit{proj}_{\textsf{c}?}(\sigma).\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}.w_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
(11)
$\displaystyle=(\mathit{proj}_{\textsf{c}?}(\sigma))^{2}.u_{\textsf{c}}.v_{\textsf{c}}.v_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
(12)

Which we can rewrite using Equation 4.8 as:

$\displaystyle u_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
$\displaystyle=(\mathit{proj}_{\textsf{c}?}(\sigma))^{2}.u_{\textsf{c}}.v_{\textsf{c}}.\mathit{proj}_{\textsf{c}!}(\sigma).v_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
(13)

And now, we can repeat the process, and use Equation 4.2 once again to obtain:

$\displaystyle u_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
$\displaystyle=(\mathit{proj}_{\textsf{c}?}(\sigma))^{2}.\mathit{proj}_{\textsf{c}?}(\sigma).u_{\textsf{c}}.v_{\textsf{c}}.w_{\textsf{c}}.v_{\textsf{c}}.(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}$
(14)

Repeating this process, we have:
$u_{\textsf{c}}\cdot(\mathit{proj}_{\textsf{c}!}(\sigma))^{\omega}=(\mathit{proj}_{\textsf{c}?}(\sigma))^{\omega}$.
Hence, the presence of an iterable node in the
$\mathit{l}\text{-}\mathit{RRT}$ implies infinite iterability, or in other
words, non-termination.

As for the case of counter machines, the $\mathit{l}\text{-}\mathit{RRT}$ of
branch-wqo FIFO machines is finite. Hence, for branch-wqo FIFO machines, it is
decidable to verify if there is an iterable node in the
$\mathit{l}\text{-}\mathit{RRT}$.

##  5\. Decidability of Coverability

Coverability algorithms for branch-WSTS. We show that the two existing
coverability algorithms (the forward and backward algorithms) for WSTS (see
Section 2.2 to recall) do not allow one to decide coverability for branch-
WSTS. We remark that, contrary to WSTS,
${\textsf{Pre}^{*}(\mathord{\uparrow}x)}$ is not necessarily upward-closed. In
fact, even with a single zero-test, this property may not satisfied.

$q_{0}$$q_{1}$$c\mathord{=}0?$ Figure 6. System $\mathcal{M}_{6}$ is branch-
WSTS.

In Figure 6, let us consider the counter machine $\mathcal{M}_{6}$ with a
single counter $c$. Let $x=(q_{1},0)$. We see that
${\textsf{Pre}^{*}(\mathord{\uparrow}x)}=\\{(q_{1},n)\mid n\geq
0\\}\cup\\{(q_{0},0)\\}$. However,
${\mathord{\uparrow}\textsf{Pre}^{*}(\mathord{\uparrow}x)}={\textsf{Pre}^{*}(\mathord{\uparrow}x)}\cup\\{(q_{0},n)\mid
n\geq 1\\}$. Hence, given a branch-effective branch-WSTS
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ and a state $x\in X$, the
set $\textsf{Pre}^{*}(\mathord{\uparrow}x)$ is not necessarily upward-closed.
Hence, we cannot use the backward algorithm to verify the coverability problem
for branch-WSTS correctly.

Let us consider using the forward algorithm instead, where the first procedure
(cf. Procedure 1) checks for coverability, and the second procedure (cf.
Procedure 2) looks for a witness of non-coverability.

The second procedure computes all sets $X$ which satisfy the property
$\mathord{\downarrow}\textsf{Post}^{*}(X)\subseteq X$. This is because, for
WSTS, the set $\mathord{\downarrow}\textsf{Post}^{*}(x)$ satisfies this
property. However, we now show a counter-example of a branch-WSTS which does
not satisfy this property.

$q_{0}$$q_{1}$$q_{2}$$c{\mathord{++}}$$c\mathord{=}0?$ Figure 7. System
$\mathcal{M}_{7}$ is branch-WSTS.

Consider the counter machine $\mathcal{M}_{7}$ from Figure 7, with
$x_{0}=(q_{0},0)$. We compute
$Y=\mathord{\downarrow}\textsf{Post}^{*}(x_{0})$. We see that
$\textsf{Post}^{*}(x_{0})=\\{(q_{0},0),(q_{1},1)\\}$, hence,
$Y=\mathord{\downarrow}\textsf{Post}^{*}(x_{0})=\\{(q_{0},0),(q_{1},1),(q_{1},0)\\}$.
However, as
$\mathord{\downarrow}\textsf{Post}^{*}(Y)=\\{(q_{0},0),(q_{1},1),(q_{1},0),(q_{2},0)\\}$
is strictly larger than $Y$, we have
$\mathord{\downarrow}\textsf{Post}^{*}(Y)\not\subseteq Y$. Therefore, for
branch-effective, branch-WSTS
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ such that
$\mathord{\downarrow}\textsf{Post}(\mathord{\downarrow}x)$ is computable for
all $x\in X$, the set $Y=\mathord{\downarrow}\textsf{Post}^{*}(x_{0})$ does
not necessarily satisfy the property
$\mathord{\downarrow}\textsf{Post}^{*}(Y)\subseteq Y$. Hence, it is not
possible to guarantee the termination of the forward coverability algorithm.

We can deduce:

######  Proposition 24.

For branch-WSTS, both the backward coverability algorithm and the forward
coverability algorithm do not terminate, in general.

Not only the two coverability algorithms do not terminate but we may prove
that coverability is undecidable.

######  Theorem 25.

The coverability problem is undecidable for branch-effective branch-WSTS
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ (even if $\mathcal{S}$ is
strongly monotone and $\leq$ is wqo).

######  Proof 5.1.

We use the family of systems given in the proof of Theorem 4.3 [FMP04]. Let us
denote by $\mathit{TM}_{j}$ the $j^{th}$ Turing Machine in some enumeration.
Consider the family of functions
$f_{j}:\mathbb{N}^{2}\xrightarrow{}\mathbb{N}^{2}$ defined by
$f_{j}(n,k)=(n,0)$ if $k=0$ and $TM_{j}$ runs for more than $n$ steps, else
$f_{j}(n,k)=(n,n+k)$.

Let $g:\mathbb{N}^{2}\xrightarrow{}\mathbb{N}^{2}$ be the function defined by
$g(n,k)=(n+1,k)$. The transition system $\mathcal{S}_{j}$ induced by the two
functions $f_{j}$ and $g$ is strongly monotone hence it is also branch-
monotone. Moreover, system $\mathcal{S}_{j}$ is branch-effective and we
observe that Post is computable and $\leq$ is wqo. Now, we have $(1,1)$ is
coverable from $(0,0)$ in $\mathcal{S}_{j}$ iff $\mathit{TM}_{j}$ halts. This
proves that coverability is undecidable.

Decidability of coverability. We show that coverability is decidable for a
class of systems with a wqo but with a restricted notion of monotony. As for
example in [BFM18], we define the $Cover$ of a system $\mathcal{S}$ from a
state $x$ by:
$Cover_{\mathcal{S}}(x)=\mathord{\downarrow}\textsf{Post}_{\mathcal{S}}^{*}(x)$.
Let us consider the following monotony condition.

Let $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ be a system. We say
that $\mathcal{S}$ is _cover-monotone_ (resp. strongly cover-monotone) if, for
all $y_{1}\in Cover_{\mathcal{S}}(x_{0})$ and for all $x_{1},x_{2}\in X$ such
that $x_{1}\leq y_{1}$ and $x_{1}\xrightarrow{}x_{2}$, there exists a state
$y_{2}\in X$ such that $y_{1}\xrightarrow{*}y_{2}$ (resp.
$y_{1}\xrightarrow{}y_{2}$) and $x_{2}\leq y_{2}$.

Let us emphasize that cover-monotony of a system
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ is a property that depends
on the initial state $x_{0}$ while the usual monotony does not depend on any
initial state (see Figure 8).

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$c\mathord{=}0?$$c{\mathord{++}}$$c{\mathord{--}}$$c{\mathord{++}}$$c{\mathord{++}}$
Figure 8. Machine $\mathcal{M}_{8}$ is cover-monotone. However, if we modify
the system such that the initial state $(q_{0},1)$, then it is not cover-
monotone.

######  Remark 26.

The strong cover-monotony property is not trivially decidable for general
models while (usual) strong-monotony is decidable for many powerful models
like FIFO machines and counter machines. However, this notion is still of
theoretical interest, as it shows that we can relax the general monotony
condition.

However, there is a link between general monotony and cover-monotony.

propCoverxComp A system $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq)$ is
monotone iff for all $x_{0}\in X$, $(X,\Sigma,\xrightarrow{},\leq,x_{0})$ is
cover-monotone.

######  Proof 5.2.

Every monotone system is trivially cover-monotone for all $x_{0}\in X$.
Conversely, consider a system $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq)$
such that $(X,\Sigma,\xrightarrow{},\leq,x_{0})$ is cover-monotone for all
$x_{0}\in X$. Let us consider $x_{1},y_{1},x_{2}\in X$ such that $x_{1}\leq
y_{1}$ and $x_{1}\xrightarrow{}x_{2}$. In order to show that $\mathcal{S}$ is
monotone, we need to prove that there exists $y_{2}$ such that
$y_{1}\xrightarrow{*}y_{2}$ and $x_{2}\leq y_{2}$.

Since $x_{1}\leq y_{1}$ (by hypothesis), $x_{1}\in
Cover_{\mathcal{S}}(y_{1})$. By the hypothesis,

$(X,\Sigma,\xrightarrow{},\leq,y_{1})$ is cover-monotone, hence

there exists $y_{2}$ such that $y_{1}\xrightarrow{*}y_{2}$ with $x_{2}\leq
y_{2}$. Hence, $\mathcal{S}$ is monotone.

We may now define cover-WSTS as follows.

A _cover-WSTS_ is a finitely branching cover-monotone system
$\mathcal{S}=(X,\Sigma,$ $\xrightarrow{},\leq,x_{0})$ such that $(X,\leq)$ is
wqo.

For cover-WSTS, the backward algorithm fails. This is once again because the
presence of a single zero test removes the property of the set being upward-
closed. But we will now show that the forward coverability approach is
possible.

propinvariantPost Given a system
$\mathcal{S}=(X,\Sigma,\xrightarrow{}{},\leq,x_{0})$ and a downward-closed set
$D\subseteq X$ such that $\mathord{\downarrow}\textsf{Post}(D)\subseteq D$,
then we have the inclusion $\mathord{\downarrow}\textsf{Post}^{*}(D)\subseteq
D$.

######  Proof 5.3.

We prove the following claim by induction first.

Claim: Given a system $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$, for
every downward-closed set $D\subseteq X$ such that
$\mathord{\downarrow}\textsf{Post}(D)\subseteq D$, the following inclusion
holds: $\mathord{\downarrow}\textsf{Post}^{k}(D)\subseteq D$, for all $k\geq
1$.

Base case: For $k=1$, this is the hypothesis.

Inductive step: The inductive hypothesis asserts that: Given a system
$\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$, for every downward-closed
set $D\subseteq X$ such that $\mathord{\downarrow}\textsf{Post}(D)\subseteq
D$, the following inclusion holds:
$\mathord{\downarrow}\textsf{Post}^{k}(D)\subseteq D$.

We now prove that it is also true for $k+1$.

Let $Z=\textsf{Post}^{k}(D)$. Since
$Z\subseteq\mathord{\downarrow}\textsf{Post}^{k}(D)$, we know that $Z\subseteq
D$ (by hypothesis). Furthermore, for any subset $Y\subseteq D$,
$\mathord{\downarrow}\textsf{Post}(Y)$ is also a subset of $D$. Therefore,
$\mathord{\downarrow}\textsf{Post}(Z)\subseteq D$. Hence, we deduce
$\mathord{\downarrow}\textsf{Post}(\textsf{Post}^{k}(D))\subseteq D$, i.e.
$\mathord{\downarrow}\textsf{Post}^{k+1}(D)\subseteq D$. Hence, we have proved
the claim by induction.

From the above claim, we know that
$\mathord{\downarrow}\textsf{Post}^{k}(D)\subseteq D$ for all $D\subseteq X$.
Note also that $\textsf{Post}^{*}(D)=D\cup\bigcup\limits_{k\geq
1}\textsf{Post}^{k}(D)$. Therefore, $\textsf{Post}^{*}(D)\subseteq D$, and
finally since $D$ is downward-closed,
$\mathord{\downarrow}\textsf{Post}^{*}(D)\subseteq D$.

Let us define a particular instance of the coverability problem in which we
verify if a state is coverable from the initial state.

Given a system $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$. _The
$x_{0}$-coverability problem_ is: Given a state $y\in X$, do we have
$y\in\mathord{\downarrow}\textsf{Post}_{\mathcal{S}}^{*}(x_{0})$ ?

We show that $x_{0}$-coverability is decidable for cover-WSTS:

######  Theorem 27.

Let $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ be an ideally effective
cover-WSTS such that Post is computable. Then, the $x_{0}$-coverability
problem is decidable.

######  Proof 5.4.

Consider a system $\mathcal{S}=(X,\Sigma,\xrightarrow{},\leq,x_{0})$ that is
cover-WSTS, and let us consider a state $y\in X$. To find a certificate of
coverability (if it exists), we cannot use Procedure 1 since general monotony
is not satisfied and then, in general,
$\mathord{\downarrow}\textsf{Post}^{*}(x_{0})\neq\mathord{\downarrow}\textsf{Post}^{*}(\mathord{\downarrow}x_{0})$
but we can use a variation of Procedure 1, where we iteratively compute
$x_{0}$, $\textsf{Post}(x_{0})$, $\textsf{Post}(\textsf{Post}(x_{0}))$, and so
on, and at each step check if $y\leq x$ for some $x$ in the computed set. This
can be done because $\mathcal{S}$ is finitely branching and the sets
$\textsf{Post}^{k}(x_{0})$ are computable for all $k\geq 0$. Hence, if there
exists a state that can cover $y$ reachable from $x_{0}$, it will eventually
be found.

Now, let us prove that Procedure 2 terminates for input $y$ iff $y$ is not
coverable from $x_{0}$.

If Procedure 2 terminates, then at some point, the while condition is not
satisfied and there exists a set $D$ such that $y\notin D$ and $x_{0}\in D$
and $\mathord{\downarrow}\textsf{Post}(D)\subseteq D$. Moreover,
$\mathord{\downarrow}\textsf{Post}^{*}(I)\subseteq I$ for every inductive
invariant $I$ (see Proposition 5.2). Hence,
$Cover_{\mathcal{S}}(x_{0})\subseteq D$, therefore, since $y\notin D$, we
deduce that $y\not\in Cover_{\mathcal{S}}(x_{0})$ and then $y$ is not
coverable from $x_{0}$.

Note that every downward-closed subset of $X$ decomposes into finitely many
ideals since $(X,\leq)$ is wqo. Moreover, since $\mathcal{S}$ is ideally
effective, ideals of $X$ may be effectively enumerated. By [BFM18] and
[BFM17], for ideally effective systems, testing of inclusion of downward-
closed sets, and checking the membership of a state in a downward-closed set,
are both decidable.

To show the opposite direction, let us prove that if $y$ is not coverable from
$x_{0}$, the procedure terminates. It suffices to prove that
$Cover_{\mathcal{S}}(x_{0})$ is an inductive invariant. Indeed, this implies
that $Cover_{\mathcal{S}}(x_{0})$ is eventually computed by Procedure 2 when
$y$ is not coverable from $x_{0}$.

Let us show
$\mathord{\downarrow}\textsf{Post}(Cover_{\mathcal{S}}(x_{0}))\subseteq
Cover_{\mathcal{S}}(x_{0})$. Let
$b\in\mathord{\downarrow}\textsf{Post}(Cover_{\mathcal{S}}(x_{0}))$. Then,
there exists $a,a^{\prime},b^{\prime}$ such that
$x_{0}\xrightarrow{*}a^{\prime}$, $a^{\prime}\geq a$,
$a\xrightarrow{}b^{\prime}$ and $b^{\prime}\geq b$. Furthermore,
$a^{\prime},a\in Cover(x_{0})$. Hence, by cover-monotony, there exists
$b^{\prime\prime}\geq b^{\prime}$ such that
$a^{\prime}\xrightarrow{*}b^{\prime\prime}$. Therefore,
$x_{0}\xrightarrow{*}b^{\prime\prime}$ and $b^{\prime\prime}\geq
b^{\prime}\geq b$, hence, $b\in Cover_{\mathcal{S}}(x_{0})$. Hence, the
$x_{0}$-coverability problem is decidable.

On the other hand, we cannot decide the (general) coverability problem for
this class of systems:

######  Theorem 28.

The coverability problem is undecidable for cover-WSTS.

######  Proof 5.5.

Given any counter machine $\mathcal{C}=(Q,V,T,q_{0})$, let
$\mathcal{S}_{\mathcal{C}}=(X,A_{\mathcal{C}},\xrightarrow{},\leq,x_{0})$ be
its transition system equipped with the natural order on counters. We can
construct a system
$\mathcal{S}^{\prime}=(X^{\prime},A_{\mathcal{C}},\xrightarrow{}^{\prime},\leq,x^{\prime}_{0})$
such that $\mathcal{S}^{\prime}$ is cover-monotone, and any state $x\in X$ is
coverable iff it is also coverable in $X^{\prime}$. The construction is as
follows. We add a new control-state $q$ from the initial state in the counter
machine ($q_{0}$) reachable via an empty transition, therefore,
$X^{\prime}=X\cup\\{(q,0)\\}$. This new control-state is a sink state, i.e.
there are no transitions from $q$ to any other control-state (except itself).
Moreover, we let $x^{\prime}_{0}=(q,0)$. Note that $\mathcal{S}^{\prime}$ is
cover-monotone, because there is no state reachable from $x^{\prime}_{0}$,
hence, the property is vacuously satisfied. However, for all other states, as
we leave the system unchanged, we see that a state $x$ is coverable in
$\mathcal{S}$ by a state $y$ iff it is coverable in $\mathcal{S}^{\prime}$.
Hence, coverability for counter machines reduces to the coverability problem
for cover-WSTS, and coverability is therefore undecidable for cover-WSTS.

##  6\. Conclusion

We have tried to relax the notions of monotony and of the wellness of the
quasi-ordering which were traditionally used to define a WSTS. We observed
that we do not need the wellness of the quasi-ordering or monotony between all
states. By relaxing the conditions to only states reachable from one another,
thus defining what we call _branch-WSTS_ , we are still able to decide non-
termination and boundedness. Moreover, some systems that have been studied
recently have been shown to belong to this class, which adds interest to this
relaxation. Furthermore, we have used the ideas of branch-monotony to hold
along a single run, in order to provide an algorithm that can decide non-
termination and boundedness for a larger class of counter machines and branch-
wqo FIFO machines.

However, as coverability is undecidable for branch-WSTS, the notion of
coverability seems to require a stricter condition than what we define for
branch-WSTS. This leads us to introduce a different class of systems,
incomparable to branch-WSTS, which we call _cover-WSTS_. These systems relax
the condition of monotony to only states within the coverability set, while
still retaining the decidability of a restricted form of coverability.

As future work, other systems that belong to these classes can be studied.
Moreover, it would be interesting to precisely characterise the systems for
which we can decide non-termination and boundedness along a single run. It
would also be interesting to see if the branch-WSTS relaxation translates to
better hope for usability of WSTS and relaxations as a verification technique.

#### Acknowledgements

We thank the reviewers for the detailed comments and suggestions. The work
reported was carried out in the framework of ReLaX, UMI2000 (ENS Paris-Saclay,
CNRS, Univ. Bordeaux, CMI, IMSc). It is partly supported by ANR FREDDA
(ANR-17-CE40-0013) and ANR BRAVAS (ANR-17-CE40-0028). It is also partly
supported by UKRI/EPSRC, references: EP/T006544/2, and EU HORIZON EUROPE
Research and Innovation Programme, grant agreement 101093006 (TaRDIS).

## References

  * [ACJT00] Parosh Aziz Abdulla, Kārlis Cerāns, Bengt Jonsson, and Yih-Kuen Tsay.  Algorithmic Analysis of Programs with Well Quasi-ordered Domains.  Information and Computation, 160(1):109–127, July 2000.
  * [BFM17] Michael Blondin, Alain Finkel, and Pierre McKenzie.  Well Behaved Transition Systems.  Log. Methods Comput. Sci., 13(3), 2017.
  * [BFM18] Michael Blondin, Alain Finkel, and Pierre McKenzie.  Handling infinitely branching well-structured transition systems.  Information and Computation, 258:28–49, February 2018.
  * [BFS20] Benedikt Bollig, Alain Finkel, and Amrita Suresh.  Bounded Reachability Problems Are Decidable in FIFO Machines.  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 49:1–49:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [BS13] N. Bertrand and P. Schnoebelen.  Computable fixpoints in well-structured symbolic model checking.  Formal Methods in System Design, 43(2):233–267, October 2013.
  * [BZ83] Daniel Brand and Pitro Zafiropulo.  On communicating finite-state machines.  Journal of the ACM (JACM), 30(2):323–342, 1983.  Publisher: ACM.
  * [DFS98] C. Dufourd, A. Finkel, and Ph. Schnoebelen.  Reset nets between decidability and undecidability.  In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, Lecture Notes in Computer Science, pages 103–115, Berlin, Heidelberg, 1998. Springer.
  * [Dic13] Leonard Eugene Dickson.  Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors.  American Journal of Mathematics, 35(4):413–422, 1913.  Publisher: Johns Hopkins University Press.
  * [DS20] Emanuele D’Osualdo and Felix Stutz.  Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions.  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 31:1–31:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [ER56] P. Erdös and R. Rado.  A partition calculus in set theory.  Bulletin of the American Mathematical Society, 62(5):427–489, 1956\.
  * [FG19] Alain Finkel and Ekanshdeep Gupta.  The Well Structured Problem for Presburger Counter Machines.  In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), volume 150 of Leibniz International Proceedings in Informatics (LIPIcs), pages 41:1–41:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  ISSN: 1868-8969.
  * [Fin87] Alain Finkel.  A Generalization of the Procedure of Karp and Miller to Well Structured Transition Systems.  In Thomas Ottmann, editor, Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings, volume 267 of Lecture Notes in Computer Science, pages 499–508. Springer, 1987.
  * [Fin90] Alain Finkel.  Reduction and covering of infinite reachability trees.  Inf. Comput., 89(2):144–179, 1990.
  * [FMP04] Alain Finkel, Pierre McKenzie, and Claudine Picaronny.  A well-structured framework for analysing petri net extensions.  Information and Computation, 195(1):1–29, November 2004.
  * [FP20] Alain Finkel and M. Praveen.  Verification of Flat FIFO Systems.  Logical Methods in Computer Science, 20(4), October 2020.
  * [FS01] Alain Finkel and Philippe Schnoebelen.  Well-structured transition systems everywhere!  Theor. Comput. Sci., 256(1-2):63–92, 2001.
  * [Hig52] Graham Higman.  Ordering by Divisibility in Abstract Algebras.  Proceedings of The London Mathematical Society, pages 326–336, 1952\.
  * [KSS04] E.V. Kouzmin, N.V. Shilov, and V.A. Sokolov.  Model checking /spl mu/-calculus in well-structured transition systems.  In Proceedings. 11th International Symposium on Temporal Representation and Reasoning, 2004. TIME 2004., pages 152–155, July 2004\.  ISSN: 1550-1311.
  * [LS15] Ranko Lazić and Sylvain Schmitz.  Nonelementary Complexities for Branching VASS, MELL, and Extensions.  ACM Transactions on Computational Logic, 16(3):20:1–20:30, June 2015.
  * [Sch21] Sylvain Schmitz.  Branching in Well-Structured Transition Systems (Invited Talk).  In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1–3:3, Dagstuhl, Germany, 2021. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  ISSN: 1868-8969.
  * [SG07] N. V. Shilov and N. O. Garanina.  Well-Structured Model Checking of Multiagent Systems.  In Irina Virbitskaite and Andrei Voronkov, editors, Perspectives of Systems Informatics, Lecture Notes in Computer Science, pages 363–376, Berlin, Heidelberg, 2007. Springer.
  * [SS12] Sylvain Schmitz and Philippe Schnoebelen.  Algorithmic Aspects of WQO Theory.  Lecture Notes, August 2012.
  * [ZWH12] Damien Zufferey, Thomas Wies, and Thomas A. Henzinger.  Ideal Abstractions for Well-Structured Transition Systems.  In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, pages 445–460, Berlin, Heidelberg, 2012. Springer.
  * [Öz22] Okan Özkan.  Decidability of Resilience for Well-Structured Graph Transformation Systems.  In Nicolas Behr and Daniel Strüber, editors, Graph Transformation, Lecture Notes in Computer Science, pages 38–57, Cham, 2022. Springer International Publishing.