18119 LABEL:LastPageMay 17, 2021Jan. 20, 2022 MnLargeSymbols’164
MnLargeSymbols’171

# Bounded Reachability Problems are Decidable
in FIFO Machines

Benedikt Bolliga  ,  Alain Finkela,b  and  Amrita Suresha  Université Paris-
Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France
<EMAIL_ADDRESS>Institut
Universitaire de France

###### Abstract.

The undecidability of basic decision problems for general FIFO machines such
as reachability and unboundedness is well-known. In this paper, we provide an
underapproximation for the general model by considering only runs that are
input-bounded (i.e. the sequence of messages sent through a particular channel
belongs to a given bounded language). We prove, by reducing this model to a
counter machine with restricted zero tests, that the rational-reachability
problem (and by extension, control-state reachability, unboundedness,
deadlock, etc.) is decidable. This class of machines subsumes input-letter-
bounded machines, flat machines, linear FIFO nets, and monogeneous machines,
for which some of these problems were already shown to be decidable. These
theoretical results can form the foundations to build a tool to verify general
FIFO machines based on the analysis of input-bounded machines.

###### Key words and phrases:

FIFO machines, reachability, underapproximation, counter machines

##  1\. Introduction

Context. Asynchronous distributed processes communicating using First In First
Out (FIFO) channels are being widely used for distributed and concurrent
programming, and more recently, for web service choreographies. Since systems
of processes communicating through (at least two) one-directional FIFO
channels, or equivalently, machines having a unique control-structure with a
single FIFO channel (acting as a buffer) simulate Turing machines, most
properties, such as unboundedness of a channel, are undecidable for such
systems [VF80, BZ83, MF85].

#### Reachability in FIFO machines.

If one restricts to runs with $B$-bounded channels (the number of messages in
every channel does not exceed $B$), then reachability becomes decidable for
existentially-bounded and universally-bounded FIFO systems [GKM07]. When
limiting the number of phases, the bounded-context reachability problem is in
$2$-EXPTIME, even for recursive FIFO systems [LMP08, HLMS10]. For non-
confluent topology, reachability is in EXPTIME for recursive FIFO systems with
$1$-bounded channels [HLMS10]. The notion of $k$-synchronous computations was
introduced in [BEJQ18]. Reachability under this restriction and checking
$k$-synchronizability are both PSPACE-complete [GLL20]. Reachability is in
PTIME in half-duplex systems [CF05] with two processes (moreover, the
reachability set is recognizable and effectively computable), but the natural
extension to three processes leads to undecidability. Lossy FIFO systems
(where the channels can lose messages) [ACBJ04, Fin94] have been shown to be
well-structured and have a decidable (but non-elementary) reachability problem
[CS08]. In [MP11, AGK14], uniform criteria for decidability of reachability
and model-checking questions are established for communicating recursive
systems whose restricted architecture or communication mechanism gives rise to
behaviours of bounded tree-width.

#### Input-bounded FIFO machines.

Many papers, starting in the 80s until today, have studied FIFO machines in
which the input-language of a channel (i.e. the set of words that record the
messages entering a channel) is included in the set
$\mathit{Pref}(w_{1}^{*}w_{2}^{*}\ldots w_{n}^{*})$ of prefixes of a bounded
language $w_{1}^{*}w_{2}^{*}\ldots w_{n}^{*}$. We call this class of FIFO
machines _input-bounded_.

If the _set of letters_ that may enter a channel $c$ is reduced to a unique
letter $a_{c}$, then the input-language of $c$ is included in $a_{c}^{*}$ and
this subclass trivially reduces to VASS and Petri nets [YG83]. Also note that,
in general, the behaviour of those FIFO machines does not have bounded tree-
width. _Monogeneous_ FIFO nets [Fin82, MF85, FS01] (input-languages of
channels $c$ are included in $\mathit{Pref}(u_{c}v_{c}^{*})$ where
$u_{c},v_{c}$ are two words associated with $c$) and _linear_ FIFO nets [FC87]
(input-languages are included in $\mathit{Pref}(a_{1}^{*}a_{2}^{*}\ldots
a_{n}^{*})$ where each $a_{i}$ is a letter and $a_{i}\neq a_{j}$ iff $i\neq
j$) both generalize Petri nets with still a decidable reachability problem. A
variant of the reachability problem, the deadlock problem, is shown decidable
for input-_letter_ -bounded FIFO systems in [GGLR87] by reducing to
reachability for VASS, but the extension to general input-bounded machines was
left open.

_Flat_ machines are another subclass of input-bounded machines in which the
language of their control-graph, considered as a finite automaton, is a
bounded language. For flat FIFO machines, control-state reachability is NP-
complete [EGM12]; this result has recently been extended to reachability,
channel unboundedness, and other classical properties [FP19].

To the best of our knowledge, the decidability status of control-state
reachability, reachability, deadlock, and termination was not known for input-
bounded FIFO machines, which strictly include all the classes discussed above
such as flat, input-letter-bounded, monogeneous, and linear FIFO machines (the
last three types contain VASS and they are all incomparable). The
unboundedness problem of input-bounded FIFO machines was shown decidable in
[JJ93] by using the well-structured concepts but with no extension to
decidability of reachability.

#### Contributions

Our contributions can be summarized as follows:

  * •

We solve a problem that was left open in [GGLR87], the decidability of the
reachability problem for input-bounded FIFO machines. We present a simulation
of input-bounded FIFO machines by counter machines with restricted zero tests.
The main idea is to associate a counter with each word in the bounded
language, and to ensure that the counters are incremented and decremented in a
way that corresponds to the FIFO order. Since we can have repeated letters,
and ambiguities in the FIFO machine, we first need to construct a normal form
of the FIFO machine. Furthermore, we ensure that for every run in the FIFO
machine, we can construct an equivalent run in the counter machine and vice-
versa.

  * •

As we actually solve the general rational-reachability problem, we can deduce
the decidability of other verification properties like control-state
reachability, deadlock, unboundedness, and termination.

  * •

We unify various definitions from the literature, survey the (not well-known)
results, and generalize them.

  * •

We study the natural dual of the input-bounded reachability problem, which are
systems of output-bounded languages in which the set of words received by each
channel is constrained to be bounded, and are able to deduce the reachability,
unboundedness, termination and control-state reachability for the same.

  * •

We obtain better upper bounds for the input-bounded reachability of FIFO
machines with a single channel (reachability is still undecidable for FIFO
machines with a single channel). This is done by reducing it to reachability
in _unary ordered multi-pushdown systems_ (a class that was previously
analyzed in [ABH17]). It is, hence, solvable in EXPTIME.

  * •

Following the bounded verification paradigm, applied to FIFO machines (for
instance in [EGM12, FP19]), we open the way to a methodology that would apply
existing results on input-bounded FIFO machines to general FIFO machines.

#### Plan

In Section 2, we present counter and FIFO machines, with the connection-
deconnection protocol as an example. Section 3 contains the main result, which
states the decidability of rational-reachability for FIFO machines restricted
to input-bounded languages. Sections 4 and 5 consider variants of the rational
reachability problem such as deadlock, unboundedness and termination. In
Section 6, we consider the output-bounded reachability problem, and other
variants such as boundedness and termination. We look at the input-bounded
problems FIFO machines with a single channel, and obtain some lower bounds in
Section 7. Finally, in Section 8, we mention further results, state some open
problems, and discuss a possible theory of boundable FIFO machines.

A preliminary version of this work has been presented at the 31st
International Conference on Concurrency Theory (CONCUR ’20). Our contributions
extend the conference version as follows:

This work additionally considers the symmetric case of output-bounded
languages in which the set of words received by each channel is constrained to
be bounded. We are able to deduce the reachability, unboundedness, termination
and control-state reachability for the same. It also studies the special case
of input-bounded FIFO machines with a single channel (reachability is still
undecidable for general FIFO machines with a single channel). This is done by
reducing it to reachability in unary ordered multi-pushdown systems (a class
that was previously analyzed). It is, hence, solvable in EXPTIME. We also
expand on the proof idea for boundedness and termination for input-bounded
FIFO machines, and provide the explicit construction for the decidability of
the same.

##  2\. Preliminaries

### Words and Languages.

Let $A$ be a finite alphabet. As usual, $A^{\ast}$ is the set of finite words
over $A$, and $A^{+}$ the set of non-empty finite words. We let $|w|$ denote
the length of $w\in A^{\ast}$. For the empty word $\varepsilon$, we have
$|\varepsilon|=0$. Given $a\in A$, let $|w|_{a}$ denote the number of
occurrences of $a$ in $w$. With this, we let $\mathit{Alph}(w)=\\{a\in
A\mid|w|_{a}\geq 1\\}$. The concatenation of two words $u,v\in A^{\ast}$ is
denoted by $u\cdot v$ or $u.v$ or simply $uv$. The sets of prefixes, suffixes,
and infixes of $w\in A^{\ast}$ are denoted by $\mathit{Pref}(w)$,
$\mathit{Suf}(w)$, and $\mathit{Infix}(w)$, resp. Note that
$\\{\varepsilon,w\\}\subseteq\mathit{Pref}(w)\cap\mathit{Suf}(w)\cap\mathit{Infix}(w)$.
For a set $X$, any mapping $f:A^{\ast}\to 2^{X}$ can be extended to
$f:2^{A^{\ast}}\to 2^{X}$ letting, for $L\subseteq A^{\ast}$,
$f(L)=\bigcup_{w\in L}f(w)$. In particular, $\mathit{Alph}$, $\mathit{Pref}$,
$\mathit{Suf}$, and $\mathit{Infix}$ are extended in that way.

[[GS64]] Let $w_{1},\ldots,w_{n}\in A^{+}$ be non-empty words where $n\geq 1$.
A _bounded language_ over $(w_{1},\ldots,w_{n})$ is a language $L\subseteq
w_{1}^{\ast}\ldots w_{n}^{\ast}$.

We always assume that a bounded language $L$ is given together with its tuple
$(w_{1},\ldots,w_{n})$ and that $\mathit{Alph}(L)=\mathit{Alph}(w_{1}\ldots
w_{n})$. We say that $L$ is _distinct-letter_ if $|w_{1}\ldots w_{n}|_{a}\leq
1$ for all $a\in A$. If $|w_{1}|=\cdots=|w_{n}|=1$, i.e.
$w_{1},\ldots,w_{n}\in A$, then $L$ is a _letter-bounded language._ Let us
remark that the set of bounded languages is closed under $\mathit{Pref}$ and
$\mathit{Suf}$.

### Semi-Linear Sets.

A _linear_ set $X$ (of dimension $d\geq 1$) is defined as a subset of
$\mathbb{N}^{d}$ for which there exist a basis $\mathbf{b}\in\mathbb{N}^{d}$
and a finite set of periods
$\\{\mathbf{p}_{1},\ldots,\mathbf{p}_{m}\\}\subseteq\mathbb{N}^{d}$ such that
$X=\\{\mathbf{b}+\sum_{i=1}^{m}\lambda_{i}\mathbf{p}_{i}\mid\lambda_{1},\ldots,\lambda_{m}\in\mathbb{N}\\}$.
A _semi-linear_ set is defined as a finite union of linear sets.

### Transition Systems.

A _labeled transition system_ is a quadruple
$\mathcal{T}=(S,A,\to,\mathit{init})$ where $S$ is the (potentially infinite)
set of _configurations_ 111We say _configurations_ rather than _states_ to
distinguish them from the _control states_ used in FIFO and counter machines.,
$A$ is a finite alphabet, $\mathit{init}\in S$ is the _initial configuration_
, and ${\to}\subseteq S\times A\times S$ is the _transition relation_.

For $s,s^{\prime}\in S$, let $s\to s^{\prime}$ if $s\xrightarrow{a}s^{\prime}$
for some $a\in A$. For $w\in A^{\ast}$, we write $s\xrightarrow{w}s^{\prime}$
if there is a $w$-labeled path from $s$ to $s^{\prime}$. Formally,
$s\xrightarrow{\varepsilon}s^{\prime}$ if $s=s^{\prime}$, and
$s\xrightarrow{aw}s^{\prime}$ if there is $t\in S$ such that
$s\xrightarrow{a}t$ and $t\xrightarrow{w}s^{\prime}$. We let
$\mathit{Traces}(\mathcal{T})=\\{w\in
A^{\ast}\mid\mathit{init}\xrightarrow{w}s$ for some $s\in S\\}$.

Given $w\in A^{\ast}$, we let $\mathit{Reach}_{\mathcal{T}}(w)=\\{s\in
S\mid\mathit{init}\xrightarrow{w}s\\}$. Moreover, for $L\subseteq A^{\ast}$,
$\mathit{Reach}_{\mathcal{T}}(L)=\bigcup_{w\in
L}\mathit{Reach}_{\mathcal{T}}(w)$ is the set of configurations that are
reachable via a word from $L$. Finally, the _reachability set_ of
$\mathcal{T}$ is defined as
$\textit{Reach}_{\mathcal{T}}=\mathit{Reach}_{\mathcal{T}}(A^{\ast})$. We call
$\mathcal{T}$ _finite_ if $\textit{Reach}_{\mathcal{T}}$ is finite (and this
is the case if $S$ is finite). Otherwise, $\mathcal{T}$ is called _infinite_.

### FIFO Machines.

We consider FIFO machines having a sequential control graph rather than
systems of communicating processes that are distributed systems. It is clear
that, given a distributed system, one may compute the Cartesian product of all
processes to obtain a FIFO machine (the converse is not always true).

A _FIFO machine_ is a tuple ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ where $Q$ is
a finite set of _control states_ , $q_{0}\in Q$ is an _initial control state_
, and $\mathit{Ch}$ is a finite set of _channels_. Moreover, $\Sigma$ is a
finite _message alphabet_. It is partitioned into
$\Sigma=\biguplus_{c\in\mathit{Ch}}\Sigma_{c}$ where $\Sigma_{c}$ contains the
messages that can be sent through channel $c$. Finally, $T\subseteq Q\times
A_{{M}}\times Q$ is a _transition relation_ where $A_{{M}}=\\{\langle
c!a\rangle\mid c\in\mathit{Ch}$ and $a\in\Sigma_{c}\\}\cup\\{\langle
c?a\rangle\mid c\in\mathit{Ch}$ and $a\in\Sigma_{c}\\}$ is the set of send and
receive actions.

[Connection-Deconnection Protocol] A model for the (simplified) connection-
deconnection protocol, CDP, between two processes is described as follows (see
Figure 1): We model the protocol with two automata (representing the two
processes) and two (infinite) channels. The first processes (on the left) can
open a session (this is denoted by sending the message “$a$” through channel
$c_{1}$ to the other process). Once a session is open, the first process can
close it (by sending message “$b$” to the other process), or on the demand of
the second process (if it receives the message “$e$”). This protocol has been
studied in [Jér91].

In the example, it is natural to have two separate processes. However,
following Definition 2, we formalize this in terms of the Cartesian product of
the two processes. That is, the CDP is modeled as the FIFO machine
${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ where $Q=\\{0,1\\}\times\\{0,1\\}$ (the
Cartesian product of the local state spaces) with initial state $q_{0}=(0,0)$,
$\mathit{Ch}=\\{c_{1},c_{2}\\}$, $\Sigma=\Sigma_{c_{1}}\uplus\Sigma_{c_{2}}$
with $\Sigma_{c_{1}}=\\{a,b\\}$ and $\Sigma_{c_{2}}=\\{e\\}$. Moreover, the
transition relation $T$ contains, amongst others, $((0,0),\langle
c_{1}!a\rangle,(1,0))$ and $((1,0),\langle c_{1}?a\rangle,(1,1))$. $\lhd$

$0$$1$$c_{1}$$c_{2}$$0$$1$$\langle c_{1}!a\rangle$$\langle
c_{1}!b\rangle$$\langle c_{2}?e\rangle$$\langle c_{1}?a\rangle$$\langle
c_{1}?b\rangle$$\langle c_{2}!e\rangle$ Figure 1. The model of the connection-
deconnection protocol

A FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ induces a (potentially
infinite) transition system
$\mathcal{T}_{{M}}=(S_{M},A_{{M}},\to_{M},\mathit{init}_{M})$. Its set of
configurations is $S_{M}=Q\times\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$. In
$(q,\mathbf{w})\in S_{M}$, the first component $q$ denotes the current control
state and $\mathbf{w}=(\mathbf{w}_{c})_{c\in\mathit{Ch}}$ determines the
contents $\mathbf{w}_{c}\in\Sigma_{c}^{\ast}$ for every channel
$c\in\mathit{Ch}$. The initial configuration is
$\mathit{init}_{M}=(q_{0},\bm{\varepsilon})$ where
$\bm{\varepsilon}=(\varepsilon,\ldots,\varepsilon)$, i.e., every channel is
empty. The transitions are given as follows:

  * •

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

  * •

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

The index ${M}$ may be omitted whenever ${M}$ is clear from the context.

The _reachability set_ of ${M}$ is defined as the reachability set of
$\mathcal{T}_{{M}}$, i.e.,
$\textit{Reach}_{{M}}=\textit{Reach}_{\mathcal{T}_{{M}}}$ and, for $L\subseteq
A_{{M}}^{\ast}$,
$\mathit{Reach}_{{M}}(L)=\mathit{Reach}_{\mathcal{T}_{{M}}}(L)$. Moreover, we
let $\mathit{Traces}({M})=\mathit{Traces}(\mathcal{T}_{{M}})$.

An example run of the FIFO machine ${M}$ from Example 2 and Figure 1 is
$((0,0),(\varepsilon,\varepsilon))\xrightarrow{\langle
c_{1}!a\rangle}((1,0),(a,\varepsilon))\xrightarrow{\langle
c_{1}?a\rangle}((1,1),(\varepsilon,\varepsilon))\xrightarrow{\langle
c_{2}!e\rangle}((1,0),(\varepsilon,e))$. As for the reachability set, we have,
e.g., $((1,1),((ba)^{\ast},\varepsilon)))\subseteq\textit{Reach}_{{{M}}}$ and
$((0,0),(b(ab)^{\ast},e))\subseteq\textit{Reach}_{{{M}}}$. Let us remark that
CDP is not half-duplex because there are reachable configurations with both
channels non-empty, e.g., $((0,0),(b,e))$; moreover, it is neither
monogeneous, nor linear, nor input-letter-bounded. $\lhd$

