Verifying lossy channel systems has nonprimitive recursive complexity.
Lossy channel systems are systems of finite state automata that communicate via unreliable unbounded fifo channels. It is known that reachability, termination and a few other verification problems are decidable for these systems. In this article we show that these problems cannot be solved in primitive recursive time.
Introduction
Channel systems, also called Finite State Communicating Machines, are systems of nite state
automata that communicate via asynchronous unbounded fo channels [Boc78, BZ83]. Figure
1 displays an example, where the labels c!x and c?x mean that message x (a letter) is sent
to (respectively read from) channel c. Channel systems are a natural model for asynchronous
channel c 1
b a a b a
channel c 2
a c

Figure

1: A channel system with two automata and two channels
communication protocols and constitute the semantical basis for ISO protocol specication
languages such as SDL and Estelle. Channel systems are Turing powerful, and no verication
method for them can be general and fully algorithmic.
A few years ago, Abdulla and Jonsson identied lossy channel systems as a very interesting
model: in lossy channel systems messages can be lost while they are in transit, without
any notication. These systems are very close to the completely specied protocols independently
introduced by Finkel, and for which he showed the decidability of termination.
Abdulla and Jonsson showed that reachability, safety properties over traces, and eventuality
properties over states are decidable for lossy channel systems. The decidability results
of [Fin94, CFP96, AJ96b] are fundamental since lossy systems are the natural model for
fault-tolerant protocols where the communication channels are not supposed to be reliable
(see [AKP97, ABJ98, AAB99] for applications).
For lossy channel systems, the aforementioned decidability results lead to algorithms whose
termination rely on Higman's Lemma (see [A
CJT00, FS01] for more examples of this phe-
nomenon). No complexity bound is known and, e.g., Abdulla and Jonsson stated in [AJ96b]
that they could not evaluate the cost of their algorithm.
In this article we show that all the above-mentioned decidable problems have nonprimitive
recursive complexity, i.e., cannot be solved by algorithms with running time bounded by a
primitive recursive function of their input size. This puts these problems among the hardest
decidable problems.
Our proof relies on a simple construction showing how lossy channel systems can weakly
compute some fast growing number-theoretic functions A related to Ackermann's
function and their inverses A 1
\weakly computing f" we mean that, starting
from x, all values between 0 and f(x) can be obtained. This notion was used by Rabin in his
proof that equality of the reachability sets of Petri nets is undecidable, a proof based on the
weak computability of multivariate polynomials (see [Hac76]). Petri nets can weakly compute
the A n functions (see [MM81]) but they cannot weakly compute their inverses A 1
n as lossy
channel systems can do.
There exist other families of systems that can weakly compute both A n and A 1
lossy counter machines of [May00], or the reset nets of [DFS98, DJS99]. Our construction can
easily be adapted to show that, for these systems too, decidable problems like termination,
control-state reachability, . , are nonprimitive recursive.
Finally, let us observe that there does not exist many uncontrived problems that have been
shown decidable but not primitive recursive. In the eld of verication, we are only aware
of one instance: the \nite equivalence problem for Petri nets" 1 introduced by Mayr and
Meyer [MM81]. This problem is, given two Petri nets, to decide whether they both have the
same set of reachable markings and this set is nite (equivalence is undecidable without the
niteness assumption). It can be argued that the verication (termination or reachability) of
lossy channel systems is a less contrived problem.
Channel systems, from perfect to lossy
A channel system usually combines several nite-state automata that communicate through
several channels. Here, and without loss of generality, we assume our systems only have one
1 See [Jan01] for a more general proof that all nite equivalence problems for Petri nets are nonprimitive
recursive.
automaton that uses its several channels as fo buers.
Formally, a channel system is a tuple is a nite set of
control states, is a nite set of channels, is a nite alphabet
of messages, and   Q C  f?; !g    Q is a nite set of transition rules (see below).
A conguration of S is a tuple
denoting that control is currently in
state q, while channels c 1 to c k contain words w (from   ).
The transition rules in  state how S can move from a conguration to another. For-
mally, S has a \perfect" step
is some hq; w
0 is some
and (3.1) there is a rule (q; c
has been written to the tail of c i ) or (3.2) there is a rule (q; c
has been read from the head of c i ). These steps are called perfect because no message is lost.
It is well known that, assuming perfect steps, channel systems can faithfully simulate
Turing machines in quadratic time [BZ83] (a single channel is enough to replace a Turing
machine work tape; reading and writing in the middle of the channel requires rotating the
content of the channel for positioning reasons, hence the quadratic overhead). Thus all
interesting verication problems are undecidable for systems with perfect channels, even when
restricted to single-channel systems.
2.1 Lossy systems
The most elegant and convenient way to model lossy channel systems is to see them as channel
systems with an altered notion of steps [AJ96b].
We write u v v when u is a subword of v, i.e. u can be obtained by deleting any number
(including of letters from v. E.g. abba v abracadabra as indicated by the underlining. The
subword ordering extends to congurations: hq; w
Lemma [Hig52], this gives a a well-quasi-ordering:
Lemma 2.1 Every innite sequence
congurations contains an innite increasing
subsequence
When
we write

0 and say that S may evolve from
to
0 by losing messages.
The steps of a lossy channel system are all
congurations - 0 (i.e. losses may occur before and after a perfect step is performed).
Note that a perfect step is a special case of a lossy step. A run is a sequence
of chained lossy steps. A perfect run is a run that uses perfect steps only. We use
and
0 to denote the existence of a nite run (resp. perfect run) that goes from
to
We are interested in the following two problems:
Given a channel system S and an initial conguration
0 , are all runs from
Reachability: Given a channel system S and two congurations
0 and
f , is there a run
from
0 to
Theorem 2.2 [Fin94, AJ96b]. Termination and reachability are decidable for lossy channel
systems.
In the remaining of this note we show
Theorem 2.3 Termination and reachability for lossy channel systems have nonprimitive recursive
complexity.
Theorem 2.3 also applies to the other verication problems that are known decidable for
lossy channel systems. Indeed, termination is an instance of inevitability (shown decidable
in [AJ96b]). Reachability is easily reduced to control-state reachability (shown decidable
in [AJ96b]). Finally, termination can be reduced to simulation with a nite-state system 2
(shown decidable in [AK95, A
CJT00]). Thus we are entitled to claim that \verifying lossy
channel systems has nonprimitive recursive complexity". Note that there exist many undecidable
problems for lossy channel systems [AK95, CFP96, AJ96a, May00, ABPJ00, Sch01].
3 The main construction
3.1 Ackermann's function
Let be the following sequence of functions over the natural numbers:
A
| {z }
times
2. (2)
Thus A n is followed by
A 3
A 4 (a tower of k 2's) (4)
and so on. The A n 's are monotonic and expansive in the following sense: for any n  2 and
We dene inverse functions
Observe that the A 1
n 's are partial functions. Another way to understand these functions is
to notice that
| {z }
times
There exists many versions of Ackermann's function. One possible denition is Ack(n)
A n (2). It is well-known that Ack(n) dominates any primitive recursive function of n. Thus it
follows from classical complexity-theoretic results that halting problems for Turing machines
running in time or space bounded by Ack(n) (n being the size of the input) cannot be decided
in primitive recursive time or space.S terminates i it is not simulation-equivalent with a simple loop.
3.2 Weakly computing A n with expanders
We construct a family . of expanders, channel systems that weakly compute A 2 (k),
A 3 (k), . As illustrated in Fig. 2, E n , the nth expander, uses n channels: c 1 is the \output
channel c n
channel c n 1
channel c 1

Figure

2: Interface for expander E n
channel" (in which the system will write the result A n (k)), c n is the \input channel" (from
which the argument k is read), and channels c 2 to c n 1 are used to store auxiliary results.
E n has one starting and one ending state, called s n and f n respectively.
These systems use a simple encoding for numbers: k 2 N is encoded as a string dke over
the alphabet  0
eg. Formally, dke
k e is made of k letters \1" surrounded by
one \b"egin and one \e"nd marker. For example, the channels in Fig. 2 contain respectively
d0e, . , d0e, and d4e.
Before explaining the construction of the expanders, we describe the simple transferring
devices This illustrates the way encodings dke of numbers are used.
The T n 's, dened in Fig. 3, start in state t n and end in state x n after they have transfered the
contents of channel c 1 into channel c n (assuming c 1 contains at least d1e). In Fig. 3 (and in
future constructions) we sometimes omit depicting all intermediate states when their names
are not required in the proof.

Figure

3: T n , channel system for transferring c 1 into c n (n > 1)
Formally, the lossy behaviors of T n can be characterized by:
Proposition 3.1 For all n  2,
a 1
Proof. Omitted.
Note that the design of T n ensures that it blocks when c 1 contains d0e. This property is
used in the proof of Lemma 3.4.
We now move to the expanders themselves. The internals of E n are given in Fig. 4.

Figure

4: Expanders
For subsystems. This is because E n implements
equation (2): every time a 1 is consumed from c n , run and the result is transfered
(by can be applied again.
It is easy to convince oneself that the perfect (non-lossy) behavior of E n is to compute
A n in the following formal sense:
and
Indeed, for n > 2 a perfect run has the following form (where congurations are displayed in
vector
d0e
d0e
dke
d1e
d0e
dke
d1e
d0e
eb
d1e
d0e
eb
d0e
d1e
eb
d0e
d1e
eb
d0e
eb
d0e
eb
d0e
eb
d0e
eb
d0e
d0e
When perfect behavior is not assumed, E n still computes A n , this time in a weak sense,
according to the following statement:
Proposition 3.2 For all n  2,
a 1  A n (k)
and
Proof. The \(" direction is an easy consequence of (9). A detailed proof of the \)" direction
can be found in the Appendix but the underlying idea is simple: First, if some 1s are lost
at any time during the computation, the nal result will end up being smaller because of the
monotonicity properties (5). Then, if a b or a e marker is lost, the system can never recover
it and will fail to reach a conguration where all channels contain encodings of numbers.
Note that the dierence between (9) and (10) does not only come from the replacement
of a \= A n (k)" by a \ A n (k)": (9) guarantees that the w i s are encodings of numbers, while
assumes this.
3.3 Weakly computing A 1
n with folders
Folder systems F are channel systems that weakly compute the A 1
's. Here channel
c 1 is the input channel and c n is the output, while channels c 2 to c n 1 store auxiliary results.
The denition of the F n 's, given in Fig. 5, is based on (7). It uses transferring systems T 0
these systems are variants of the T n 's and move the contents of channel c n into channel c 1
(instead of the other way around).
When possibly lossy behaviors are considered, F n weakly computes A 1
n in the following
formal sense:
Proposition 3.3 For all n  2,

Figure

5: Folders F
Proof. We prove the \)" direction in the Appendix and omit the easier \(" direction.
One additional property of the construction will be useful in the following:
Lemma 3.4 E n and F n have no innite run, regardless of the initial conguration.
Proof. We rst deal with the E n 's by induction over n. E 2 terminates since its loop consumes
from c 2 . For n > 2, a run of E n cannot visit q n innitely often (this would consume innitely
from c n ) and, by ind. hyp., cannot contain an innite subrun of (obviously, the T n 1
part must terminate too).
For the F n 's, we rst observe (again using induction on n) that, if c 1 contains at least one
1, then a run from s 0
n to f 0
removes strictly more 1's than it writes back. Finally, traversing
must move some 1's to c 1 (or lose them).
4 The hardness results
Expander and folder systems can now be used to prove Theorem 2.3.
4.1 Hardness for reachability
Let's consider a Turing Machine (a TM) M that is started on a blank work tape of size m
(for some m) and that never goes beyond the allocated workspace. One can build a channel
system S that simulates M using as workspace channel c 1 initially lled with b1
e. We do
not describe further the construction of S since it follows the standard simulation of TM's by
channel systems (from [BZ83]) 3 . Since M never goes beyond the allocated workspace, the
3 And since TM's are not really required and could be replaced by perfect channel systems that preserve
the size of the channel contents.
transition rules of S always write exactly as many messages as they read, so that if no loss
occurs the channel always contains the same number of letters. The resulting system has two
types of runs: perfect runs where M is simulated faithfully, and lossy runs that do not really
simulate M but where messages have been irremediably lost.
Now, in order to know whether M accepts in space m, there only remains to provide S
with enough workspace, and to look at runs where no message is lost. This is exactly what
is done by S n
, depicted in Fig. 6, where expander E n provides a potentially large dme in
channel c 1 and folder F n is used to check that no message has been lost.
Simulation of M using c 1
as bounded workspace
start
accept

Figure

simulating Turing machine M with huge workspace
Thus any run of S n
M of the form hs
perfect and
must visit both hstart; dAck(n)e; Hence
Proposition 4.1 hs
accepts in space
Ack(n).
Therefore, since S n
M has size O(n + jM j), reachability for lossy channel systems is at least as
hard as termination for TM's running in Ackermann space. Hence
Corollary 4.2 Reachability for lossy channel systems has nonprimitive recursive complexity.
4.2 Hardness for termination
The second hardness result uses a slight adaptation of our previous construction, and relies
on the following simulation (Fig. 7).
Here S 0n
lls two channels with dAck(n)e: c 1 used as before as working space, and c 0
used as a countdown that ensures termination of the simulation of M . Every time one step
of M is simulated, S 0n
consumes one 1 from c 0 . When the accepting state of M is reached,
M moves to s 0
n where it uses F n to check that c 1 does contain dAck(n)e (i.e. the simulation
was faithful). If the check succeeds, S 0n
can enter a loop. Therefore, a run of S 0n
terminates
when the simulation is not perfect, or when M does not accept in at most Ack(n) steps.
Proposition 4.3 S 0n
M has an innite run from hs n accepts in time
Ack(n).
Proof. Clearly, S 0n
M can only reach the nal loop if the simulation is faithful, and halts
in at most Ack(n) steps. There remains to show that the unfaithful, lossy, behaviors are
deals with the E n and F n part of S 0n
M , the duplication gadget (be-
tween f n and start) obviously terminates, and we solve the problem for the simulation part
by programming it in such a way that the rotation of the tape (necessary for simulating a
(duplicating c 1 in c 0 )
start
loop
Simulation of M using c 1 as bounded
workspace and c 0 as bounded time
accept

Figure

7: S 0n
another simulation of M with huge workspace
TM) cannot induce non-termination. One way 4 to achieve this is to use two copies (one
positive and one negative) of the TM alphabet: in \+" mode, the simulation reads +-letters
and writes back their -twin. Only when an actual TM step is performed does S 0n
from \+" mode to \ " mode and vice versa. More details can be found in section 5 where
the same trick is used.
This shows that termination for lossy channel systems is at least as hard as termination
for TM's runnings in Ackermann time. Hence
Corollary 4.4 Termination for lossy channel systems has nonprimitive recursive complexity.
5 Systems with only one channel
Our construction used several channels for clarity, not out of necessity, and our result still
holds when we restrict ourselves to lossy channel systems with only one channel. This is one
more application of the slogan \lossy systems with k channels can be encoded into lossy systems
with one channel". The encoding given in [AJ96a, Section 4.5] preserves the existence
of runs that visit a given control state innitely often. Below we give another encoding that
further preserves termination and reachability. It uses standard techniques (e.g. from the
study of TM's with k tapes) and the only original aspect is the lossy behavior of our systems.
Consider a system that uses channels c We simulate S by a
system uses one single channel c. Without loss of generality we
assume a dierent subalphabet is used with every channel of S (i.e.  is partitioned in disjoint
alphabets The encoding uses a larger alphabet where k markers #
have been added, and where every letter comes in two copies (a positive and a negative one).
Formally and a pair (x; shortly x  . For
an occurrence of some x  in c means \one x in c i " (and the polarity  is only used
for bookkeeping purposes).
4 An alternative solution would use c0 as a countdown for channel system steps rather than TM steps, but
Prop. 4.3 would have to be reworded in a clumsy way.
A k-tuple hw
k is encoded as
same polarity  is used to label all letters. For example, hab; "; ddci is coded as
under positive polarity.
Fig. 8 shows how two example rules from  (left-hand side) are encoded in S 0 (right-hand
side). On this gure, four loops (marked by ) provide for the rotation of the contents of c
c!x
c?x
c!x
c?x

Figure

8: From S to encoding k channels into one
(with a change of polarity): they are shorthands for several loops as indicated by the \for all
x" comment. A state q from S gives rise to two copies q + and q in positive
letters and writes negative letters, thus preventing non-termination induced by the rotation
loops, q does the converse, and S 0 changes polarity each time a step of S has been simulated.
Now, if W and V are encodings of hw
g.
This extends to lossy behaviors:
S terminates from hq; w
Note that these equivalences only hold for W and V that are correct encodings of k-tuples,
and for q; q 0 that are original states from Q. S 0 has behaviors that do not correspond to
behaviors of S in the sense of (12), e.g. when it gets blocked in new states, or when it loses
one of the # i markers.
Corollary 5.1 Reachability and termination for lossy single-channel systems have nonprimitive
recursive complexity.
6 Conclusion
There exist several constructions in the literature where a problem P is shown undecidable
for lossy channel systems by simulating a Turing machine in such a way that the faithfulness
of the simulation can be ensured, or checked, or rewarded in some way. Our construction
uses similar tricks since it rst builds a nonprimitive recursive number of messages, and later
checks that none has been lost. Still, there are a number of new aspects in our construction,
and this explains why it is the rst complexity result for decidable problems on lossy channel
systems.

Acknowledgements

We are grateful to Alain Finkel who brought this topic to our attention, to Petr Jancar who
suggested major improvements on an earlier draft, and to the anonymous referee who helped
us improve section 5.
A

Appendix

Proof of Prop. 3.2
The di-culty with the \)" direction of Prop. 3.2 is that we have to consider lossy behaviors
that need not respect the logic of the E n systems we designed. However, when we restrict our
attention to behaviors that do not lose the b and e markers, managing the problem becomes
feasible.
We start with the following lemma:
Lemma A.1 If a run hs
is such that every w i
contains one b and one e, then every w i has the form b1  e, i.e. encodes a number.
The same holds for a run ht
Proof. Since our systems always write a b or a e after they consumed one, saying that every
contains one b and one e means that losses did not concern the markers. Therefore, it
only remains to prove that the pattern b1  e is respected, even when some 1's have been lost.
has to consume all of da 1 e and da 2 e and what it writes in c 1 and c 2 encodes a number
even after losses. The same reasoning applies to the channels c 1 and c n of T n , while the other
channels are untouched (and losses there respect the b1  e pattern).
For proceed by induction over n. For c n , observe that all of a n is
consumed and replaced by d0e. For the other channels (c 1 to c n 1 ), they all contain a number
when the run rst reaches q n and, since the lemma holds for
this remains the case every time the run revisits q n , until it eventually reaches f n . Then all
channels contain encodings of numbers.
We are now ready to prove that
a 1  A n (k); and
by induction over n. The base case is left to the reader: a simple inspection of E 2
shows it weakly computes A 2
For n > 2 we consider a run
and isolate the congurations where (14) visits q n and f n 1 by writing it under the form
Since the b and e markers are not lost in (14), we can state that all w i
n have the formk i eb (resp. 1
eb). Since the transition leaving q n for t n 1 consumes one 1 from c n , one sees
that
implying m  k. Finally a can only be reached by consuming e from c n ) and
this concludes the proof for the part that concerns c n .
When we consider the other channels (c 1 to c n 1 ) the proof of Lemma A.1 shows that,
i all are encodings of numbers.
Furthermore, they satisfy
| {z }
times
(1)e and w j
2:
as we prove by induction on j. The base case, (W 0 ) is a consequence of the assumption (14).
Then one shows that (W j ) entails (V j+1 ) using Prop. 3.1. Finally, one proves that
using
One concludes the proof of (H n ) by observing that m  k and (Wm ) entail the right hand
side of (H n ) because of the monotonicity and expansion properties of A n stated in (5).

Appendix

Proof of Prop. 3.3
For the \)" direction, we proceed as with the proof of Prop. 3.2, and start with a result
mimicking Lemma A.1:
Lemma B.1 If a run hs 0
is such that every w i
contains one b and one e, then every w i encodes a number.
Proof. Omitted.
We now prove
by induction over n. The base is easy to see. For n > 2, we consider a run
isolate the congurations where it visits
writing it under the form
We start with the contents of c n : the w i
n have the form eb1 k i and, resp., eb1 k 0
. The
transition from q 0
n to s 0
one 1 to c n , so that, for
l  a n we deduce l  a n .
When we consider the contents of the other channels, the w j
's and v j
's encode numbers for
Using (H 0
shows, by induction on i, that w j
so that a
writing
so that, by monotonicity of A n 1 ,
| {z }
l times
(because nally leaving q 0
consumes d1e from c n 1
entail that A n (a n )  m, completing the proof.



--R

Symbolic veri

Reasoning about probabilistic lossy channel systems.

Undecidable veri
Verifying programs with unreliable channels.
Decidability of simulation and bisimulation between lossy channel systems and
An improved search strategy for lossy channel systems.
Finite state description of communication protocols.


Reset nets between decidability and undecidability.

Decidability of the termination problem for completely speci
Well structured transition systems everywhere!
The equality problem for vector addition systems is undecidable.
Ordering by divisibility in abstract algebras.

Undecidable problems in unreliable computations.
The complexity of the
Bisimulation and other undecidable equivalences for lossy channel systems.
--TR
Unreliable channels are easier to verify than perfect channels
Undecidable verification problems for programs with unreliable channels
The Complexity of the Finite Containment Problem for Petri Nets
On Communicating Finite-State Machines
Algorithmic analysis of programs with well quasi-ordered domains
Nonprimitive recursive complexity and undecidability for Petri net equivalence
Well-structured transition systems everywhere!
Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems
An Improved Search Strategy for Lossy Channel Systems
Boundedness of Reset P/T Nets
Reset Nets Between Decidability and Undecidability
Undecidable Problems in Unreliable Computations
Symbolic Verification of Lossy Channel Systems
Reasoning about Probabilistic Lossy Channel Systems
Decidability of Simulation and Bisimulation between Lossy Channel Systems and Finite State Systems (Extended Abstract)
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

--CTR
Giorgio Delzanno, Constraint-based automatic verification of abstract models of multithreaded programs, Theory and Practice of Logic Programming, v.7 n.1-2, p.67-91, January 2007
Alexander Rabinovich, Quantitative analysis of probabilistic lossy channel systems, Information and Computation, v.204 n.5, p.713-740, May 2006
P. A. Abdulla , N. Bertrand , A. Rabinovich , Ph. Schnoebelen, Verification of probabilistic systems with faulty communication, Information and Computation, v.202 n.2, p.141-165, 1 November, 2005
Blaise Genest , Dietrich Kuske , Anca Muscholl, A Kleene theorem and model checking algorithms for existentially bounded communicating automata, Information and Computation, v.204 n.6, p.920-956, June 2006
Roberto M. Amadio , Charles Meyssonnier, On decidability of the control reachability problem in the asynchronous -calculus, Nordic Journal of Computing, v.9 n.2, p.70-101, Summer 2002
Grard Cc , Alain Finkel, Verification of programs with half-duplex communication, Information and Computation, v.202 n.2, p.166-190, 1 November, 2005
Antonn Kuera , Philippe Schnoebelen, A general approach to comparing infinite-state systems with their finite-state specifications, Theoretical Computer Science, v.358 n.2, p.315-333, 7 August 2006
Antonn Kuera , Petr Janar, Equivalence-checking on infinite-state systems: Techniques and results, Theory and Practice of Logic Programming, v.6 n.3, p.227-264, May 2006
verification of infinite-state systems;communication protocols;program correctness;formal methods