### Counter Machines.

We next recall the notion of counter machines, where multiple counters can
take non-negative integer values, be incremented and decremented, and be
tested for zero (though in a restricted fashion).

A _counter machine_ (with zero tests) is a tuple
$\mathcal{C}=(Q,\mathit{Cnt},T,q_{0})$. Like in a FIFO machine, $Q$ is the
finite set of _control states_ and $q_{0}\in Q$ is the _initial control
state_. Moreover, $\mathit{Cnt}$ is a finite set of _counters_ and $T\subseteq
Q\times A_{\mathcal{C}}\times Q$ is the transition relation where
$A_{\mathcal{C}}=\\{\mathsf{inc}(x),\mathsf{dec}(x)\mid
x\in\mathit{Cnt}\\}\times 2^{\mathit{Cnt}}$.

The counter machine $\mathcal{C}$ induces a transition system
$\mathcal{T}_{\mathcal{C}}=(S_{\mathcal{C}},A_{\mathcal{C}},\to_{\mathcal{C}},\mathit{init}_{\mathcal{C}})$
with set of configurations $S_{\mathcal{C}}=Q\times\mathbb{N}^{\mathit{Cnt}}$.
In $(q,\mathbf{v})\in S_{\mathcal{C}}$, $q$ is the current control state and
$\mathbf{v}=(\mathbf{v}_{x})_{x\in\mathit{Cnt}}$ represents the counter
values. The initial configuration is
$\mathit{init}_{\mathcal{C}}=(q_{0},\bm{0})$ where $\bm{0}$ maps all counters
to $0$. For $\mathit{op}\in\\{\mathsf{inc},\mathsf{dec}\\}$,
$x\in\mathit{Cnt}$, and $Z\subseteq\mathit{Cnt}$ (the counters tested for
zero), there is a transition
$(q,\mathbf{v})\xrightarrow{(\mathit{op}(x),Z)}_{\mathcal{C}}(q^{\prime},\mathbf{v}^{\prime})$
if $(q,(\mathit{op}(x),Z),q^{\prime})\in T$, $\mathbf{v}_{y}=0$ for all $y\in
Z$ (applies the zero tests), $\mathbf{v}_{x}^{\prime}=\mathbf{v}_{x}+1$ if
$\mathit{op}=\mathsf{inc}$ and $\mathbf{v}_{x}^{\prime}=\mathbf{v}_{x}-1$ if
$\mathit{op}=\mathsf{dec}$, and $\mathbf{v}_{y}^{\prime}=\mathbf{v}_{y}$ for
all $y\in\mathit{Cnt}\setminus\\{x\\}$.

The _reachability set_ of $\mathcal{C}$ is defined as
$\textit{Reach}_{\mathcal{C}}=\textit{Reach}_{\mathcal{T}_{\mathcal{C}}}$. For
$L\subseteq A_{\mathcal{C}}^{\ast}$, we also let
$\mathit{Reach}_{\mathcal{C}}(L)=\mathit{Reach}_{\mathcal{T}_{\mathcal{C}}}(L)$.
Moreover,
$\mathit{Traces}(\mathcal{C})=\mathit{Traces}(\mathcal{T}_{\mathcal{C}})$. To
get decidability of reachability in counter machines, we impose the
restriction that, once a counter has been tested for zero, it cannot be
incremented or decremented anymore. This is clearly an extension of VASS. To
define this, let $\smash{L_{\mathcal{C}}^{\textsf{{zero}}}}$ be the set of
words $(\mathit{op}_{1}(x_{1}),Z_{1})\ldots(\mathit{op}_{n}(x_{n}),Z_{n})\in
A_{\mathcal{C}}^{\ast}$ such that, for every two positions $1\leq i\leq j\leq
n$, we have $x_{j}\not\in Z_{i}$.

######  Theorem 1.

The following problem is decidable (though inherently non-elementary): Given a
counter machine $\mathcal{C}=(Q,\mathit{Cnt},T,q_{0})$, a regular language
$L\subseteq A_{\mathcal{C}}^{\ast}$, a control state $q\in Q$, and a semi-
linear set $V\subseteq\mathbb{N}^{\mathit{Cnt}}$, do we have
$(q,\mathbf{v})\in\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap
L)$ for some $\mathbf{v}\in V$?

######  Proof 2.1 (Proof sketch).

Reachability in presence of a semi-linear target set and restricted zero tests
straightforwardly reduces to configuration-reachability in counter machines
without zero tests (i.e., VASS and Petri nets). The latter is decidable
[May84], though inherently non-elementary [CLL+19]. First, zero tests are
postponed to the very end of an execution and, to this aim, stored in the
control-state. Second, to check whether a counter valuation is contained in
$V$, we can branch, whenever we are in the given control-state $q$, into a new
component that decrements counters accordingly and eventually checks whether
they are all zero.

##  3\. The Input-Bounded Rational-Reachability Problem

It is very well known that the following reachability problem is undecidable:
Given a FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a configuration
$(q,\mathbf{w})\in S_{M}$, and a regular language $L\subseteq A_{{M}}^{\ast}$,
do we have $(q,\mathbf{w})\in\mathit{Reach}_{{M}}(L)$? Of course, the problem
is already undecidable when we impose $L=A_{{M}}^{\ast}$. Motivated by this
negative result, we are looking for language classes $\mathfrak{C}$ that
render the problem decidable under the restriction that $L\in\mathfrak{C}$.

We say that a FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ has a _bounded
reachability set_ if there is a tuple $(L_{c})_{c\in\mathit{Ch}}$ of regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$ such that, for all
$(q,\mathbf{w})\in\textit{Reach}_{{M}}$, we have
$\mathbf{w}\in\prod_{c\in\mathit{Ch}}L_{c}$. We observe that restricting the
reachability set to be bounded is not sufficient to obtain a decidable
reachability problem. We show this by simulating any two counter Minsky
machine by a FIFO machine with fixed languages $L_{c}$.

######  Theorem 2.

The reachability problem is undecidable for FIFO machines with a (given)
bounded reachability set.

######  Proof 3.1.

We prove this by simulating a (two) counter Minsky machine by a FIFO machine
with a bounded reachability set. Intuitively, if the two counters have values
$x_{1}$ and $x_{2}$ at a state $q$, the FIFO machine is at state $q$ with
channel contents $\$a^{x_{1}}\\#b^{x_{2}}\&$.

Consider a Minsky machine $\mathcal{C}=(Q,\mathit{Cnt},T,q_{0})$, where $Q$ is
the set of states, $\mathit{Cnt}=\\{x_{1},x_{2}\\}$ is the set of counters,
$q_{0}$ the initial state, and $T=\\{\delta_{1},\ldots,\delta_{n}\\}$ is the
set of transition rules, which can be of two types from any state $\hat{q}\in
Q$:

  * •

$\delta_{i}:x_{j}:=x_{j}+1;\texttt{ goto }q;$

  * •

$\delta_{i}:\texttt{if }x_{j}>0\texttt{ then }(x_{j}:=x_{j}-1;\texttt{ goto
}q)\texttt{ else}\texttt{ goto }q^{\prime};$

for $j=\\{1,2\\}$ and $q,q^{\prime}\in Q$.

We can construct a FIFO machine ${M}=(Q^{\prime},\mathit{Ch},\Sigma,T,q_{0})$
with a bounded reachability set as follows: $Q^{\prime}=Q\uplus
Q^{\prime\prime}$, where $Q^{\prime\prime}$ is a set of intermediate states;
$\Sigma=\\{a,b,\\#,\$,\&\\}$. There is a single channel, hence
$|\mathit{Ch}|=1$. We consider the language
$L=\$^{*}a^{*}\\#^{*}b^{*}\&^{*}\$^{*}a^{*}\\#^{*}b^{*}\&^{*}$, and we start
with queue contents as $\$\\#\&$, where the letters $\\#,\$,\&$ are used as
markers during the test for zero. The number of occurrences of the letter $a$
(resp. $b$) corresponds to the counter valuations for $x_{1}$ (resp. $x_{2}$)
in the configurations of the Minsky machine, and we rotate the tape contents
in such a way that the contents always belong to $L$. For every state
$q^{\prime\prime}\in Q$ and every transition from it with the rule
$\delta_{i}:x_{1}:=x_{1}+1;\texttt{ goto }q;$ for some $q\in Q$, we create the
following transition sequence. We ensure that we read the markers, and add an
additional letter $a$ to the channel. We see that at every intermediate
configuration, the channel contents still belongs to $L$.

$q^{\prime\prime}$$q$$?\$.!\$$$?a$$!a$$?\\#$$!a$$!\\#$$?b$$!b$$?\&.!\&$ Figure
2. Incrementing $x_{1}$

Likewise, a transition of the form

$\delta_{i}:\texttt{if }x_{1}>0\texttt{ then }(x_{1}:=x_{1}-1;\texttt{ goto
}q)$ $\texttt{ else}\texttt{ goto }q^{\prime};$

can be constructed as show in Figure 3. Here, in the first case ($x_{1}>0$) we
ensure that at least one letter $a$ is read from the channel contents, and
rewrite the rest of the contents as is. If $x_{1}=0$, then we read only the
end markers (and letters $b$, if any) and rewrite them once again.

$q^{\prime\prime}$$q$$q^{\prime}$$?\$!\$$$?a$$?a$$!a$$?\\#$$!\\#$$?b$$!b$$?\&.!\&$$?\\#.!\\#$$?b$$!b$$?\&.!\&$
Figure 3. Decrementing $x_{1}$

Similar constructions can be made for all transitions, and the queue contents
are always contained in
$\$^{*}a^{*}\\#^{*}b^{*}\&^{*}\$^{*}a^{*}\\#^{*}b^{*}\&^{*}$. Hence, the
reachability set of the FIFO machine is letter-bounded (but it is not
distinct-letter).

######  Remark 3.

We see, in the previous proof, that the input language of the above machine is
not bounded: If we have a transition from $q$ in the original machine of the
kind $\delta_{i}:x_{j}:=x_{j}+1;\texttt{ goto }q;$ (a loop), the input
language of the machine would be $(\$^{*}a^{*}\\#b^{*}\&)^{*}$ for this
transition, which is not bounded. Furthermore, the machine is not flat either,
since there can be control states that are in more than one elementary loop.

We therefore consider a different restriction to obtain decidability. For a
given FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, we are interested in
$\mathit{Reach}_{{M}}(L)$ where $L\subseteq A_{{M}}^{\ast}$ is _input-bounded_
in the following sense: For every channel $c$, the sequence of messages that
are sent through channel $c$ is from a given regular bounded language
$L_{c}\subseteq\Sigma_{c}^{\ast}$.

Let us be more formal. For $c\in\mathit{Ch}$, we let
$\mathit{proj}_{c!}:A_{{M}}^{\ast}\to\Sigma_{c}^{\ast}$ be the homomorphism
defined by $\mathit{proj}_{c!}(\langle c!a\rangle)=a$ for all
$a\in\Sigma_{c}$, and $\mathit{proj}_{c!}(\beta)=\varepsilon$ if $\beta\in
A_{{M}}$ is not of the form $\langle c!a\rangle$ for some $a\in\Sigma_{c}$. We
define $\mathit{proj}_{c?}:A_{{M}}^{\ast}\to\Sigma_{c}^{\ast}$ accordingly.

With this, given a tuple $\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$
of bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$, we set
$\mathord{\operatorname{\text{L}}_{!}}=\\{\sigma\in
A_{{M}}^{\ast}\mid\mathit{proj}_{c!}(\sigma)\in L_{c}$ for all
$c\in\mathit{Ch}\\}$ and $\operatorname{\text{L}}_{?}=\\{\sigma\in
A_{{M}}^{\ast}\mid\mathit{proj}_{c?}(\sigma)\in L_{c}$ for all
$c\in\mathit{Ch}\\}$. We observe that, if all $L_{c}$ are regular, then so are
$\mathord{\operatorname{\text{L}}_{!}}$ and
$\mathord{\operatorname{\text{L}}_{?}}$.

The _input-bounded (IB) reachability problem_ asks whether a given
configuration $(q,\mathbf{w})$ is reachable along a sequence of actions from
$\mathord{\operatorname{\text{L}}_{!}}$, i.e., whether
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$.

Note that, if $(q_{0},\bm{\varepsilon})\xrightarrow{\sigma}_{M}(q,\mathbf{w})$
and $\sigma\in\mathord{\operatorname{\text{L}}_{!}}$, then we also have
$\sigma\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$ due to the
FIFO policy. Thus,
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})=\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}}))$
so that we can restrict to action sequences from
$\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$.
We will call
$\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$
the set of _valid_ words.

Let us come back to the protocol CDP ${M}$ from Example 2 and Figure 1, which
is neither monogeneous nor linear nor flat. Since the “input-languages” of the
two channels (i.e. the languages of words that record the messages entering a
channel) contain $\\{a,ab\\}^{*}$ and $e^{\ast}$, resp., and since
$\\{a,ab\\}^{*}$ is not a bounded language, we have
$\mathit{Traces}({M})\not\subseteq\mathord{\operatorname{\text{L}}_{!}}$ for
every pair of bounded languages $\operatorname{\text{L}}$. In other words,
${M}$ is not input-bounded. However, when we look at the reachability set
obtained by considering the tuple of bounded languages
$\operatorname{\text{L}}=(L_{c_{1}},L_{c_{2}})$ where
$L_{c_{1}}=(ab)^{*}(a+\varepsilon)(ab)^{*}$ is a bounded language over
$(ab,a,ab)$, and $L_{c_{2}}=e^{\ast}$ is a bounded language over $(e)$, we
still obtain the entire reachability set. That is, we have
$\textit{Reach}_{{M}}=\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$.
Hence, even though the input-languages of the system are not all bounded, we
can still compute the reachability set by restricting our exploration to a
tuple of (regular) bounded languages $\operatorname{\text{L}}$. $\lhd$

Actually, instead of reachability of a single configuration as stated in
Definition 3, we study a more general problem, called the _input-bounded
rational-reachability problem_. It asks whether a configuration
$(q,\mathbf{w})$ is reachable for some channel contents $\mathbf{w}$ from a
given _rational_ relation. So let us define rational relations.

### Rational and Recognizable Relations.

Consider a relation
$\text{R}\subseteq\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$. We say that R is
_rational_ if there is a regular word language $R\subseteq\Theta^{\ast}$ over
the alphabet $\Theta=\prod_{c\in\mathit{Ch}}(\Sigma_{c}\cup\\{\varepsilon\\})$
such that
$\text{R}=\\{{(\mathbf{a}_{c}^{1}\cdot\cdots\cdot\mathbf{a}_{c}^{n})}_{c\in\mathit{Ch}}\mid\mathbf{a}^{1}\cdots\mathbf{a}^{n}\in
R$ with $n\in\mathbb{N}$ and
$\mathbf{a}^{i}={(\mathbf{a}^{i}_{c})}_{c\in\mathit{Ch}}\in\Theta$ for
$i\in\\{1,\ldots,n\\}\\}$. Here,
$\mathbf{a}_{c}^{1}\cdot\cdots\cdot\mathbf{a}_{c}^{n}\in\Sigma_{c}^{\ast}$ is
the concatenation of all
$\mathbf{a}_{c}^{i}\in\Sigma_{c}\cup\\{\varepsilon\\}$ while ignoring the
neutral element $\varepsilon$. For example, in the presence of two channels,
$\text{R}=\\{(a^{m},b^{n})\mid m\geq n\\}$ is a rational relation, witnessed
by $R=((a,b)+(a,\varepsilon))^{\ast}$. In the following, we will always assume
that a rational relation is given in terms of a finite automaton for the
underlying regular language $R$.

A relation $\text{R}\subseteq\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$ is
called _recognizable_ if it is the finite union of relations of the form
$\prod_{c\in\mathit{Ch}}R_{c}$ where all $R_{c}\subseteq\Sigma_{c}^{\ast}$ are
regular languages. Note that every recognizable relation is rational while the
converse is, in general, false.

We define the _Parikh image_ of a relation
$\text{R}\subseteq\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$ as
$\textup{Parikh}(\text{R})=\\{(\pi_{a})_{a\in\Sigma}\in\mathbb{N}^{\Sigma}\mid\exists\mathbf{w}=(\mathbf{w}_{c})_{c\in\mathit{Ch}}\in\text{R}:\pi_{a}=|\mathbf{w}_{c}|_{a}$
for all $c\in\mathit{Ch}$ and $a\in\Sigma_{c}\\}$. It is well known that, if R
is rational, then $\textup{Parikh}(\text{R})$ is semi-linear.

For more background on rational relations and their subclasses, we refer to
[Ber79, Cho06].

### The IB Rational-Reachability Problem.

We are now prepared to define the input-bounded (IB) rational-reachability
problem and to state its decidability:

The _IB rational-reachability problem_ is defined as follows: Given a FIFO
machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$ (each given in terms of a
finite automaton), a control state $q\in Q$, and a rational relation
$\text{R}\subseteq\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$. Do we have
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
for some $\mathbf{w}\in\text{R}$?

######  Theorem 4.

IB rational-reachability is decidable for FIFO machines.

The remainder of this section is devoted to the proof of Theorem 4.

Let ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ and let
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ be a tuple of non-empty
regular bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$ over
$(w_{c,1},\ldots,w_{c,n_{c}})$. We proceed by reduction to counter machines.
The rough idea is to represent the contents of channel $c$ in terms of several
counters, one for every component $w_{c,i}$. To have a faithful simulation, we
rely on a normal form of ${M}$ and its bounded languages, which can be
achieved at the expense of an exponential blow-up of the FIFO machine.

We say that ${M}$ and $\operatorname{\text{L}}$ are in _normal form_ if the
following hold:

  1. (1)

For all $c\in\mathit{Ch}$, $\Sigma_{c}\subseteq\mathit{Alph}(L_{c})$ and
$L_{c}$ is distinct-letter.

  2. (2)

We have $\mathit{Traces}((Q,A_{{M}},T,q_{0}))\subseteq\mathit{Pref}(\text{V})$
where
$\text{V}=\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$.
Note that $(Q,A_{{M}},T,q_{0})$ is the finite transition system induced by the
control graph of ${M}$.

Given a FIFO machine
$\hat{M}=(\hat{Q},\mathit{Ch},\hat{\Sigma},\hat{T},\hat{q}_{0})$ and the tuple
$\hat{\operatorname{\text{L}}}=(\hat{L}_{c})_{c\in\mathit{Ch}}$ of non-empty
regular bounded languages $\hat{L}_{c}\subseteq\hat{\Sigma}_{c}^{\ast}$, we
now construct ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ and
$\operatorname{\text{L}}={(L_{c})}_{c\in\mathit{Ch}}$ in normal form such that
a reachability query in the former can be transformed into a reachability
query in the latter (made precise in Lemma 5 below).

### Distinct-Letter Property.

Consider the bounded language $\hat{L}_{c}$ over
$(\hat{w}_{c,1},\ldots,\hat{w}_{c,n_{c}})$. For $i\in\\{1,\ldots,n_{c}\\}$,
let $m_{i}=|\hat{w}_{c,1}|+\ldots+|\hat{w}_{c,i}|$ be the number of letters in
the first $i$ words. Moreover, $m=m_{n_{c}}$. Let $\Sigma_{c}$ denote the
alphabet $\\{a_{1}^{c},\ldots,a_{m}^{c}\\}$. It contains the “distinct”
letters for the bounded language $L_{c}$ over $(w_{c,1},\ldots,w_{c,n_{c}})$,
where we let $w_{c,1}=a_{1}^{c}\ldots a_{m_{1}}^{c}$ and
$w_{c,i}=a_{m_{i-1}+1}^{c}\ldots a_{m_{i}}^{c}$ for $i\geq 2$. In other words,
the letters in $(w_{c,1},\ldots,w_{c,n_{c}})$ are numbered consecutively. In
order to obtain the language $L_{c}$, we first consider the homomorphism
$h_{c}:\Sigma_{c}^{\ast}\to\hat{\Sigma}_{c}^{\ast}$ where $h_{c}(a_{i}^{c})$
is the $i$-th letter in the word $\hat{w}_{c,1}\ldots\hat{w}_{c,n_{c}}$. We
obtain $L_{c}$ as
$h_{c}^{-1}(\hat{L}_{c})\cap(w_{c,1})^{\ast}\ldots(w_{c,n_{c}})^{\ast}$, hence
preserving regularity and boundedness. We then remove those words from
$(w_{c,1},\ldots,w_{c,n_{c}})$ (and their letters from $\Sigma_{c}$) whose
letters do not occur in $L_{c}$. We have
$\Sigma_{c}\subseteq\mathit{Alph}(L_{c})$.

For example, suppose we have one channel $c$ and
$\hat{L}_{c}=(ab)^{\ast}bb^{\ast}$ over $(ab\hskip 1.00006pt,\hskip
1.00006ptb)$. We determine the language $L_{c}$ over $(a_{1}a_{2}\hskip
1.00006pt,\hskip 1.00006pta_{3})$ (omitting the superscript $c$ in the
letters). The homomorphism
$h_{c}:\\{a_{1},a_{2},a_{3}\\}^{\ast}\to\\{a,b\\}^{\ast}$ is given by
$h_{c}(a_{1})=a$ and $h_{c}(a_{2})=h_{c}(a_{3})=b$. We have
$h_{c}^{-1}(\hat{L}_{c})=(a_{1}(a_{2}+a_{3}))^{\ast}(a_{2}+a_{3})(a_{2}+a_{3})^{\ast}$,
which we intersect with $(a_{1}a_{2})^{\ast}a_{3}^{\ast}$. We thus get the
regular bounded language $L_{c}=(a_{1}a_{2})^{\ast}a_{3}a_{3}^{\ast}$ over
$(a_{1}a_{2}\hskip 1.00006pt,\hskip 1.00006pta_{3})$. All letters from
$\\{a_{1},a_{2},a_{3}\\}$ occur in $L_{c}$ so that we are done.

### Trace Property.

In the next step, we build the FIFO machine
${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ such that
$\mathit{Traces}((Q,A_{{M}},T,q_{0}))\subseteq\mathit{Pref}(\text{V})$ with
$\text{V}=\mathord{\operatorname{\text{L}}_{!}}\mathrel{\cap}\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$.
First, to take care of the homomorphisms $h_{c}$, we define the transition
relation $h^{-1}({\hat{T}})=\\{(q,\langle
c!\text{e}\rangle,q^{\prime})\mid(q,\langle c!a\rangle,q^{\prime})\in\hat{T}$
and $\text{e}\in h_{c}^{-1}(a)\\}\mathrel{\cup}\\{(q,\langle
c?\text{e}\rangle,q^{\prime})\mid(q,\langle c?a\rangle,q^{\prime})\in\hat{T}$
and $\text{e}\in h_{c}^{-1}(a)\\}$. Thus, the set of actions of ${M}$ will be
$A_{{M}}=\\{\langle c!\text{e}\rangle\mid c\in\mathit{Ch}$ and
$\text{e}\in\Sigma_{c}\\}\cup\\{\langle c?\text{e}\rangle\mid c\in\mathit{Ch}$
and $\text{e}\in\Sigma_{c}\\}$.

To continue our above example, a transition $(q,\langle
c!b\rangle,q^{\prime})$ would be replaced with the two transitions $(q,\langle
c!a_{2}\rangle,q^{\prime})$ and $(q,\langle c!a_{3}\rangle,q^{\prime})$, and
similarly for $(q,\langle c?b\rangle,q^{\prime})$.

To guarantee trace inclusion in $\mathit{Pref}(\text{V})$, we will consider a
deterministic (not necessarily complete) finite automaton
$\mathcal{A}=(Q_{\mathcal{A}},A_{{M}},T_{\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})=\text{V}$ and where, from every state, a final
state is reachable in the finite graph $(Q_{\mathcal{A}},T_{\mathcal{A}})$.
With this, we define ${M}$ as the product of the FIFO machine
$h^{-1}(\hat{M})=(\hat{Q},\mathit{Ch},\Sigma,h^{-1}(\hat{T}),\hat{q}_{0})$ and
$\mathcal{A}$ in the expected manner. In particular, the set of control states
of ${M}$ is $\hat{Q}\times Q_{\mathcal{A}}$, and its initial state is the pair
$(\hat{q}_{0},q^{0}_{\mathcal{A}})$.

Figure 4 illustrates the result of the normalization procedure for a FIFO
machine $\hat{M}$ with one single channel $c$ (which is therefore omitted) and
its bounded language $\hat{L}_{c}=(ab)^{\ast}bb^{\ast}$ over $(ab\hskip
1.00006pt,\hskip 1.00006ptb)$. Recall from Example 3 that the corresponding
homomorphism $h_{c}$ maps $a_{1}$ to $a$ and both $a_{2}$ and $a_{3}$ to $b$,
and that we obtain $L_{c}=(a_{1}a_{2})^{\ast}a_{3}a_{3}^{\ast}$. Moreover,
${M}$ is the product of $h^{-1}(\hat{M})$ (depicted in the top center) and a
finite automaton $\mathcal{A}$ for
$\text{V}=\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$
(obtained as the shuffle of the two finite automata on the top right). The
state names in ${M}$ reflect the states of $\hat{M}$ and $\mathcal{A}$ they
originate from. We depict only accessible states of ${M}$ from which we can
still complete the word read so far to a word in V. For example,
$(q_{1},\textup{M},\textup{L})$ and $(q_{1},\textup{L},\textup{R})$ would no
longer allow us to reach the final state R of the
$\mathord{\operatorname{\text{L}}_{!}}$-component. $\lhd$

$q_{0}$$q_{1}$$\hat{M}$$\hat{L}_{c}=(ab)^{\ast}bb^{\ast}$$L_{c}=(a_{1}a_{2})^{\ast}a_{3}a_{3}^{\ast}$$!a\,|\,!b\,|\,?a$$?b$$?b$$q_{0}$$q_{1}$$h^{-1}(\hat{M})$MLR$\mathcal{A}$
for
$\text{V}=\mathord{\operatorname{\text{L}}_{!}}\cap\,\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$MLR$!a_{1}\,|\,!a_{2}\,|\,!a_{3}\,|\,?a_{1}$
$?a_{2}\,|\,?a_{3}$$?a_{2}\,|\,?a_{3}$$!a_{1}$$!a_{2}$$!a_{3}$$!a_{3}$$?a_{1}$$?a_{2}$$?a_{3}$$?a_{3}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{L},{M}}}\end{array}$${M}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{M},{M}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{M}}}\end{array}$$\begin{array}[]{c}q_{1}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{R}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{L},{L}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{M},{L}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{L}}}\end{array}$$\begin{array}[]{c}q_{1}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{M}}}\end{array}$$!a_{1}$$!a_{2}$$!a_{1}$$!a_{2}$$?a_{1}$$!a_{3}$$!a_{3}$$?a_{1}$$?a_{1}$$!a_{3}$$!a_{3}$$?a_{3}$$?a_{2}$$?a_{3}$$?a_{3}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{L},{M}}}\end{array}$$\mathcal{C}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{M},{M}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{M}}}\end{array}$$\begin{array}[]{c}q_{1}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{R}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{L},{L}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{M},{L}}}\end{array}$$\begin{array}[]{c}q_{0}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{L}}}\end{array}$$\begin{array}[]{c}q_{1}\\\\[-3.44444pt]
{\scalebox{0.7}{{R},{M}}}\end{array}$$\mathsf{inc}(x)$$\mathsf{inc}(x)$$\mathsf{inc}(x)$$\mathsf{inc}(x)$$\mathsf{dec}(x)$$\mathsf{inc}(y)$$\mathsf{inc}(y)$$\mathsf{dec}(x)$$\mathsf{dec}(x)$$\mathsf{inc}(y)$$\mathsf{inc}(y)$$\begin{array}[]{c}\mathsf{dec}(y)\\\\[-2.15277pt]
x=0\end{array}$$\mathsf{dec}(x)$$\begin{array}[]{c}\mathsf{dec}(y)\\\\[-2.15277pt]
x=0\end{array}$$\begin{array}[]{c}\mathsf{dec}(y)\\\\[-2.15277pt]
x=0\end{array}$

Figure 4. For a FIFO machine $\hat{M}$ with a single channel $c$ and the
bounded language $\hat{L}_{c}=(ab)^{\ast}bb^{\ast}$ over $(ab\hskip
1.00006pt,\hskip 1.00006ptb)$ (top leftmost), we construct a FIFO machine
${M}$ (bottom left), together with
$L_{c}=(a_{1}a_{2})^{\ast}a_{3}a_{3}^{\ast}$, in normal form as the product of
$h^{-1}(\hat{M})$ and an automaton for V (top right). From ${M}$, we then
obtain the counter machine $\mathcal{C}$ (bottom right).

Now suppose we are given a reachability query for $\hat{M}$ in terms of
$\hat{q}\in\hat{Q}$ and a rational relation
$\hat{\text{R}}\subseteq\prod_{c\in\mathit{Ch}}\hat{\Sigma}_{c}^{\ast}$. The
lemma below shows how to reduce it to a reachability query in ${M}$. Here, for
$\mathbf{w}=(\mathbf{w}_{c})_{c\in\mathit{Ch}}\in\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$,
we define
$h(\mathbf{w})=(h_{c}(\mathbf{w}_{c}))_{c\in\mathit{Ch}}\in\prod_{c\in\mathit{Ch}}\hat{\Sigma}_{c}^{\ast}$.
Note that $h^{-1}(\hat{\text{R}})$ is rational. Furthermore,
$h:\Sigma^{\ast}\to\hat{\Sigma}^{\ast}$ is defined by $h(a)=h_{c}(a)$ for all
$c\in\mathit{Ch}$ and $a\in\Sigma_{c}$, and we extend this to
$h:A_{M}^{\ast}\to A_{\hat{M}}^{\ast}$ in the expected manner.

######  Lemma 5.

We have
$(\hat{q},\hat{\mathbf{w}})\in\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$
for some $\hat{\mathbf{w}}\in\hat{\text{R}}$ iff
$((\hat{q},q_{\mathcal{A}}),\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
for some $q_{\mathcal{A}}\in Q_{\mathcal{A}}$ and $\mathbf{w}\in
h^{-1}(\hat{\text{R}})$.

######  Proof 3.2.

Let us assume we have
$(\hat{q},\hat{\mathbf{w}})\in\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$
for some $\hat{\mathbf{w}}\in\hat{\text{R}}$. Hence, there exists
$\hat{\sigma}\in\hat{\mathord{\operatorname{\text{L}}_{!}}}$ such that
$(\hat{q}_{0},\bm{\varepsilon})\xrightarrow{\hat{\sigma}}(\hat{q},\hat{\mathbf{w}})$.
For channel $c$, let $\hat{w}_{c}=\mathit{proj}_{c!}(\hat{\sigma})$. Since
$\hat{\sigma}\in\hat{\mathord{\operatorname{\text{L}}_{!}}}$, we have
$\hat{w}_{c}\in\hat{L}_{c}$ for all $c\in\mathit{Ch}$. Let $w_{c}\in
L_{c}=h_{c}^{-1}(\hat{L}_{c})\cap(w_{c,1})^{\ast}\ldots(w_{c,n_{c}})^{\ast}$
such that $h_{c}(w_{c})=\hat{w}_{c}$. There is a unique $\sigma\in
A_{M}^{\ast}$ such that $h(\sigma)=\hat{\sigma}$ and
$\mathit{proj}_{c!}(\sigma)=w_{c}$ and
$\mathit{proj}_{c?}(\sigma)\in\mathit{Pref}(w_{c})$ for all $c\in\mathit{Ch}$.
Here, $h:\Sigma^{\ast}\to\hat{\Sigma}^{\ast}$ is defined by $h(a)=h_{c}(a)$
for all $c\in\mathit{Ch}$ and $a\in\Sigma_{c}$, and we extend this to
$h:A_{M}^{\ast}\to A_{\hat{M}}^{\ast}$ in the expected manner. Note that
$\sigma\in\mathord{\operatorname{\text{L}}_{!}}\mathrel{\cap}\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$.
Hence, we know that in the FIFO machine $h^{-1}({\hat{M}})$, one has
$(\hat{q}_{0},\bm{\varepsilon})\xrightarrow{\sigma}(\hat{q},\mathbf{w})$ for
some $\mathbf{w}$ (by construction of $h^{-1}({\hat{T}})$), and that
$\sigma\in L(\mathcal{A})$. Therefore, since ${M}$ is a product of the two
machines, we can deduce that there is a run in ${M}$ of the kind
$((\hat{q}_{0},q_{\mathcal{A}}^{0}),\bm{\varepsilon})\xrightarrow{\sigma}(\hat{q},q_{\mathcal{A}}),\mathbf{w})$,
for some value of $q_{\mathcal{A}}$. Furthermore, by $h(\sigma)=\hat{\sigma}$,
we have $h(\mathbf{w})=\hat{\mathbf{w}}$. Hence, $\mathbf{w}\in
h^{-1}(\hat{\text{R}})$.

Conversely, let us assume that
$((\hat{q},q_{\mathcal{A}}),\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
for some $q_{\mathcal{A}}\in Q_{\mathcal{A}}$ and channel contents
$\mathbf{w}\in h^{-1}(\hat{\text{R}})$. Then, we know that there exists
$\sigma\in\mathord{\operatorname{\text{L}}_{!}}$ such that
$((\hat{q}_{0},{q_{\mathcal{A}}^{0}}),\bm{\varepsilon})\xrightarrow{\sigma}((\hat{q},q_{\mathcal{A}}),\mathbf{w})$.
Let $\hat{\sigma}=h(\sigma)$. Since
$\sigma\in\mathord{\operatorname{\text{L}}_{!}}$, we have
$\mathit{proj}_{c!}(\sigma)\in L_{c}$ for all $c\in\mathit{Ch}$. In
particular, $\mathit{proj}_{c!}(\sigma)\in h_{c}^{-1}(\hat{L}_{c})$ and,
therefore,
$h_{c}(\mathit{proj}_{c!}(\sigma))=\mathit{proj}_{c!}(h(\sigma))\in\hat{L}_{c}$.
We deduce $\hat{\sigma}\in\hat{\mathord{\operatorname{\text{L}}_{!}}}$.
Furthermore, we can execute $\hat{\sigma}$ in $\hat{{M}}$ (by construction) to
reach configuration $(\hat{q},\hat{\mathbf{w}})$ for some $\hat{\mathbf{w}}$.
By $\hat{\sigma}=h(\sigma)$, we have $\hat{\mathbf{w}}=h(\mathbf{w})$.
Therefore, $\hat{\mathbf{w}}\in\hat{\text{R}}$.

#### Reduction of Normal Form to Counter Machine

Henceforth, we suppose that ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ and
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ are in normal form, where
$L_{c}$ is a bounded language over $(w_{c,1},\ldots,w_{c,n_{c}})$. In
particular, for every letter $a\in\Sigma_{c}$, there is a unique index
$i\in\\{1,\ldots,n_{c}\\}$ such that $a\in\Sigma_{c,i}$ where
$\Sigma_{c,i}=\mathit{Alph}(w_{c,i})$. We denote this index $i$ by
$\mathit{i}_{a}$.

We build a counter machine $\mathcal{C}$ such that the IB rational-
reachability problem for ${M}$ can be solved by answering a reachability query
in $\mathcal{C}$, using Theorem 1. Each run in $\mathcal{C}$ will simulate a
run in ${M}$. In particular, we want a configuration of $\mathcal{C}$ to allow
us to draw conclusions about the simulated configuration in ${M}$. The
difficulty here is that counter values are just natural numbers and a priori
store less information than channel contents with their messages. To overcome
this, the idea is to represent each word $w_{c,i}$ of a tuple
$(w_{c,1},\ldots,w_{c,n_{c}})$ as a counter $x_{(c,i)}$. Since the set of
possible action sequences is “guided” by a bounded language, we can replace
send actions with increments and receive actions with decrements. More
precisely, $\langle c!a\rangle$ becomes
$(\mathsf{inc}(x_{(c,\mathit{i}_{a})}),\emptyset)$, thus incrementing the
counter associated with the unique word $w_{c,i}$ in which $a$ occurs.
Similarly, $\langle c?a\rangle$ translates to
$(\mathsf{dec}(x_{(c,\mathit{i}_{a})}),Z)$ (for suitable $Z$).

This alone does not put us in a position yet where, from a counter valuation,
we can infer a unique channel contents. However, when we additionally keep
track of the last messages that have been sent for each channel, we can
reconstruct a unique channel contents.

There is one more thing to consider here. While the counters $x_{(c,i)}$ for a
given channel $c$ are kind of independent, the FIFO policy would not allow us
to receive a letter from $w_{c,j}$ while a letter from $w_{c,i}$ with $i<j$ is
in transit. Translated to the counter setting, this means that performing
$\mathsf{dec}(x_{(c,j)})$ should require all counters $x_{(c,i)}$ with $i<j$
to be $0$, so this is where zero tests come into play. As the $L_{c}$ are
bounded languages and thanks to the normal form, however, a counter that has
been tested for zero does not need to be modified anymore.

We can directly implement these ideas formally and define
$\mathcal{C}=(Q,\mathit{Cnt},T^{\prime},q_{0})$ as follows (note that $Q$ and
$q_{0}$ remain unchanged):

  * •

The set of counters is $\mathit{Cnt}=\\{x_{(c,i)}\mid c\in\mathit{Ch}$ and
$i\in\\{1,\ldots,n_{c}\\}\\}$.

  * •

For every $(q,\langle c!a\rangle,q^{\prime})\in T$, we have
$(q,(\mathsf{inc}(x_{(c,\mathit{i}_{a})}),\emptyset),q^{\prime})\in
T^{\prime}$.

  * •

For every $(q,\langle c?a\rangle,q^{\prime})\in T$, we have
$(q,(\mathsf{dec}(x_{(c,\mathit{i}_{a})}),Z),q^{\prime})\in T^{\prime}$ where
the set of counters to be tested for zero is $Z=\\{x_{(c,j)}\mid
j<\mathit{i}_{a}\\}$.

Figure 4 illustrates the construction of $\mathcal{C}$ from a FIFO machine
${M}$ in normal form (cf. Example 3). Recall that we have one channel $c$ and
the bounded language $L_{c}=(a_{1}a_{2})^{\ast}a_{3}a_{3}^{\ast}$ over
$(a_{1}a_{2}\hskip 1.00006pt,\hskip 1.00006pta_{3})$. Thus, $\mathcal{C}$ will
have two counters, say $x$ for $a_{1}a_{2}$ and $y$ for $a_{3}$. Note that
performing $\mathsf{dec}(y)$ indeed comes with a test of $x$ for zero.

Let us first observe that it is actually important that the FIFO machine
satisfies the trace property. Suppose that, rather than from ${M}$, we
constructed the counter machine directly from $h^{-1}(\hat{M})$. Then,
configuration $(q_{1},(1,0))$ would be reachable in the counter machine via
$\mathsf{inc}(x)\mathsf{inc}(x)\mathsf{dec}(x)$, which arises from $\langle
c!a_{1}\rangle\langle c!a_{2}\rangle\langle c?a_{2}\rangle$. However the only
corresponding trace from $\mathit{Pref}(\text{V})$ is $\langle
c!a_{1}\rangle\langle c!a_{2}\rangle\langle c?a_{1}\rangle$, which in the FIFO
machine $h^{-1}(\hat{M})$ leads to $q_{0}$.

So consider ${M}$ and its counter machine $\mathcal{C}$. A channel contents
$\mathbf{w}\in\Sigma_{c}^{\ast}$ (here, we have one channel) has a natural
counter analogue
$\llangle\mathbf{w}\rrangle=(|\mathbf{w}|_{a_{1}}+|\mathbf{w}|_{a_{2}},|\mathbf{w}|_{a_{3}})$.
In fact, if $(\overline{q},\mathbf{w})$ is reachable in ${M}$, then following
the corresponding transitions in $\mathcal{C}$ will lead us to
$(\overline{q},\llangle\mathbf{w}\rrangle)$. For example,
$((q_{0},\textup{R},\textup{L}),a_{2}a_{3}a_{3})$ is reachable in ${M}$ along
the trace $\langle c!a_{1}\rangle\langle c!a_{2}\rangle\langle
c?a_{1}\rangle\langle c!a_{3}\rangle\langle c!a_{3}\rangle$, and so is
$((q_{0},\textup{R},\textup{L}),(1,2))$ in $\mathcal{C}$ along
$\mathsf{inc}(x)\mathsf{inc}(x)\mathsf{dec}(x)\mathsf{inc}(y)\mathsf{inc}(y)$
(all zero tests are empty).

But how about the converse? In general, one may associate with a counter
valuation such as $(4,0)$ several channel contents. Actually, both
$a_{1}a_{2}a_{1}a_{2}$ and $a_{2}a_{1}a_{2}a_{1}$ seem suitable. However, if
we know the most recent message that has been sent, say $a_{1}$, then this
leaves only one option, namely $a_{2}a_{1}a_{2}a_{1}$. In this way, we can
associate with each counter valuation $\mathbf{v}$ and message
$a_{i}\in\Sigma_{c}$ a unique (if it exists at all) possible channel contents
$\llbracket{\mathbf{v}}\rrbracket_{a_{i}}$. Suppose that $\tau$ is a trace in
$\mathcal{C}$ arising from a trace $\sigma$ in ${M}$ whose last sent message
is $a_{i}$. If $(\overline{q},\mathbf{v})$ is reachable in $\mathcal{C}$ via
$\tau$, then $(\overline{q},\llbracket{\mathbf{v}}\rrbracket_{a_{i}})$ is
reachable in ${M}$ via $\sigma$. For example,
$\tau=\mathsf{inc}(x)\mathsf{inc}(x)\mathsf{dec}(x)$ allows us to go to
configuration $((q_{0},\textup{M},\textup{L}),(1,0))$. It arises from
$\sigma=\langle c!a_{1}\rangle\langle c!a_{2}\rangle\langle
c?a_{1}\rangle\in\mathit{Pref}(\text{V})$, whose last sent message is $a_{2}$.
We have $\llbracket{(1,0)}\rrbracket_{a_{2}}=a_{2}$. Indeed, $\sigma$ leads to
$((q_{0},\textup{M},\textup{L}),a_{2})$. $\lhd$

#### Relation between FIFO Machine and Counter Machine

Recall that the FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ and
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ are in normal form, where
$L_{c}$ is a bounded language over $(w_{c,1},\ldots,w_{c,n_{c}})$. Let
$\mathcal{C}=(Q,\mathit{Cnt},T^{\prime},q_{0})$ be the associated counter
machine. We will now formalize the tight forth-and-back correspondence that
allows us to solve reachability queries in ${M}$ in terms of reachability
queries in $\mathcal{C}$.

We start with a simple observation concerning the traces of ${M}$ and
$\mathcal{C}$.

######  Lemma 6.

We have $\mathit{Traces}({M})\subseteq\mathit{Pref}(\text{V})$ and
$\mathit{Traces}(\mathcal{C})\subseteq L_{\mathcal{C}}^{\textsf{{zero}}}$.

######  Proof 3.3.

Observe that
$\mathit{Traces}({M})\subseteq\mathit{Traces}((Q,A_{{M}},T,q_{0}))\subseteq\mathit{Pref}(\text{V})$.
Thus, the first property holds.

For the second statement, consider

$(q_{0},\bm{0})=(q_{0},\mathbf{v}_{0})\xrightarrow{\alpha_{1}}_{\mathcal{C}}(q_{1},\mathbf{v}_{1})\xrightarrow{\alpha_{2}}_{\mathcal{C}}\ldots\xrightarrow{\alpha_{n}}_{\mathcal{C}}(q_{n},\mathbf{v}_{n})$

and let $\tau=\alpha_{1}\ldots\alpha_{n}$. Thus,
$\tau\in\mathit{Traces}(\mathcal{C})$. Suppose that we apply a zero test at
position $\ell\in\\{1,\ldots,n\\}$, i.e.,
$\alpha_{\ell}=(\mathsf{dec}(x_{(c,j)}),Z)$ for some $(c,j)$, where $Z$
contains the counters $x_{(c,i)}$ with $i<j$. Then, there is $k<\ell$ such
that $\alpha_{k}=(\mathsf{inc}(x_{(c,j)}),\emptyset)$. By the construction of
$\mathcal{C}$, we have transitions $(q_{k-1},\langle c!a\rangle,q_{k})$ and
$(q_{\ell-1},\langle c?b\rangle,q_{\ell})$ in ${M}$ for some
$a,b\in\Sigma_{c,j}$. By the trace property of ${M}$, none of the actions
“reachable” from $q_{\ell}$ in ${M}$ employs a message from $\Sigma_{c,i}$,
for all $i<j$. Thus, none of the actions $\alpha_{m}$ with $\ell\leq m$
modifies a counter from $Z$. We deduce that
$\tau\in\smash{L_{\mathcal{C}}^{\textsf{{zero}}}}$.

With every channel contents
$\mathbf{w}\in\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$ of the FIFO machine
${M}$, we associate a counter valuation
$\llangle\mathbf{w}\rrangle=\mathbf{v}\in\mathbb{N}^{\mathit{Cnt}}$ where, for
each counter $x_{(c,i)}$, we let
$\mathbf{v}_{x_{(c,i)}}=\sum_{a\in\Sigma_{c,i}}|\mathbf{w}_{c}|_{a}$.
Furthermore, abusing notation, we define a homomorphism
$\llangle\,.\,\rrangle:A_{{M}}^{\ast}\to A_{\mathcal{C}}^{\ast}$ which maps a
sequence of actions of ${M}$ to a sequence of actions of $\mathcal{C}$. It is
defined by $\llangle\langle
c!a\rangle\rrangle=(\mathsf{inc}(x_{(c,\mathit{i}_{a})}),\emptyset)$ and
$\llangle\langle c?a\rangle\rrangle=(\mathsf{dec}(x_{(c,\mathit{i}_{a})}),Z)$
where $Z=\\{x_{(c,j)}\mid j<\mathit{i}_{a}\\}$.

Conversely, we will associate, with counter values and traces of $\mathcal{C}$
the corresponding objects in the FIFO machine. Because of the inherent
ambiguity, this is, however, less straightforward. First, we define a partial
mapping $\llbracket{\,.\,}\rrbracket:A_{\mathcal{C}}^{\ast}\to A_{{M}}^{\ast}$
(that is not a homomorphism). For $\tau\in A_{\mathcal{C}}^{\ast}$, we let
$\llbracket{\tau}\rrbracket$ be the unique (if it exists) word
$\sigma\in\mathit{Pref}(\text{V})$ such that $\llangle\sigma\rrangle=\tau$.

Next, we associate with a counter valuation a corresponding channel contents.
As explained above, there is no unique choice unless we make an assumption on
the last messages that have been sent. For $c\in\mathit{Ch}$, we set
$\Sigma^{\bot}_{c}=\Sigma_{c}\uplus\\{\bot\\}$. Let $a\in\Sigma^{\bot}_{c}$
and $w\in\Sigma_{c}^{\ast}$. We say that $a$ is _good_ for $w$ if
$w\in\mathit{Infix}(L_{c})$ and either $w=\varepsilon$ or $w=u.a$ for some
$u\in\Sigma_{c}^{\ast}$. Intuitively, it may be possible to obtain contents
$w$ in channel $c$ when $a$ is the last message sent (no message was sent yet
through $c$ if $a=\bot$). Note that the set of words $w\in\Sigma_{c}^{\ast}$
such that $a$ is good for $w$ is a regular language. Moreover, with
$\mathbf{w}\in\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$, we associate the
finite set $G(\mathbf{w})\subseteq\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$ of
tuples $\mathbf{a}=(\mathbf{a}_{c})_{c\in\mathit{Ch}}$ such that, for all
$c\in\mathit{Ch}$, $\mathbf{a}_{c}$ is good for $\mathbf{w}_{c}$.

Let $\mathbf{v}\in\mathbb{N}^{\mathit{Cnt}}$ and
$\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$. Abusing notation, we
will associate with $\mathbf{v}$ and $\mathbf{a}$ the channel contents
$\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}\in\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$
(if it exists). We let
$\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}=\mathbf{w}$ if
$\llangle\mathbf{w}\rrangle=\mathbf{v}$ and $\mathbf{a}\in G(\mathbf{w})$.
There is at most one such $\mathbf{w}$ so that this is well-defined. Note that
$\llangle\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}\rrangle=\mathbf{v}$.

If we have one channel $c$ and our bounded language is
$L_{c}=(a_{1}a_{2}a_{3})^{\ast}(a_{4})^{\ast}$, then
$\llbracket{(4,0)}\rrbracket_{a_{2}}=a_{2}a_{3}a_{1}a_{2}$ and
$\llbracket{(2,1)}\rrbracket_{a_{4}}=a_{2}a_{3}a_{4}$, whereas
$\llbracket{(3,1)}\rrbracket_{a_{3}}$ is undefined. Moreover,
$G(a_{2}a_{3})=\\{a_{3}\\}$ and
$G(\varepsilon)=\\{a_{1},a_{2},a_{3},a_{4},\bot\\}$. $\lhd$

Given $\mathbf{v}$ and $\mathbf{a}$, we can easily compute
$\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}$ since there are only finitely
many words $\mathbf{w}$ for a given $\mathbf{v}$ such that
$\llangle\mathbf{w}\rrangle=\mathbf{v}$. Furthermore, we can also compute
$G(\mathbf{w})$ for a given $\mathbf{w}$ as we have finitely many
possibilities of $\mathbf{a}$.

Finally, for $\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$, we let
$L_{\mathbf{a}}^{\mathsf{last}}\subseteq A_{{M}}^{\ast}$ be the set of words
$\sigma$ such that, for all $c\in\mathit{Ch}$, $\mathbf{a}_{c}$ is the last
message sent to $c$ in $\sigma$ (no message was sent if
$\mathbf{a}_{c}=\bot$). We are now ready to state that runs in the FIFO
machine are faithfully simulated by runs in the counter machine (the proof is
by induction on the length of the trace):

######  Proposition 7.

Let $\sigma\in A_{{M}}^{\ast}$. For all $(q,\mathbf{w})\in S_{M}$ and
$\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$ such that $\sigma\in
L_{\mathbf{a}}^{\mathsf{last}}$, we have:
$(q_{0},\bm{\varepsilon})\xrightarrow{\sigma}_{M}(q,\mathbf{w})\implies\bigl{(}(q_{0},\bm{0})\xrightarrow{\llangle\sigma\rrangle}_{\mathcal{C}}(q,\llangle\mathbf{w}\rrangle)\text{
and }\mathbf{a}\in G(\mathbf{w})\bigr{)}\,.$

######  Proof 3.4.

We will prove the statement by induction on the length of $\sigma$. In the
base case, $|\sigma|=0$. The only value of $\sigma$ such that $|\sigma|=0$ is
$\sigma=\varepsilon$. Furthermore, $\varepsilon\in\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}}^{\mathsf{last}}$ where $\mathbf{a}=(\bot)^{\mathit{Ch}}$. The
initial configuration $(q_{0},\bm{\varepsilon})\in S_{M}$ is the only
configuration reachable by $\varepsilon$. In $\mathcal{T}_{\mathcal{C}}$, the
only configuration reachable via $\llangle\varepsilon\rrangle=\varepsilon$ is
$(q_{0},\bm{0})$ = $(q,\llangle\bm{\varepsilon}\rrangle)$, and
$\llangle\varepsilon\rrangle\in L_{\mathcal{C}}^{\textsf{{zero}}}$. Finally,
we also see that $\mathbf{a}\in G(\bm{\varepsilon})$. Therefore, the base case
is valid.

We suppose that the statement is true for all $\sigma\in A_{{M}}^{\ast}$ such
that $|\sigma|=n$. We will now show that it is true for $\sigma^{\prime}\in
A_{{M}}^{\ast}$ where $|\sigma^{\prime}|=n+1$. Let
$\mathbf{a}^{\prime}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$ and suppose
$\sigma^{\prime}\in\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}^{\prime}}^{\mathsf{last}}$.

We write $\sigma^{\prime}=\sigma.\beta$ such that
$\sigma\in\mathit{Pref}(\text{V})\cap L_{\mathbf{a}}^{\mathsf{last}}$ for some
$\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$, $|\sigma|=n$, and
$\beta\in A_{{M}}$. There exists such a $\sigma$ since the set
$\mathit{Pref}(\text{V})$ is prefix-closed.

Let $(q^{\prime},\mathbf{w}^{\prime})\in S_{M}$ such that
$(q_{0},\bm{\varepsilon})\xrightarrow{\sigma^{\prime}}_{M}(q^{\prime},\mathbf{w}^{\prime})$.
Then, there is $(q,\mathbf{w})\in S_{M}$ such that
$(q_{0},\bm{\varepsilon})\xrightarrow{\sigma}_{M}(q,\mathbf{w})\xrightarrow{\beta}_{M}(q^{\prime},\mathbf{w}^{\prime})$.
Hence, there exists $t=(q,\beta,q^{\prime})\in T$ in the FIFO machine.

### Case (1):

Suppose $\beta=\langle c!a\rangle$, for some $c\in\mathit{Ch}$ and
$a\in\Sigma_{c}$. Hence, we have $\mathbf{w}_{c}^{\prime}=\mathbf{w}_{c}.a$,
and $\mathbf{w}_{d}^{\prime}=\mathbf{w}_{d}$ for all
$d\in\mathit{Ch}\setminus\\{c\\}$. Moreover, since
$\sigma^{\prime}=\sigma.\beta$ and $\beta=\langle c!a\rangle$, we can deduce
that $\mathbf{a}^{\prime}_{c}=a$ and $\mathbf{a}^{\prime}_{d}=\mathbf{a}_{d}$
for all $d\neq c$. This is because the only change in the last sent letters
between $\sigma$ and $\sigma^{\prime}$ is in the channel $c$.

By construction of $\mathcal{C}$, we know that there is a transition
$t^{\prime}=(q,\mathsf{inc}(x_{(c,\mathit{i}_{a})}),\emptyset,q^{\prime})\in
T^{\prime}$ in $\mathcal{C}$, and by the definition of
$\llangle\,.\,\rrangle$, we also have
$\llangle\beta\rrangle=(\mathsf{inc}(x_{(c,\mathit{i}_{a})}),\emptyset)$. By
induction hypothesis, we have
$(q_{0},\bm{0})\xrightarrow{\llangle\sigma\rrangle}(q,\mathbf{v})$ where
$\mathbf{v}=\llangle\mathbf{w}\rrangle$. Since $\llangle\beta\rrangle$
increases a counter, we have
$(q,\mathbf{v})\xrightarrow{\llangle\beta\rrangle}(q^{\prime},\mathbf{v}^{\prime})$
for the counter valuation $\mathbf{v}^{\prime}$ such that
$\mathbf{v}_{x}^{\prime}=\mathbf{v}_{x}+1$ for $x=x_{(c,\mathit{i}_{a})}$ and
$\mathbf{v}_{y}^{\prime}=\mathbf{v}_{y}$ for all
$y\in\mathit{Cnt}\setminus\\{x\\}$. Hence,
$\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$ and we have
$(q_{0},\bm{0})\xrightarrow{\llangle\sigma.\beta\rrangle}(q^{\prime},\llangle\mathbf{w}^{\prime}\rrangle)$.
Note that, by Lemma 6, we have $\llangle\sigma.\beta\rrangle\in
L_{\mathcal{C}}^{\textsf{{zero}}}$.

From the induction hypothesis, we know that $\mathbf{a}\in G(\mathbf{w})$. In
order to show that $\mathbf{a}^{\prime}\in G(\mathbf{w}^{\prime})$, we only
need to address the case of the channel $c$, since the values of
$\mathbf{a}_{d},\mathbf{w}_{d}$ remain unchanged for all $d\neq c$. We know
that $\mathbf{w}^{\prime}_{c}=\mathbf{w}_{c}.\mathbf{a}^{\prime}_{c}$. By
induction hypothesis, $\mathbf{w}_{c}\in\mathit{Infix}(L_{c})$. Since
$\sigma^{\prime}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$, we
also have $\mathbf{w}_{c}.\mathbf{a}^{\prime}_{c}\in\mathit{Infix}(L_{c})$.
Hence, $\mathbf{a}^{\prime}\in G(\mathbf{w}^{\prime})$.

### Case (2):

Suppose $\beta=\langle c?a\rangle$, for some $c\in\mathit{Ch}$ and
$a\in\Sigma_{c}$. We have $\mathbf{w}_{c}=a.\mathbf{w}_{c}^{\prime}$, and
$\mathbf{w}_{d}^{\prime}=\mathbf{w}_{d}$ for all
$d\in\mathit{Ch}\setminus\\{c\\}$. Since $\sigma^{\prime}=\sigma.\beta$ and
$\beta=\langle c?a\rangle$, we can deduce that
$\mathbf{a}^{\prime}=\mathbf{a}$. This is because there is no change in the
last letter sent between $\sigma$ and $\sigma^{\prime}$.

By construction of $\mathcal{C}$, we know that there is a transition
$t^{\prime}=(q,\mathsf{dec}(x_{(c,\mathit{i}_{a})}),Z,q^{\prime})\in
T^{\prime}$ in $\mathcal{C}$ where $Z=\\{(x_{(c,j)})\mid j<\mathit{i}_{a}\\}$.
By the definition of $\llangle\,.\,\rrangle$, we also have
$\llangle\beta\rrangle=(\mathsf{dec}(x_{(c,\mathit{i}_{a})}),Z)$. By the
induction hypothesis, we have
$(q_{0},\bm{0})\xrightarrow{\llangle\sigma\rrangle}(q,\llangle\mathbf{w}\rrangle)$.
Furthermore, recall that $\mathbf{w}_{c}=a.\mathbf{w}_{c}^{\prime}$. This
implies that $a$ is at the head of the channel $c$ in the configuration
$(q,\mathbf{w})$. Hence, all the letters $b$ such that
$\mathit{i}_{b}<\mathit{i}_{a}$ are not present in the channel. Therefore, in
the configuration $(q,\llangle\mathbf{w}\rrangle)$, all the counters
$x_{(c,\mathit{i}_{b})}$ are equal to zero for
$\mathit{i}_{b}<\mathit{i}_{a}$. Hence, we can execute the transition
$t^{\prime}$ from $(q,\llangle\mathbf{w}\rrangle)$, and we have
$(q_{0},\bm{0})\xrightarrow{\llangle\sigma\rrangle}(q,\llangle\mathbf{w}\rrangle)\xrightarrow{\llangle\beta\rrangle}(q^{\prime},\mathbf{v}^{\prime})$
for some counter valuation $\mathbf{v}^{\prime}$. By Lemma 6, we have
$\llangle\sigma.\beta\rrangle\in\smash{L_{\mathcal{C}}^{\textsf{{zero}}}}$. We
write $\mathbf{v}=\llangle\mathbf{w}\rrangle$, and from the counter machine
transition relation, we know that $\mathbf{v}_{x}^{\prime}=\mathbf{v}_{x}-1$
for $x=x_{(c,\mathit{i}_{a})}$ and $\mathbf{v}_{y}^{\prime}=\mathbf{v}_{y}$
for all $y\in\mathit{Cnt}\setminus\\{x\\}$. Hence,
$\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$.

From the induction hypothesis, we know that $\mathbf{a}\in G(\mathbf{w})$. In
order to show that $\mathbf{a}^{\prime}\in G(\mathbf{w}^{\prime})$, we only
need to address the case of the channel $c$, since the values of
$\mathbf{a}_{d},\mathbf{w}_{d}$ remain unchanged for all $d\neq c$. We know
from the induction hypothesis that $\mathbf{w}_{c}\in\mathit{Infix}(L_{c})$.
Hence, we can immediately deduce that
$\mathbf{w}^{\prime}_{c}\in\mathit{Suf}(\mathbf{w}_{c})\subseteq\mathit{Infix}(L_{c})$.

Furthermore, we know that $\mathbf{w}_{c}=u.\mathbf{a}^{\prime}_{c}$ for some
$u\in\Sigma_{c}^{\ast}$. If $u=\varepsilon$, then we can deduce that
$\mathbf{w}^{\prime}_{c}=\varepsilon$. If $u\neq\varepsilon$, then we have
$\mathbf{w}^{\prime}_{c}=u^{\prime}.\mathbf{a}^{\prime}_{c}$ such that
$a.u^{\prime}=u$. Hence, $\mathbf{a}^{\prime}\in G(\mathbf{w}^{\prime})$.

Conversely, we can show that runs of the counter machine can be retrieved in
the FIFO machine (again, the proof proceeds by induction on the length of the
trace):

######  Proposition 8.

Let $\tau\in A_{\mathcal{C}}^{\ast}$. For all $(q,\mathbf{v})\in
S_{\mathcal{C}}$ and $\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$
such that $\tau\in\llangle\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}}^{\mathsf{last}}\rrangle$, we have:
$(q_{0},\bm{0})\xrightarrow{\tau}_{\mathcal{C}}(q,\mathbf{v})\implies(q_{0},\bm{\varepsilon})\xrightarrow{\llbracket{\tau}\rrbracket}_{M}(q,\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}})\,.$

######  Proof 3.5.

We proceed by induction on the length of $\tau$. In the base case, $|\tau|=0$.
The only value of $\tau$ such that $|\tau|=0$ is $\tau=\varepsilon$.
Furthermore, $\varepsilon\in\llangle\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}}^{\mathsf{last}}\rrangle$ where $\mathbf{a}_{c}=\bot$ for all
$c\in\mathit{Ch}$. The only configuration reachable via $\varepsilon$ is
$(q_{0},\bm{0})$. In the FIFO machine, the configuration
$(q_{0},\bm{\varepsilon})$ is the only configuration reachable via
$\llbracket{\varepsilon}\rrbracket=\varepsilon$. We know that the initial
contents is $\bm{\varepsilon}=\llbracket{\bm{0}}\rrbracket_{\mathbf{a}}$.
Hence, the base case is valid.

Let us suppose that the statement holds for $\tau\in A_{\mathcal{C}}^{\ast}$
where $|\tau|=n$. We show that it is true for $\tau^{\prime}$ with
$|\tau^{\prime}|=n+1$. Let $\mathbf{a}^{\prime}$ such that
$\tau^{\prime}\in\llangle\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}^{\prime}}^{\mathsf{last}}\rrangle$. Then we can write
$\tau^{\prime}=\tau.\alpha$ for some $\tau\in A_{\mathcal{C}}^{\ast}$ and
$\alpha\in A_{\mathcal{C}}$. There exists
$\sigma^{\prime}\in\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}^{\prime}}^{\mathsf{last}}$ such that
$\llangle\sigma^{\prime}\rrangle=\tau^{\prime}$. Furthermore, since
$\llangle\,.\,\rrangle$ is a homomorphism, we can express
$\sigma^{\prime}=\sigma.\beta$ for some $\sigma\in A_{{M}}^{\ast}$ and
$\beta\in A_{{M}}$ where $\llangle\beta\rrangle=\alpha$ and
$\llangle\sigma\rrangle=\tau$. Since $\mathit{Pref}(\text{V})$ is prefix-
closed, we have $\sigma\in\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}}^{\mathsf{last}}$ for some
$\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$. Therefore,
$\tau\in\llangle\mathit{Pref}(\text{V})\cap
L_{\mathbf{a}}^{\mathsf{last}}\rrangle$.

Let
$(q_{0},\bm{0})\xrightarrow{\tau^{\prime}}_{\mathcal{C}}(q^{\prime},\mathbf{v}^{\prime})$.
Note that, by Lemma 6, we have $\tau^{\prime}\in
L_{\mathcal{C}}^{\textsf{{zero}}}$. We will prove that
$(q_{0},\bm{\varepsilon})\xrightarrow{\llbracket{\tau^{\prime}}\rrbracket}_{M}(q,\mathbf{w}^{\prime})$
where
$\mathbf{w}^{\prime}=\llbracket{\mathbf{v}^{\prime}}\rrbracket_{\mathbf{a}^{\prime}}$.
Since $\tau^{\prime}=\tau.\alpha$, there is $(q,\mathbf{v})\in
S_{\mathcal{C}}$ such that
$(q_{0},\bm{0})\xrightarrow{\tau}(q,\mathbf{v})\xrightarrow{\alpha}(q^{\prime},\mathbf{v}^{\prime})$.
Hence, there exists a transition $t=(q,\alpha,q^{\prime})\in T^{\prime}$.

By the induction hypothesis, we know that
$(q_{0},\bm{\varepsilon})\xrightarrow{\smash{\llbracket{\tau}\rrbracket}}_{M}(q,\mathbf{w})$
where $\mathbf{w}=\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}$.

### Case (1):

Suppose $\alpha=(\mathsf{inc}(x_{(c,i)}),\emptyset)$ for $c\in\mathit{Ch}$ and
$i\in\\{1,\ldots,n_{c}\\}$. We have $\mathbf{v}_{x}^{\prime}=\mathbf{v}_{x}+1$
for $x=x_{(c,i)}$ and $\mathbf{v}_{y}^{\prime}=\mathbf{v}_{y}$ and for all
$y\in\mathit{Cnt}\setminus\\{x\\}$.

By construction of $\mathcal{C}$, we know that there is a transition
$t^{\prime}=(q,\gamma,q^{\prime})\in T$ in ${M}$ with $\gamma=\langle
c!a\rangle$ for some $a\in\Sigma_{c}$ such that $\mathit{i}_{a}=i$. Thanks to
the trace property (Definition 3 (2.)), we have $\beta=\gamma$. Let
$\mathbf{w}^{\prime}$ be given by $\mathbf{w}_{c}^{\prime}=\mathbf{w}_{c}.a$
and $\mathbf{w}_{d}^{\prime}=\mathbf{w}_{d}$ for all
$d\in\mathit{Ch}\setminus\\{c\\}$. Then,
$(q,\mathbf{w})\xrightarrow{\beta}_{M}(q^{\prime},\mathbf{w}^{\prime})$.
Furthermore, since $\mathit{i}_{a}=i$ and
$\llangle\mathbf{w}\rrangle=\mathbf{v}$, we can deduce that
$\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$. Moreover, recall
that $\llangle\sigma.\beta\rrangle=\tau.\alpha$, hence,
$\sigma^{\prime}=\sigma.\beta=\llbracket{\tau^{\prime}}\rrbracket$.

Since $\sigma^{\prime}=\sigma.\beta$ and $\beta=\langle c!a\rangle$, we can
deduce that $\mathbf{a}^{\prime}_{c}=a$ and
$\mathbf{a}^{\prime}_{d}=\mathbf{a}_{d}$ for all $d\neq c$. This is because
the only change in the last sent letters between $\sigma$ and
$\sigma^{\prime}$ is in the channel $c$.

We recall that $\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$. From
the induction hypothesis, we know that
$\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}=\mathbf{w}$. Hence, in order
to show that
$\llbracket{\mathbf{v}^{\prime}}\rrbracket_{\mathbf{a}^{\prime}}{}=\mathbf{w}^{\prime}$,
we only need to address the case of the channel $c$, since the values of
$\mathbf{a}_{d},\mathbf{w}_{d}$ remain unchanged for all $d\neq c$. We know
that $\mathbf{w}^{\prime}_{c}=\mathbf{w}_{c}.\mathbf{a}^{\prime}_{c}$. Since
$\sigma^{\prime}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$, we
have $\mathbf{w}_{c}.\mathbf{a}^{\prime}_{c}\in\mathit{Infix}(L_{c})$.
Therefore,
$\mathbf{w}^{\prime}=\llbracket{\mathbf{v}^{\prime}}\rrbracket_{\mathbf{a}^{\prime}}{}$.

### Case (2):

Suppose $\alpha=(\mathsf{dec}(x_{(c,i)}),Z)$, for $c\in\mathit{Ch}$,
$i\in\\{1,\ldots,n_{c}\\}$ and $Z=\\{x_{(c,j)}\mid j<i\\}$. We have
$\mathbf{v}_{x}^{\prime}=\mathbf{v}_{x}-1$ for $x=x_{(c,i)}$ and
$\mathbf{v}_{y}^{\prime}=\mathbf{v}_{y}$ for all
$y\in\mathit{Cnt}\setminus\\{x\\}$.

By construction of $\mathcal{C}$, we know that there is a transition
$t^{\prime}=(q,\gamma,q^{\prime})\in T$ in ${M}$ with $\gamma=\langle
c?a\rangle$ for some $a\in\Sigma_{c}$ such that $\mathit{i}_{a}=i$. Again, by
the trace property (Definition 3 (2.)), we get $\beta=\gamma$. In order to
execute $t^{\prime}$ from $(q,\mathbf{w})$, it is necessary that we have
$\mathbf{w}_{c}=a.u$ for some word $u$.

Since $\sigma.\beta\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$
and $\mathit{proj}_{c?}(\sigma).\mathbf{w}_{c}=\mathit{proj}_{c!}(\sigma)$, we
can deduce that $\mathbf{w}_{c}=a.u$ for some word $u$. Hence, the transition
$t^{\prime}$ can be executed to reach a configuration
$(q^{\prime},\mathbf{w}^{\prime})$ such that
$\mathbf{w}_{c}=a\cdot\mathbf{w}_{c}^{\prime}$, and
$\mathbf{w}_{d}^{\prime}=\mathbf{w}_{d}$ for all
$d\in\mathit{Ch}\setminus\\{c\\}$. Furthermore, since $\mathit{i}_{a}=i$ and
$\llangle\mathbf{w}\rrangle=\mathbf{v}$, we can deduce that
$\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$. Moreover, recall
that $\llangle\sigma.\beta\rrangle=\tau.\alpha$, hence,
$\sigma^{\prime}=\sigma.\beta=\llbracket{\tau^{\prime}}\rrbracket$.

Since $\sigma^{\prime}=\sigma.\beta$ and $\beta=\langle c?a\rangle$, we can
deduce that $\mathbf{a}^{\prime}=\mathbf{a}$. This is because no letters are
sent between $\sigma$ and $\sigma^{\prime}$.

We also know from the induction hypothesis that
$\mathbf{w}=\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}$. Also recall that
$\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$. In order to show
that
$\mathbf{w}^{\prime}=\llbracket{\mathbf{v}^{\prime}}\rrbracket_{\mathbf{a}^{\prime}}{}$,
we only need to address the case of the channel $c$, since the values of
$\mathbf{a}_{d},\mathbf{w}_{d}$ remain unchanged for all $d\neq c$.

We know from the induction hypothesis that $\mathbf{w}_{c}$ is contained in
$\mathit{Infix}(L_{c})$ and, thus, so is $\mathbf{w}_{c}^{\prime}$.
Furthermore, we know that $\mathbf{w}_{c}=u.\mathbf{a}^{\prime}_{c}$ for some
$u\in\Sigma_{c}^{\ast}$. If $u=\varepsilon$, then we can deduce that
$\mathbf{w}^{\prime}_{c}=\varepsilon$. On the other hand, if
$u\neq\varepsilon$, then we know that
$\mathbf{w}^{\prime}_{c}=u^{\prime}.\mathbf{a}^{\prime}_{c}$ such that
$a.u^{\prime}=u$. We also recall that
$\llangle\mathbf{w}^{\prime}\rrangle=\mathbf{v}^{\prime}$. Hence,
$\mathbf{w}^{\prime}=\llbracket{\mathbf{v}^{\prime}}\rrbracket_{\mathbf{a}^{\prime}}{}$.

From Propositions 7 and 8 and Lemma 6, we obtain the following corollary.

######  Corollary 9.

For all $(q,\mathbf{w})\in S_{M}$, we have:
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})\Longleftrightarrow(q,\llangle\mathbf{w}\rrangle)\in\textstyle\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\text{V}\cap\bigcup_{\mathbf{a}\in
G(\mathbf{w})}L_{\mathbf{a}}^{\mathsf{last}}\rrangle)\,.$

From Theorem 1, we know that verifying whether
$(q,\llangle\mathbf{w}\rrangle)\in\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap
L)$ where $L=\llangle\text{V}\cap\bigcup_{\mathbf{a}\in
G(\mathbf{w})}L_{\mathbf{a}}^{\mathsf{last}}\rrangle$ is decidable. Hence, we
can already deduce decidability of the (configuration-)reachability problem.
In fact, using Propositions 7 and 8, we can solve the more general IB
rational-reachability problem. For this, it is actually enough to check, in
the counter machine, the reachability of a counter value that belongs to a
semi-linear set. For $\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$
and a rational relation
$\text{R}\subseteq\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$, let
$V_{\mathbf{a}}(\text{R})=\\{\mathbf{v}\in\mathbb{N}^{\mathit{Cnt}}\mid\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}\in\text{R}\\}$.

######  Lemma 10.

The set $V_{\mathbf{a}}(\text{R})$ is effectively semi-linear.

######  Proof 3.6.

For $c\in\mathit{Ch}$, let $\mathcal{G}_{c}$ be the set of words
$w\in\Sigma_{c}^{\ast}$ such that $\mathbf{a}_{c}$ is good for $w$. Moreover,
let $\text{G}=\prod_{c\in\mathit{Ch}}\mathcal{G}_{c}$.

As $\mathcal{G}_{c}$ is regular for every $c\in\mathit{Ch}$, the relation G is
recognizable. As the intersection of a rational and a recognizable relation is
rational, we have that $\text{R}\cap\text{G}$ is rational. It follows that
$\textup{Parikh}(\text{R}\cap\text{G})$ is semi-linear. From the definitions,
we obtain

$\begin{array}[]{rlll}\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}\in\text{R}&\Longleftrightarrow&\exists\mathbf{w}\in\text{R}\cap\text{G}:&\forall
x_{(c,i)}\in\mathit{Cnt}:\mathbf{v}_{x_{(c,i)}}=\sum_{a\in\Sigma_{c,i}}|\mathbf{w}_{c}|_{a}\\\
&\Longleftrightarrow&\exists\pi\in\textup{Parikh}(\text{R}\cap\text{G}):\\!\\!\\!&\forall
x_{(c,i)}\in\mathit{Cnt}:\mathbf{v}_{x_{(c,i)}}=\sum_{a\in\Sigma_{c,i}}\pi_{a}\end{array}$

Thus,

$V_{\mathbf{a}}(\text{R})=\\{\mathbf{v}\in\mathbb{N}^{\mathit{Cnt}}\mid\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}\in\text{R}\\}=\textstyle\bigl{\\{}\bigl{(}\sum_{a\in\Sigma_{c,i}}\pi_{a}\bigr{)}_{x_{(c,i)}\in\mathit{Cnt}}\mid\pi\in\textup{Parikh}(\text{R}\cap\text{G})\bigr{\\}}\,.$

Let $\varphi((X_{a})_{a\in\Sigma})$ be a Presburger formula defining
$\textup{Parikh}(\text{R}\cap\text{G})$. Then, by the above equivalence, the
following Presburger formula defines $V_{\mathbf{a}}(\text{R})$:

$\psi_{c}((Z_{y})_{y\in\mathit{Cnt}})=\exists(X_{a})_{a\in\Sigma}:\Bigl{(}\varphi((X_{a})_{a\in\Sigma})\wedge\bigwedge_{y\in\mathit{Cnt}}Z_{y}=\sum_{a\in\Sigma_{y}}X_{a}\Bigl{)}$

where, for $y=x_{(c,i)}\in\mathit{Cnt}$, we let $\Sigma_{y}=\Sigma_{c,i}$. It
follows that $V_{\mathbf{a}}(\text{R})$ is effectively semi-linear.

Using this property, we finally reduce the IB rational-reachability problem to
a reachability problem in counter machines:

######  Corollary 11.

For every $q\in Q$, we have:
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})\text{
for some
$\mathbf{w}\in\text{R}$}\Longleftrightarrow(q,\mathbf{v})\in\textstyle\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\text{V}\cap
L_{\mathbf{a}}^{\mathsf{last}}{}\rrangle)\textup{ for some
}\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}\text{ and
}\mathbf{v}\in V_{\mathbf{a}}(\text{R})\,.$

######  Proof 3.7.

Suppose
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
with $\mathbf{w}\in\text{R}$. There are
$\mathbf{a}\in\prod_{c\in\mathit{Ch}}\Sigma^{\bot}_{c}$ and
$\sigma\in\text{V}\cap L_{\mathbf{a}}^{\mathsf{last}}{}$ such that
$(q_{0},\bm{\varepsilon})\xrightarrow{\sigma}_{M}(q,\mathbf{w})$. By
Proposition 7 and Lemma 6, we have
$(q_{0},\bm{0})\xrightarrow{\llangle\sigma\rrangle}_{\mathcal{C}}(q,\llangle\mathbf{w}\rrangle)$
and $\llangle\sigma\rrangle\in L_{\mathcal{C}}^{\textsf{{zero}}}$ and
$\mathbf{a}\in G(\mathbf{w})$. By definition, the latter implies
$\mathbf{w}=\llbracket{\llangle\mathbf{w}\rrangle}\rrbracket_{\mathbf{a}}{}$
and hence $\llangle\mathbf{w}\rrangle\in V_{\mathbf{a}}(\text{R})$.

Conversely, suppose we have
$(q_{0},\bm{0})\xrightarrow{\llangle\sigma\rrangle}_{\mathcal{C}}(q,\mathbf{v})$
where $\sigma\in\text{V}\cap L_{\mathbf{a}}^{\mathsf{last}}{}$,
$\llangle\sigma\rrangle\in L_{\mathcal{C}}^{\textsf{{zero}}}$, and
$\mathbf{v}\in V_{\mathbf{a}}(\text{R})$. By Proposition 8, we get
$(q_{0},\bm{\varepsilon})\xrightarrow{\llbracket{\llangle\sigma\rrangle}\rrbracket}_{M}(q,\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{})$.
Note that
$\llbracket{\llangle\sigma\rrangle}\rrbracket=\sigma\in\mathord{\operatorname{\text{L}}_{!}}$.
Moreover, $\mathbf{v}\in V_{\mathbf{a}}(\text{R})$ implies
$\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}\in\text{R}$, which concludes
the proof.

By Theorem 1, we can now deduce Theorem 4, i.e., decidability of IB rational-
reachability.

##  4\. Reachability and Deadlock

We now address some other commonly studied reachability problems, which, as it
turns out, can be reduced to the IB rational-reachability problem studied in
the previous section.

A configuration $(q,\mathbf{w})$ of a FIFO machine ${M}$ is a _deadlock_ if
there is no $(q^{\prime},\mathbf{w}^{\prime})$ such that
$(q,\mathbf{w})\to_{M}(q^{\prime},\mathbf{w}^{\prime})$.

[IB decision problems] Given a FIFO machine
${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a control-state $q\in Q$, a
configuration $s\in S_{M}$, and a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$.

  * •

_IB reachability_ : Do we have
$s\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ ?

  * •

_IB control-state reachability_ : Do we have
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
for some $\mathbf{w}$ ?

  * •

_IB deadlock_ : Does
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ contain a
deadlock ?

In [FP19], it was shown that reachability reduces to control-state
reachability for flat FIFO machines but the converse is not true. However,
using the same reductions as in [FP19], we obtain the following results:

######  Proposition 12.

IB reachability is

  1. (a)

recursively equivalent to IB control-state reachability for FIFO machines, and

  2. (b)

recursively reducible to IB deadlock for FIFO machines.

######  Proof 4.1.

We show both parts of the lemma.

### Part (a):

Let us consider a FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$ with
$\mathit{Ch}=\\{1,\ldots,m\\}$, a control-state $q$, a configuration
$(q,\mathbf{w})$, and a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$. Suppose
$\mathbf{w}=(\mathbf{w}_{c})_{c\in\mathit{Ch}}$ with
$\mathbf{w}_{c}=\mathbf{w}_{c}^{1}\ldots\mathbf{w}_{c}^{n_{c}}$.

We first reduce IB reachability to IB control-state reachability. Another
machine
${M}_{(q,\mathbf{w})}=(Q^{\prime},\mathit{Ch},\Sigma^{\prime},T^{\prime},q_{0})$
is constructed as follows. We set $Q^{\prime}=Q\cup\\{q_{\text{end}}\\}$ such
that $q_{\text{end}}\notin Q$, and $\Sigma^{\prime}=\Sigma\cup\\{\$\\}$ such
that $\$\not\in\Sigma$. Moreover, a “path”
$q\xrightarrow{\sigma}q_{\text{end}}$ with $\sigma=\sigma_{1}\ldots\sigma_{m}$
is added from the control state $q$ as follows. For $c\in\mathit{Ch}$, we have

$\sigma_{c}=\begin{cases}\langle c!\$\rangle\langle
c?\mathbf{w}_{c}^{1}\rangle\ldots\langle
c?\mathbf{w}_{c}^{n_{c}}\rangle\langle c?\$\rangle&\text{if
}|\mathbf{w}_{c}|>0,\\\ \langle c!\$\rangle\langle
c?\$\rangle&\text{otherwise. }\end{cases}$

Then,
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
iff
$(q_{\text{end}},\mathbf{w}^{\prime})\in\mathit{Reach}_{{M}_{(q,\mathbf{w})}}(\mathord{\operatorname{\text{L}}_{!}}^{\prime})$
for _some_ $\mathbf{w}^{\prime}$, where $\mathop{\operatorname{\text{L}}\hskip
0.09995pt^{\prime}}=(L_{c}.\mathbf{w}_{c}.\$)_{c\in\mathit{Ch}}$. Furthermore,
$\mathop{\operatorname{\text{L}}\hskip 0.09995pt^{\prime}}$ is bounded if
$\operatorname{\text{L}}$ is bounded, since concatenation of a finite word
with a bounded language results in a bounded language. Therefore, IB
reachability reduces to IB control-state reachability for FIFO machines.

Conversely, in order to show that IB control-state reachability is reducible
to IB reachability, we construct ${M}_{q}$ as follows. To ${M}$, we add
$|\Sigma|\times m$ self-loops from and to the control state $q$ as follows:
$q\xrightarrow{c?a}q$ for all $c\in\mathit{Ch}$ and $a\in\Sigma_{c}$.

The control-state $q$ is reachable in ${M}$ iff there exists $\mathbf{w}$ such
that $(q,\mathbf{w})$ is reachable in ${M}$ iff $(q,\bm{\varepsilon})$ is
reachable in ${M}_{q}$. Furthermore, consider
$\sigma\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$ such that
$(q_{0},\bm{\varepsilon})\xrightarrow{\sigma}_{M}(q,\mathbf{w})$ for some
channel contents $\mathbf{w}$. Let us append to $\sigma$ a sequence of actions
$\sigma^{\prime}=\sigma_{1}\ldots\sigma_{m}$ such that $\sigma_{c}=\langle
c?\mathbf{w}_{c}\rangle$ for all $c\in\mathit{Ch}$, where $\langle
c?\mathbf{w}_{c}\rangle$ is to be understood as a sequence of transitions
whose effect is to consume the string $\mathbf{w}_{c}$ from the channel $c$.
By construction, we have,
$(q_{0},\bm{\varepsilon})\xrightarrow{\sigma\cdot\sigma^{\prime}}_{{M}_{q}}(q,\bm{\varepsilon})$.
Furthermore,
$\mathit{proj}_{c!}(\sigma)=\mathit{proj}_{c!}(\sigma\cdot\sigma^{\prime})$
for all $c\in\mathit{Ch}$. Hence,
$\sigma\cdot\sigma^{\prime}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$
and we can conclude that
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\operatorname{\text{L}}_{!})$ iff
$(q,\bm{\varepsilon})\in\mathit{Reach}_{{M}_{q}}(\operatorname{\text{L}}_{!})$.

Therefore, IB control-state reachability reduces to IB reachability for FIFO
machines.

### Part (b):

Given a FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a configuration
$(q,\mathbf{w})$, and a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$, we construct
${M}_{(q,\mathbf{w})}$ as in the case of reducing reachability to control-
state reachability (see proof of Proposition 12(a)). We then modify
${M}_{(q,w)}$ to ${M}^{\prime}$ as follows. We add a new channel $d$ to the
existing set of channels $\mathit{Ch}$ (the set of channels is now
$\mathit{Ch}^{\prime}$). For all $q\neq q_{\textsf{end}}$, we add the
following transition: $(q,\langle d!\$\rangle,q)$. Hence, except for
$q_{\textsf{end}}$, every control state has at least one send action. Finally,
we also construct a new tuple $\mathop{\operatorname{\text{L}}\hskip
0.09995pt^{\prime}}=(L^{\prime}_{c})_{c\in\mathit{Ch}^{\prime}}$ such that
$L^{\prime}_{c}=L_{c}.\$$ for all $c\in\mathit{Ch}$ and
$L^{\prime}_{d}=\$^{\ast}$.

We claim that
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
iff
$\mathit{Reach}_{{M}^{\prime}}(\mathord{\operatorname{\text{L}}_{!}}^{\prime})$
contains a deadlock. To see this, first, we observe that, if there is a
deadlock in
$\mathit{Reach}_{{M}^{\prime}}(\mathord{\operatorname{\text{L}}_{!}}^{\prime})$,
then the associated control state would be $q_{\textsf{end}}$ since if we are
in any configuration $s^{\prime}$ such that the associated control state
$q^{\prime}$ is not $q_{\textsf{end}}$, the transition $(q^{\prime},\langle
d!\$\rangle,q^{\prime})$ can always be taken, and hence, there will never be a
deadlock.

Let us now suppose that the configuration $(q,\mathbf{w})$ is in
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$. We can execute
the same set of transitions as in ${M}$ and reach the control state $q$ with
the channel contents $\mathbf{w}$ via an execution $\sigma^{\prime}$ in
${M}^{\prime}$. Having done that, we can then execute the path
$q\xrightarrow{\sigma}q_{\textsf{end}}$ as described in $T^{\prime}$ in order
to reach $q_{\textsf{end}}$. Also observe that
$\sigma^{\prime}\cdot\sigma\in\mathord{\operatorname{\text{L}}_{!}}^{\prime}$.
Since there are no transitions from this control state, we reach a deadlock.

Suppose now that $(q,\mathbf{w})$ is not in
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$. Hence, we
cannot reach $(q,\mathbf{w})$ in ${M}^{\prime}$ and thus, cannot execute
$q\xrightarrow{\sigma}q_{\textsf{end}}$. Furthermore, as we saw previously, we
can never be in a deadlock as we can always send $\$$ to the channel $d$.

If, for a given $q\in Q$, we set R to be the universal relation
$\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$, IB rational-reachability captures
IB control-state reachability, and if we set $\text{R}=\\{\mathbf{w}\\}$, we
can decide if the configuration $(q,\mathbf{w})$ is reachable. In order to
reduce IB deadlock to IB rational-reachability, we first explore the control
states in order to find the set of states $Q^{\prime}\subseteq Q$ which allow
only receptions (no control states with sends can be part of a deadlock). This
set can easily be computed from the set of transitions of the machine. Then,
for each $q\in Q^{\prime}$, we can see if there exists a reachable
configuration $(q,\mathbf{w})$ such that, for all $c$, we have
$\mathbf{w}_{c}\in K_{c}=\\{\varepsilon\\}\cup\\{a.u\mid
u\in\Sigma_{c}^{\ast}\text{ and }a\in\Sigma_{c}$ such that there is no
transition $(q,\langle c?a\rangle,q^{\prime})$ in ${M}\\}$. Note that
$\text{R}_{q}=\prod_{c\in\mathit{Ch}}K_{c}$ is recognizable and, therefore,
rational. Furthermore, if there exists such a reachable $(q,\mathbf{w})$ with
$\mathbf{w}\in\text{R}_{q}$, then it is a deadlock. Hence, using the fact that
generalized IB rational-reachability is decidable (Theorem 4), we immediately
deduce the following corollary:

######  Corollary 13.

The problems IB reachability, IB control-state reachability, and IB deadlock
are decidable for FIFO machines.

######  Remark 14.

Since input-bounded FIFO machines subsume VASS (a VASS can be seen as an
input-bounded FIFO machine with an alphabet reduced to a unique letter), the
complexity of IB reachability is not elementary, which is inherited from the
lower bound for VASS [CLL+19].

##  5\. Unboundedness and Termination

We now introduce two new decision problems, as follows.

[IB finiteness problems] Given a FIFO machine
${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a control-state $q\in Q$, a
configuration $s\in S_{M}$, and a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$.

  * •

_IB unboundedness_ : Is
$\mathit{Reach}_{{M}}(\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}}))$
infinite?

  * •

_IB termination_ : Is there no infinite execution of the form
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
such that, for all $i\in\mathbb{N}$, we have $s_{i}\in S_{M}$, $\beta_{i}\in
A_{{M}}$, and
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$?

Decidability of the unboundedness and termination problems can be deduced from
the reachability decision problems. We detail the construction in the sections
below.

### Unboundedness

IB unboundedness in FIFO machines reduces to an equivalent problem in counter
machines. Given a FIFO machine $\hat{M}$ and $\hat{\operatorname{\text{L}}}$,
the associated FIFO machine ${M}$ in normal form (with the corresponding tuple
$\operatorname{\text{L}}$ of distinct-letter languages), as well as the
associated counter machine $\mathcal{C}$, the following result can be derived.

######  Proposition 15.

$\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$ is
infinite iff $\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ is
infinite iff
$\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\text{V}\rrangle)$
is infinite.

######  Proof 5.1.

We first show that unboundedness is preserved by the normal-form construction.
This essentially follows from Lemma 5 and the fact that $h$ is length-
preserving.

If
$(q,\hat{\mathbf{w}})\in\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$,
then
$((q,q_{\mathcal{A}}),\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$
for some $q_{\mathcal{A}}$ and $\mathbf{w}$ such that
$h(\mathbf{w})=\hat{\mathbf{w}}$. Thus, if
$\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$ is
infinite, then so is
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$.

Conversely, if
$((q,q_{\mathcal{A}}),\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$,
then
$(q,h(\mathbf{w}))\in\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$.
Thus, if $\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ is
infinite, then so is
$\mathit{Reach}_{\hat{M}}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$.

Now, let us assume that
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ is infinite.
Hence, there are infinitely many configurations $(q,\mathbf{w})\in S_{M}$
which are reachable from $(q_{0},\bm{\varepsilon})$. From Corollary 9, for
each of these configurations,
$(q,\llangle\mathbf{w}\rrangle)\in\textstyle\mathit{Reach}_{\mathcal{C}}(L)$,
where
$L=L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\cap\bigcup_{\mathbf{a}\in
G(\mathbf{w})}L_{\mathbf{a}}^{\mathsf{last}}\rrangle$. Since $L\subseteq
L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\rrangle$,
we have
$(q,\llangle\mathbf{w}\rrangle)\in\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\rrangle)$.
Furthermore, there are only finitely many configurations $(q,\mathbf{w})\in
S_{M}$ that correspond to a configuration $(q,\llangle\mathbf{w}\rrangle)\in
S_{\mathcal{C}}$. Hence, if
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ is infinite,
$\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\rrangle)$
is infinite.

For the converse direction, let us assume that
$\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\rrangle)$
is infinite. Hence, there are infinitely many configurations $(q,\mathbf{v})$
reachable from $(q_{0},\bm{0})$ via some $\tau$ such that $\tau\in
L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\rrangle$.
Pick one such $(q,\mathbf{v})$ and $\tau$. There exists a unique $\sigma$ such
that $\llangle\sigma\rrangle=\tau$. Consider the vector $\mathbf{a}$ such that
$\sigma\in L_{\mathbf{a}}^{\mathsf{last}}{}$ and let
$\mathbf{w}=\llbracket{\mathbf{v}}\rrbracket_{\mathbf{a}}{}$. Thus,
$\llangle\mathbf{w}\rrangle=\mathbf{v}$. Hence,
$(q,\llangle\mathbf{w}\rrangle)\in\textstyle\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathord{\operatorname{\text{L}}_{!}}\cap\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})\cap\bigcup_{\mathbf{a}\in
G(\mathbf{w})}L_{\mathbf{a}}^{\mathsf{last}}\rrangle)$. From Corollary 9, we
can deduce that
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$.
Therefore, for every $\mathbf{v}$ such that $(q,\mathbf{v})$ is reachable,
there is a corresponding configuration $(q,\mathbf{w})$ reachable in
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$.

In particular, this statement applies to prefix-closed languages, i.e., we can
reduce checking whether
$\mathit{Reach}_{\hat{M}}(\mathit{Pref}(\hat{\mathord{\operatorname{\text{L}}_{!}}}))$
is infinite to checking whether
$\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\text{V}\rrangle)$
is infinite for some $\mathcal{C}$ and prefix-closed language V. The latter is
decidable as we establish in the following. Recall that, by the construction
of $\mathcal{C}$, we then have
$\textit{Reach}_{\mathcal{C}}=\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathit{Pref}(\text{V})\rrangle)=\mathit{Reach}_{\mathcal{C}}(L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\text{V}\rrangle)$.

The main idea that follows is the reduction of unboundedness of the counter
machine to reachability in a modified counter machine. It is not immediate
that we can use the results in the literature (for example [DF97]) which
reduce boundedness to reachability in Petri nets/VASS. This is because the
property of monotonicity does not extend to zero tests; if one can execute a
zero test at $(q,\mathbf{v})$, it is not necessarily the case that it can be
executed at $(q,\mathbf{v}^{\prime})$ with
$\mathbf{v}\leq\mathbf{v}^{\prime}$, where we let
$\mathbf{v}\leq\mathbf{v}^{\prime}$ if
$\mathbf{v}_{x}\leq\mathbf{v}^{\prime}_{x}$ for all $x\in\mathit{Cnt}$.
However, we show that, for the counter machine that we construct from the FIFO
machine, this property does hold. If we are able to show this, the
constructions used in the case of VASS can be adapted.

######  Lemma 16.

For every execution in $\mathcal{C}$ of the form
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
such that $\mathbf{v}\leq\mathbf{v}^{\prime}$, the following holds: The only
counters that are tested to zero during $\sigma^{\prime}$ already evaluate to
zero at $(q,\mathbf{v})$, and do not change their value throughout the
execution of $\sigma^{\prime}$.

######  Proof 5.2.

Let us assume to the contrary that there is at least one counter which is
incremented or decremented during $\sigma^{\prime}$ and also tested to zero
during the execution. Without loss of generality, let us consider $x_{(c,i)}$
to be the first counter along the execution $\sigma^{\prime}$ that is tested
to zero during $\sigma^{\prime}$ and also incremented/decremented before it
was tested to zero.

  * •

Case (1): It has a non-zero value at $(q,\mathbf{v})$, and is then either
decremented, or first incremented and then decremented, and finally tested to
zero. Since we know that $\sigma.\sigma^{\prime}\in
L_{\mathcal{C}}^{\textsf{{zero}}}$, no counter tested to zero can then be
incremented. Hence, its value will remain zero. But this is a contradiction to
our assumption that $\mathbf{v}\leq\mathbf{v}^{\prime}$. Hence, all the
counters with non-zero values at $(q,\mathbf{v})$ cannot be tested to zero
during $\sigma^{\prime}$.

  * •

Case (2): It has value zero in $(q,\mathbf{v})$, and is incremented, then
decremented, then tested to zero during $\sigma^{\prime}$. This implies that
it first has to be incremented. Consider now some sub-execution
$\sigma^{\prime\prime}\in\mathit{Pref}(\sigma^{\prime})$ where
$(q,\mathbf{v})\xrightarrow{\sigma^{\prime\prime}}(q_{1},\mathbf{v}_{1})$ such
that the value of $x_{(c,i)}$ in the configuration $(q_{1},\mathbf{v}_{1})$ is
non-zero. Since there are no “new” zero-tests along the execution
$\sigma^{\prime\prime}$ (by our assumption), we can execute
$\sigma^{\prime\prime}$ from $(q,\mathbf{v}^{\prime})$ (by the monotonicity
and trace property). However, we cannot increment the counter $x_{(c,i)}$
along $\sigma^{\prime\prime}$, because it was tested to zero during the run
$(q_{0},\bm{0})\mathrel{\smash{\xrightarrow{\sigma.\sigma^{\prime}}}}(q,\mathbf{v}^{\prime})$.
Hence, we once again have a contradiction.

Now, we can use results from [FS01] to show the following:

######  Proposition 17.

The set $\textit{Reach}_{\mathcal{C}}$ is infinite iff there exist
$\sigma,\sigma^{\prime}\in A_{\mathcal{C}}^{\ast}$, $q\in Q$, and
$\mathbf{v},\mathbf{v}^{\prime}\in\mathbb{N}^{\mathit{Cnt}}$ such that
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
and $\mathbf{v}<\mathbf{v}^{\prime}$ (i.e.,
$\mathbf{v}\leq\mathbf{v}^{\prime}$ and $\mathbf{v}\neq\mathbf{v}^{\prime}$).

######  Proof 5.3.

Let us assume that $\textit{Reach}_{\mathcal{C}}$ is infinite. As in [FS01],
we consider the tree of all prefixes of computations. We prune this tree by
removing all prefixes where there is at least a loop, i.e., containing two
nodes that are labeled by the same configuration. Since every reachable
configuration can be reached without a loop, we still have an infinite number
of prefixes in the pruned tree. For every configuration $(q,\mathbf{v})$ in
the tree, there are finitely many successors (as the transition system is
finitely branching). Hence, in order for the tree to be infinite, there is at
least one infinitely long execution (by König’s lemma). This execution has no
loop. Therefore, by Dickson’s lemma, there is an infinite subsequence of
configurations $(q_{1},\mathbf{v}_{1})$, $(q_{2},\mathbf{v}_{2}),\ldots$ such
that $\mathbf{v}_{1}<\mathbf{v}_{2}<\ldots$. Once we extract this sequence,
since there are only finitely many control states in $Q$, we know that there
is at least one pair $(q,\mathbf{v}),(q,\mathbf{v}^{\prime})$ such that
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
and $\mathbf{v}<\mathbf{v}^{\prime}$.

Conversely, let us assume that there is an execution
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
such that $\mathbf{v}<\mathbf{v}^{\prime}$. We know from Lemma 16 that the
only counters which may be tested for zero during $\sigma^{\prime}$ already
evaluate to zero at $(q,\mathbf{v})$, and do not change their value throughout
the execution of $\sigma^{\prime}$. Therefore, all the transitions of the
counter system in $\sigma^{\prime}$ can be considered as VASS operations.
Hence, the property of monotonicity holds, i.e., if
$(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$ and
$(q,\mathbf{v})<(q,\mathbf{v}^{\prime})$, then we know there exists an
infinite sequence $\mathbf{v}_{1}<\mathbf{v}_{2}<\ldots$ reachable from
configuration $(q,\mathbf{v}^{\prime})$.

#### Construction of modified counter system.

We modify the counter system $\mathcal{C}$ and construct a new counter system
$\mathcal{C^{\prime}}$ such that $\textit{Reach}_{\mathcal{C}}$ is infinite
iff a specific configuration is reachable in $\mathcal{C^{\prime}}$. The
construction is loosely based on the reduction of boundedness to reachability
for Petri Nets in [DF97].

######  Proposition 18.

We can effectively construct a counter machine $\mathcal{C^{\prime}}$ (with
bounded zero tests) and a finite set of configurations $R\subseteq
S_{\mathcal{C^{\prime}}}$ such that $\textit{Reach}_{\mathcal{C}}$ is infinite
iff some configuration from $R$ is reachable in $\mathcal{C^{\prime}}$.

######  Proof 5.4.

We modify the counter machine $\mathcal{C}$ and construct a new counter
machine $\mathcal{C^{\prime}}$ such that $\textit{Reach}_{\mathcal{C}}$ is
infinite iff a configuration belonging to a finite set is reachable in
$\mathcal{C^{\prime}}$. The construction is loosely based on the reduction of
boundedness to reachability for Petri Nets in [DF97]. Since we do not know the
values of $\mathbf{v}$ and $\mathbf{v}^{\prime}$ a priori, we will try to
characterize the general condition. The difference
$\mathbf{v}^{\prime}-\mathbf{v}$ is a non negative vector, with at least one
strictly positive component. We add a duplicate set of counters for every
counter in the system. The intuition is that the counter machine non-
deterministically moves from operating on both sets to a configuration from
where it only operates on this second set. The first set will remain unchanged
(with the value $\mathbf{v}$), and the second set will keep track of the
values (until it reaches $\mathbf{v}^{\prime}$). From this configuration
(which represents $(q,\mathbf{v}^{\prime})$), we move to a new control state,
$q_{\textsf{reach}}$. Here, we check for the condition
$\mathbf{v}^{\prime}-\mathbf{v}>\bm{0}$ by first decrementing each counter in
the first set which has a non-zero value in tandem with the corresponding
counter in the second set. We do this until all the counters in the first set
are equal to zero. If $\mathbf{v}^{\prime}-\mathbf{v}>\bm{0}$, then there is
at least one counter in the second set with a non-zero counter value. We non-
deterministically decrement all the counters in the second set until we reach
a configuration that has some counter $c$ in the second set with a value of
$1$, and all other counters evaluate to zero. Since there are finitely many
such configurations, we can just check every case.

From the above results, we have the following theorem.

######  Theorem 19.

The IB unboundedness problem is decidable for FIFO machines.

######  Remark 20.

Gouda et al, stated that unboundedness is in EXPSPACE for letter-bounded
systems [GGLR87]. However, they only give an idea of the proof, stating that
it can be done in a similar fashion as for the deadlock problem. In the
construction for solving the deadlock problem, they reduce the input language
to _tally_ letter-bounded languages (tally means that the input-language is
included in $a^{*}$ where $a$ is a letter). They add as many channels as
letters in the original letter-bounded-language. Furthermore, in order to
ensure that no channel is non-empty before the next channel is read, they
ensure that in all control states where a later channel is being read, there
are reception transitions of previous channel contents which lead to a sink
state (where there is never a deadlock). Notice that it is still possible to
leave a channel non-empty before the next channel is read. But one never
reaches a deadlock in such an “incorrect” run, since there is always the
option of reading the unread channel contents of the previous channels and
reach the sink state.

However, when we consider this model for unboundedness, there may exist
unbounded “incorrect” runs since we can leave a channel non-empty and proceed
to the next and may have an unbounded run there. Hence, it seems that one
still needs some reachability test to check if the runs are correct because we
cannot ensure that some channels are zero in an unbounded run.

### Termination

For termination, we take a similar approach as for unboundedness. Suppose
again that we are given $\hat{M}$ and $\hat{\operatorname{\text{L}}}$, the
associated FIFO machine ${M}$ in normal form (with the corresponding tuple
$\operatorname{\text{L}}$ of distinct-letter languages), and the associated
counter machine $\mathcal{C}$. We first show that the normal form preserves
the (non-)termination property. In the following, $\beta_{i}$ will denote a
send or receive action and $\alpha_{i}$ will denote an increment or decrement
action.

We obtain the following equivalence.

######  Proposition 21.

The following statements are equivalent:

  * •

There is an infinite execution of the form
$\mathit{init}_{\hat{M}}\xrightarrow{\smash{\beta_{1}}}_{\hat{M}}s_{1}\xrightarrow{\smash{\beta_{2}}}_{\hat{M}}s_{2}\xrightarrow{\smash{\beta_{3}}}_{\hat{M}}\ldots$
such that, for all $i\in\mathbb{N}$, we have
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$.

  * •

There is an infinite execution of the form
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
such that, for all $i\in\mathbb{N}$, we have
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$.

######  Proof 5.5.

Assume that there is an infinite execution of the form
$\mathit{init}_{\hat{M}}\xrightarrow{\smash{\hat{\beta}_{1}}}_{\hat{M}}\hat{s}_{1}\xrightarrow{\smash{\hat{\beta}_{2}}}_{\hat{M}}\hat{s}_{2}\xrightarrow{\smash{\hat{\beta}_{3}}}_{\hat{M}}\ldots$
in $\hat{{M}}$ such that, for all $i\in\mathbb{N}$, we have
$\hat{\beta}_{1}\ldots\hat{\beta}_{i}\in\mathit{Pref}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$.
Hence, there are $\beta_{1},\beta_{2},\beta_{3},\ldots\in A_{M}$ such that,
for all $i\in\mathbb{N}$, letting $\sigma_{i}=\beta_{1}\ldots\beta_{i}$, we
have $h(\sigma_{i})=\hat{\beta}_{1}\ldots\hat{\beta}_{i}$ and
$\sigma_{i}\in\mathit{Pref}(\text{V})$. Hence, we know that, in the FIFO
machine $h^{-1}({\hat{M}})$, one has
$(\hat{q}_{0},\bm{\varepsilon})\xrightarrow{\smash{\beta_{1}}}(\hat{q}_{1},\mathbf{w}_{1})\xrightarrow{\smash{\beta_{2}}}(\hat{q}_{2},\mathbf{w}_{2})\xrightarrow{\smash{\beta_{3}}}\ldots$
for suitable $(\hat{q}_{i},\mathbf{w}_{i})$ (by construction of
$h^{-1}({\hat{T}})$), and that $\sigma_{i}\in\mathit{Pref}(L(\mathcal{A}))$.
Therefore, since ${M}$ is a product of the two machines, we can deduce that
there is an infinite execution
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
as required.

Conversely, assume that there is an infinite execution of the form
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
such that, for all $i\in\mathbb{N}$, we have
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$.
Let $\hat{\sigma_{i}}=h(\beta_{1}\ldots\beta_{i})$ for all $i\in\mathbb{N}$.
Since
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$,
we have $\mathit{proj}_{c!}(\beta_{1}\ldots\beta_{i})\in\mathit{Pref}(L_{c})$
for all $c\in\mathit{Ch}$. In particular,
$\mathit{proj}_{c!}(\beta_{1}\ldots\beta_{i})\in
h_{c}^{-1}(\mathit{Pref}(\hat{L}_{c}))$ and, therefore,
$h_{c}(\mathit{proj}_{c!}(\beta_{1}\ldots\beta_{i}))=\mathit{proj}_{c!}(h(\beta_{1}\ldots\beta_{i}))\in\mathit{Pref}(\hat{L}_{c})$.
We deduce
$\hat{\sigma_{i}}\in\mathit{Pref}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$.
Furthermore, we can execute $\hat{\sigma}$ in $\hat{{M}}$ (by construction)
for all $i\in\mathbb{N}$. Hence, we can build an infinite execution in
$\hat{M}$, such that
$\hat{\sigma_{i}}\in\mathit{Pref}(\hat{\mathord{\operatorname{\text{L}}_{!}}})$
for all $i\in\mathbb{N}$.

The latter property can be reduced to checking a decidable property in the
counter machine as follows:

######  Proposition 22.

The following statements are equivalent:

  * •

There is an infinite execution of the form
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
such that, for all $i\in\mathbb{N}$, we have
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$.

  * •

There is an infinite execution of the form
$\mathit{init}_{\mathcal{C}}\xrightarrow{\smash{\alpha_{1}}}_{\mathcal{C}}s_{1}\xrightarrow{\smash{\alpha_{2}}}_{\mathcal{C}}s_{2}\xrightarrow{\smash{\alpha_{3}}}_{\mathcal{C}}\ldots$
such that, for all $i\in\mathbb{N}$, we have $\alpha_{1}\ldots\alpha_{i}\in
L_{\mathcal{C}}^{\textsf{{zero}}}\cap\llangle\mathit{Pref}(\text{V})\rrangle$.

  * •

There exist $\sigma\in A_{\mathcal{C}}^{\ast}$, $\sigma^{\prime}\in
A_{\mathcal{C}}^{+}$, $(q,\mathbf{v})\in S_{\mathcal{C}}$, and
$\mathbf{v}^{\prime}$ such that
$(q_{0},\bm{0})\xrightarrow{\sigma}_{\mathcal{C}}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}_{\mathcal{C}}(q,\mathbf{v}^{\prime})$
and $\mathbf{v}\leq\mathbf{v}^{\prime}$.

######  Proof 5.6.

The equivalence of the first two items is obtained as a corollary of
Propositions 7 and 8. So let us show that the latter two are equivalent.

Consider a non-terminating execution as described above. By Dickson’s lemma,
there is an infinite subsequence of configurations
$(q_{1},\mathbf{v}_{1}),(q_{2},\mathbf{v}_{2}),\ldots$ such that
$\mathbf{v}_{1}\leq\mathbf{v}_{2}\leq\ldots$. Once we extract this sequence,
since there are only finitely many control states in $Q$, we know that there
is at least one pair $(q,\mathbf{v}),(q,\mathbf{v}^{\prime})$ such that
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
and $\mathbf{v}\leq\mathbf{v}^{\prime}$.

Conversely, assume
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
and $\mathbf{v}\leq\mathbf{v}^{\prime}$. From the same argument as for
boundedness, we can deduce that no counter is being tested to zero for the
first time in $\sigma^{\prime}$ and all the counters previously tested stay
unchanged. Hence, all the transitions of the counter system in
$\sigma^{\prime}$ can be considered as VASS operations. Therefore, we know
there exists $\mathbf{v}^{\prime\prime}$ such that
$(q,\mathbf{v}^{\prime})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime\prime})$
and $\mathbf{v}^{\prime}\leq\mathbf{v}^{\prime\prime}$. Repeating this
reasoning, we can build an infinite sequence starting from
$(q,\mathbf{v}^{\prime})$.

Finally, we construct a modified counter machine as in the case for
boundedness (Proposition 18) and get the following:

######  Proposition 23.

We can effectively construct a counter machine $\mathcal{C}^{\prime\prime}$
(with bounded zero tests) and a configuration $s\in
S_{\mathcal{C^{\prime\prime}}}$ such that the following statements are
equivalent:

  * •

There exist $\sigma\in A_{\mathcal{C}}^{\ast}$, $\sigma^{\prime}\in
A_{\mathcal{C}}^{+}$, $(q,\mathbf{v})\in S_{\mathcal{C}}$, and
$\mathbf{v}^{\prime}$ such that
$(q_{0},\bm{0})\xrightarrow{\sigma}_{\mathcal{C}}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}_{\mathcal{C}}(q,\mathbf{v}^{\prime})$
and $\mathbf{v}\leq\mathbf{v}^{\prime}$.

  * •

Configuration $s$ is reachable in $\mathcal{C}^{\prime\prime}$.

######  Proof 5.7.

We can adapt the construction of $\mathcal{C}^{\prime}$ for unboundedness. The
difference is that we now allow for $\mathbf{v}=\mathbf{v}^{\prime}$. Hence,
there is no need anymore to check that, after decrementing both sets of
counters in tandem, there is still a positive counter left in the second set.
We can therefore also empty the second set of counters in a new control-state
$q$ and check whether $(q,\bm{0})$ is reachable.

Thus, we have the following theorem.

######  Theorem 24.

The IB termination problem is decidable for FIFO machines.

##  6\. Output-Bounded Problems

We consider the dual case of input-bounded languages in which the set of words
that may be received by each channel (the output-language) is constrained to
be bounded. The _OB problems_ are defined as follows:

[OB decision problems]

Given a FIFO machine ${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$ (each given in terms of a
finite automaton), a control state $q\in Q$, a configuration $s\in S_{M}$, and
a rational relation
$\text{R}\subseteq\prod_{c\in\mathit{Ch}}\Sigma_{c}^{\ast}$.

  * •

_OB rational reachability_ : Do we have
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{?}})$
for some $\mathbf{w}\in\text{R}$?

  * •

_OB reachability_ : Do we have
$s\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{?}})$ ?

  * •

_OB control-state reachability_ : Do we have
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{?}})$
for some $\mathbf{w}$ ?

  * •

_OB deadlock_ : Does
$\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{?}})$ contain a
deadlock ?

  * •

_OB unboundedness_ : Is
$\mathit{Reach}_{{M}}(\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}}))$
infinite?

  * •

_OB termination_ : Is there no infinite execution of the form
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
such that, for all $i\in\mathbb{N}$, we have $s_{i}\in S_{M}$, $\beta_{i}\in
A_{{M}}$, and
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{?}})$?

######  Theorem 25.

OB reachability is decidable for FIFO machines.

######  Proof 6.1.

Given a configuration $(q,\mathbf{w})$ in ${M}$, and a tuple of bounded
languages $\operatorname{\text{L}}$, the output-bounded reachability problem
asks if $(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\operatorname{\text{L}}_{?})$.
Since the output language is in $\operatorname{\text{L}}_{?}$, we know that
the contents of the channels which have already been read is in the
corresponding input-language, i.e., $\operatorname{\text{L}}_{!}$. Therefore,
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\operatorname{\text{L}}_{?})$ iff
$(q,\mathbf{w})\in\mathit{Reach}_{{M}}(\mathop{\operatorname{\text{L}}_{!}^{\prime}})$
where $\mathop{\operatorname{\text{L}}\hskip
0.09995pt^{\prime}}=(L^{\prime}_{c})_{c\in\mathit{Ch}}$ and
$L^{\prime}_{c}=L_{c}.\mathbf{w}_{c}$. Hence, the OB reachability problem is
decidable for FIFO machines.

######  Theorem 26.

OB control-state reachability is decidable for FIFO machines.

######  Proof 6.2.

In order to show that OB control-state reachability is decidable for FIFO
machines, we first convert it to the normal form. This construction is similar
to that as specified in Section 3, however we make a few changes. Firstly,
when we change the alphabet to distinct letter, we add an additional letter,
say $\$$, to represent all the letters which are not present in the bounded
language, but are present in the transitions of the FIFO system. Then, in
addition to the transitions we already add to the new FIFO system as in
Section 3, for every send action in the original FIFO system, we add a send
action with this new letter $\$$. However, for the reception, we leave it as
before. This new FIFO system can now only read letters in the output language,
however, it can potentially send any letter. Hence, we have only restricted
the output language.

Next, to the automata that is constructed to accept the bounded language for
send actions, we add to all the states a transition that enables the automata
to send $\$$ and go to a sink state which loops with send actions sending
$\$$. Hence, once again, we have ensured that the input language is not
restricted. To the reception automata, we make no such changes. Hence, the
reception automata only accept the bounded language.

In this new machine, we can solve for control state reachability, over the
input-language $\mathop{\operatorname{\text{L}}\hskip
0.09995pt^{\prime}}=(L^{\prime}_{c})_{c\in\mathit{Ch}}$ such that
$L^{\prime}_{c}=L_{c}.\$^{\ast}$ (but we let the output-language remain
$\operatorname{\text{L}}$ when we construct the trimmed automata). If a
configuration $(q,\mathbf{w})$ is reachable in this new machine, then there
exists a path which can be taken in the original machine to reach control
state $q$ via $\sigma\in\mathord{\operatorname{\text{L}}_{?}}$. Furthermore,
if there is a path which can be taken in the original machine, it can also be
taken in the new machine. Hence, we can decide if there exists a $\mathbf{w}$
such that $(q,\mathbf{w})$ is reachable.

######  Theorem 27.

OB unboundedness and OB termination problems are decidable for FIFO machines.

######  Proof 6.3.

We can decide the OB unboundedness and termination problems as well. We can
construct a counter system for the normal form described in the proof of
Theorem 26. Note that the counter corresponding to $\$$ will only have
increments and no decrements, which is in line with the fact that the contents
corresponding to this counter do not belong to the output-language. The FIFO
machine has an infinite run iff this newly constructed counter machine has
also an infinite run. We then construct the modified counter machine, as is
the case for boundedness (see Section 5), and test if there is a run
$(q_{0},\bm{0})\xrightarrow{\sigma}(q,\mathbf{v})\xrightarrow{\sigma^{\prime}}(q,\mathbf{v}^{\prime})$
such that $\mathbf{v}<\mathbf{v}^{\prime}$. Since this modified counter system
has bounded zero tests (the added counter has no decrements or zero tests
associated to it), we can decide the reachability of the configuration, and
hence, decide if the FIFO machine is unbounded. A similar explanation can be
made for termination.

######  Remark 28.

The rational reachability problem cannot be directly reduced to the input-
bounded case. For the output bounded case, we do not know precisely the
reachability set, since we only restrict the output-language. Hence, in order
to check if some $\mathbf{w}\in\text{R}$ is reachable, we need to be able to
compute the reachability set. Similarly, unlike the input-bounded case, we
cannot determine the deadlock problem a priori, since the deadlock problem is
reduced to rational reachability for the input-bounded case. Hence, these two
problems have been left open.

##  7\. FIFO Machines with a Single Channel

When we restrict the communication to a single channel, we obtain better upper
bound for reachability.

#### Upper bound for reachability: EXPTIME

We consider the model of ordered multi-pushdown systems, studied in [ABH17].
We define it using our counter systems. A counter system can be seen as a
multi-pushdown system with a unary alphabet. Unary ordered multi-pushdown
systems (UOMPDSs) are multi-pushdown systems which impose a total order on the
counters and limit decrements to the lowest non-empty counter. We use the
following result of reachability of UOMPDS.

######  Theorem 29 ([AKS14], Theorem 13).

The reachability problem in UOMPDS is solvable in EXPTIME.

Consider the counter machine $\mathcal{C}$ with the semantic restriction
$L_{\mathcal{C}}^{\textsf{{zero}}}$ which can be built from a single channel
FIFO machine ${M}$. We see that a counter $x_{i}$ can only be decremented if
the previous counters $x_{j}$ such that $j<i$ are equal to zero. Therefore,
the counter system $\mathcal{C}$ is a UOMPDS, where the order of the counters
is defined as $x_{i}<x_{j}$ iff $i<j$. Hence, we have the following
proposition.

######  Proposition 30.

IB reachability in single channel FIFO machines is polynomially reducible to
reachability in UOMPDS.

In [AKS14], it was also shown that repeated reachability for UOMPDS is
solvable in EXPTIME. We know that a system is non-terminating if and only if
we can reach any control state infinitely often. Therefore, we can guess a
control state and verify if it is reachable repeatedly in order to verify if
the system is non-terminating. Furthermore, we see that even for FIFO machines
with a single channel, using the same construction as in Proposition 12,
reachability and control state reachability are recursively equivalent.

We then have the following corollary.

######  Corollary 31.

The IB reachability, termination and control-state reachability problems are
in EXPTIME for FIFO machines with a single channel.

However, for the unboundedness result in Section 5, we use the reachability
for counter systems with bounded zero tests. Furthermore, the set of all
counters in the modified counter system do not have a total order anymore.
Hence, following our constructions, we may only say that the unboundedness
problem in FIFO machines with a single channel (over a bounded language) is
solvable by using the Petri net reachability (which is tower-hard).

######  Remark 32.

In the case of a single channel, we have a total order on the counters, and
therefore we are able to use results from Ordered Multipushdown Systems.
However, even when we consider two channels, we cannot immediately extend
these results since there is no longer a total order in the decrement of
counters.

#### Lower bound for reachability: NP-hard

We consider a sub-problem of the IB reachability, unboundedness, and
termination problems as follows. Recall that, given a bounded language
$L=w_{1}^{\ast}\ldots w_{n}^{\ast}$, if $|w_{1}|=\cdots=|w_{n}|=1$, i.e.,
$w_{1},\ldots,w_{n}\in A$, then $L$ is called a letter-bounded language.

[ILB-decision problems] Given a FIFO machine
${M}=(Q,\mathit{Ch},\Sigma,T,q_{0})$, a control-state $q\in Q$, a
configuration $s\in S_{M}$, and a tuple
$\operatorname{\text{L}}=(L_{c})_{c\in\mathit{Ch}}$ of non-empty regular
letter-bounded languages $L_{c}\subseteq\Sigma_{c}^{\ast}$.

  * •

_ILB-reachability_ : Do we have
$s\in\mathit{Reach}_{{M}}(\mathord{\operatorname{\text{L}}_{!}})$ ?

  * •

_ILB-unboundedness_ : Is
$\mathit{Reach}_{{M}}(\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}}))$
infinite?

  * •

_ILB-termination_ : Is there no infinite execution of the form
$\mathit{init}_{M}\xrightarrow{\smash{\beta_{1}}}_{M}s_{1}\xrightarrow{\smash{\beta_{2}}}_{M}s_{2}\xrightarrow{\smash{\beta_{3}}}_{M}\ldots$
such that, for all $i\in\mathbb{N}$, we have $s_{i}\in S_{M}$, $\beta_{i}\in
A_{{M}}$, and
$\beta_{1}\ldots\beta_{i}\in\mathit{Pref}(\mathord{\operatorname{\text{L}}_{!}})$?

We see that most of the properties are NP-hard for FIFO machines with a single
channel over a letter-bounded language. This is proved by simulating 3-CNF
formula with such machines. Our simulation follows the same ideas as the proof
of NP-hardness for flat FIFO machines with _multiple_ channels [EGM12, FP19],
except that we use a unique channel.

######  Theorem 33.

ILB-reachability, ILB-unboundedness, and ILB-non-termination are NP-hard for
machines with a single channel, even when the input language is letter
bounded.

######  Proof 7.1.

We reduce from 3SAT. Given a 3-CNF formula $C_{1}\land\ldots\land C_{m}$ over
variables $x_{1},\ldots,x_{n}$, we construct a FIFO machine with one channel.
The message alphabet has $2n+1$ letters and is as follows
$\Sigma_{\\#}=\Sigma\uplus\\{\\#\\}$, where
$\Sigma=\\{\mathsf{1},\ldots,\mathsf{n}\\}\uplus\\{\bar{\mathsf{1}},\ldots,\bar{\mathsf{n}}\\}$.
The FIFO machine consists of the gadgets shown below. The gadget for variable
$x_{k}$ adds either $\mathsf{k}$ (in the top transition) or $\bar{\mathsf{k}}$
(in the bottom edge) to the channel. At the end of this gadget, the channel
will have either $\mathsf{k}$ or $\bar{\mathsf{k}}$. We will sequentially
compose the gadgets for all variables. Starting from the initial control state
of the gadget for variable $x_{1}$, we reach the final control state of the
gadget for variable $x_{n}$, such that for every variable $x_{k}$ we either
have $\mathsf{k}$ or $\bar{\mathsf{k}}$ in the channel — and this determines
the truth valuation.

We then add the gadget that adds the stop symbol to the channel, as shown in
Figure 5.

$!\mathsf{k}$$!\bar{\mathsf{k}}$$!\\#$ (a) Gadget for variable $x_{k}$ (b)
Gadget for stop marker Figure 5. Gadget for variables

Next, we add gadgets for the clauses. The gadget for the example clause
$C_{1}=x_{1}\lor\neg x_{2}\lor\neg x_{3}$ (gadgets for other clauses follow
similar pattern) is shown in Figure 6. The gadget checks that the channel has
either $\mathsf{1}$ (in the top path) or has $\bar{\mathsf{2}}$ (in the middle
path) or has $\bar{\mathsf{3}}$ (in the bottom path). We append the clause
gadgets to the end of the variable gadgets one after the other. All clauses
are satisfied by the truth valuation determined by the contents of channels
$x_{1},\ldots,x_{n}$ iff we can reach the last control state of the last
clause.

The gadget for cleaning up all the variables is shown below (it receives all
the letters from the channel). We append the cleanup gadget to the end of the
clause gadget for $C_{m}$.

$\varepsilon$$\varepsilon$$\varepsilon$$?\mathsf{a}!\mathsf{a}$$?\mathsf{1}!\mathsf{1}$$?\mathsf{a}!\mathsf{a}$$?\\#!\\#$$?\mathsf{a}!\mathsf{a}$$?\bar{\mathsf{2}}!\bar{\mathsf{2}}$$?\mathsf{a}!\mathsf{a}$$?\\#!\\#$$?\mathsf{a}!\mathsf{a}$$?\bar{\mathsf{3}}!\bar{\mathsf{3}}$$?\mathsf{a}!\mathsf{a}$$?\\#!\\#$$?\Sigma_{\\#}$
(a) Gadget for clause $C_{1}=x_{1}\lor\neg x_{2}\lor\neg x_{3}$ (b) Gadget for
cleanup Figure 6. Gadget for clauses (the loop labelled
$?\mathsf{a}!\mathsf{a}$ represents loops for all $\mathsf{a}\in\Sigma$)

Note that in the FIFO machine given above, every gadget can only be visited
once, and the input language of each gadget for a variable $x_{k}$ is equal to
$\\{\mathsf{k},\bar{\mathsf{k}}\\}$ which is included in the letter-bounded
language $\mathsf{k}^{*}\bar{\mathsf{k}}^{*}$. Hence, for every execution
$\sigma$ along the sequence of variable gadgets, we have
$\sigma\in\mathord{\operatorname{\text{L}}_{!}}$ where
$\operatorname{\text{L}}=\mathsf{1}^{*}\bar{\mathsf{1}}^{*}\ldots\mathsf{n}^{*}\bar{\mathsf{n}}^{*}\\#^{*}$.