4th Asian Computing Science Conference, ASIAN ’98 Proceedings: Jieh Hsiang and Atsushi Ohori (eds.) Springer Lecture Notes in Computer Science 1538 (1998), 282–299.

Towards a characterisation of finite-state message-passing systems

Madhavan Mukund^{1}^{⋆}, K Narayan Kumar^{1}^{⋆⋆}, Jaikumar Radhakrishnan^{2}, and Milind Sohoni^{3}

1 SPIC Mathematical Institute, 92 G.N. Chetty Road, Madras 600 017, India.

             E-mail: {madhavan,kumar}@smi.ernet.in

2 Computer Science Group, Tata Institute of Fundamental Research, Homi Bhabha

Road, Bombay 400 005, India. E-mail: jaikumar@tcs.tifr.res.in 3 Department of Computer Science and Engineering, Indian Institute of Technology,

Bombay 400 076, India. E-mail: sohoni@cse.iitb.ernet.in

Abstract. We investigate an automata-theoretic model of distributed systems which communicate via message-passing. Each node in the system is a finite-state device. Channels are assumed to be reliable but may deliver messages out of order. Hence, each channel is modelled as a set of counters, one for each type of message. These counters may not be tested for zero. Though each node in the network is finite-state, the overall system is potentially infinite-state because the counters are unbounded. We work in an interleaved setting where the interactions of the system with the environment are described as sequences. The behaviour of a system is described in terms of the language which it accepts—that is, the set of valid interactions with the environment that are permitted by the system. Our aim is to characterise the class of message-passing systems whose behaviour is finite-state. Our main result is that the language accepted by a message-passing system is regular if and only if both the language and its complement are accepted by message-passing systems. We also exhibit an alternative characterisation of regular message-passing languages in terms of deterministic automata.

1 Introduction

Today, distributed systems which use asynchronous communication are ubiquitous— the Internet is a prime example. However, there has been very little work on studying the finite-state behaviour of such systems. In particular, this area lacks a satisfactory automata-theoretic framework. In contrast, automata theory for systems with synchronous communication is well developed via Zielonka’s

⋆ Partly supported by IFCPAR Project 1502-1. ⋆⋆ Currently on leave at Department of Computer Science, State University of New

York at Stony Brook, NY 11794-4400, USA. E-mail: kumar@cs.sunysb.edu.

asynchronous automata [Z87] and the connections to Mazurkiewicz trace theory [M78].

In [MNRS98], we introduce networks of message-passing automata as a model for distributed systems which communicate via message-passing. Each node in the network is a finite-state process. The number of different types of messages used by the system is assumed to be finite. This is not unreasonable if we distinguish “control” messages from “data” messages.

In our model, channels may reorder or delay messages, though messages are never lost. Since messages may be reordered, the state of each channel can be represented by a finite set of counters which record the number of messages of each type that have been sent along the channel but are as yet undelivered. The nodes cannot test if a counter’s value is zero—this restriction captures the intuition that it is not practical for a node to decide that another process has not sent a message, since messages may be delayed arbitrarily.

Though each node in the network is finite-state, the overall system is potentially infinite-state since counter values are unbounded. Our goal is to characterise when such a network is “effectively finite-state”. This is important because finite-state networks are amenable to verification using automated tools [H91].

To make precise the notion of a network being “effectively finite-state”, we use formal language theory. The behaviour of the network is described in terms of its interaction with the environment. This can be represented as a formal language over a finite alphabet of possible interactions. Our goal then is to characterise when the language accepted by a network is regular.

In [MNRS98], we assume that each node interacts independently with its environment. Thus, the behaviour of the overall network is described as a language consisting of tuples of strings. The main result is that the language accepted by a robust message-passing network, whose behaviour is insensitive to message delays and differences in speed between nodes, can be “represented” by a sequential regular language.

Here, we adopt an interleaved approach and record the interactions of a network with its environment from the point of view of a sequential observer. In this framework, it is sufficient to concentrate on the global states of the system and regard the entire network as a single automaton equipped with a set of counters. Our main result is that a language L accepted by a messagepassing automaton is regular if and only if the complement of L is also accepted by a message-passing automaton. This is more general than requiring that L be robust in the sense of [MNRS98]—see Section 5.1. We also demonstrate an alternative characterisation in terms of deterministic message-passing automata. Along the way, we establish a variety of results about message-passing automata, including pumping lemmas which are useful for showing when languages are not recognisable by these automata.

The paper is organised as follows. In the next section we define messagepassing automata and establish some basic results about them. In Section 3 we prove a Contraction Lemma which leads to the decidability of the emptiness problem and the fact that the languages accepted by message-passing automata are not closed under complementation. Section 4 describes a family of pumping lemmas which are exploited in Section 5 to prove our main results concerning the regularity of languages accepted by message-passing automata. In the final section, we discuss in detail the connection between our results and those in Petri net theory and point out directions for future work. We have had to omit many proofs in this extended abstract. Full proofs and related results can be found in [MNRS97,MNRS98].

2 Message-Passing Automata

Natural numbers and tuples As usual, ℕ denotes the set {0, 1, 2, …} of natural numbers. For i, j ∈ ℕ, [i..j] denotes the set {i, i+1, …, j}, where [i..j] = ∅ if i > j. We compare k-tuples of natural numbers component-wise. Let \overline{m} = ⟨m_{1}, m_{2}, …, m_{k}⟩ and \overline{n} = ⟨n_{1}, n_{2}, …, n_{k}⟩. Then \overline{m} ≤ \overline{n} iff m_{i} ≤ n_{i} for each i ∈ [1..k].

Message-passing automata A message-passing automaton A is a tuple (Q, Σ, Γ, T, q_{in}, F), where:

– Q is a finite set of states, with initial state q_{in} and accepting states F ⊆ Q.

– Σ is a finite input alphabet.

– Γ is a finite set of counters. We use C, C′, … to denote counters. With each counter C, we associate two symbols, C^{+} and C^{−}. We write Γ^{±} to denote the set {C^{+}|C ∈ Γ } ∪ {C^{−}|C ∈ Γ }.

– T ⊆ Q × (Σ ∪ Γ^{±}) × Q is the transition relation.

Configurations A configuration of A is a pair (q, f) where q ∈ Q and f : Γ → ℕ is a function which records the values stored in the counters. If the counters are C_{1}, C_{2}, …, C_{k} then we represent f by an element ⟨f(C_{1}), f(C_{2}), …, f(C_{k})⟩ of ℕ^{k}. By abuse of notation, the k-tuple ⟨0, 0, …, 0⟩ is uniformly denoted \overline{0}, for all values of k.

We use χ to denote configurations. If χ = (q, f), Q(χ) denotes q and F (χ) denotes f. Further, for each counter C, C(χ) denotes the value f(C).

Moves Each move of a message-passing automaton consists of either reading a letter from its input or manipulating a counter. Reading from the input represents interaction with the environment. Incrementing and decrementing counters correspond to sending and reading messages, respectively.

Formally, a message-passing automaton moves from configuration χ to configuration χ′ on d ∈ Σ ∪ Γ^{±} if (Q(χ), d, Q(χ′)) ∈ T and one of the following holds:

– d ∈ Σ and F (χ) = F (χ′).

– d = C^{+}, C(χ′) = C(χ) + 1 and C′(χ) = C′(χ′) for every C′ ≠ C.

– d = C^{−}, C(χ′) = C(χ) − 1 ≥ 0 and C′(χ) = C′(χ′) for every C′ ≠ C.

Such a move is denoted χ ⟶^{(q,d,q′)} χ′—that is, transitions are labelled by elements of T. Given a sequence of transitions t_{1}t_{2} … t_{n} = (q_{1}, d_{1}, q_{2})(q_{2}, d_{2}, q_{3}) … (q_{n}, d_{n}, q_{n+1}), the corresponding sequence d_{1}d_{2} … d_{n} over Σ ∪ Γ^{±} is denoted α(t_{1}t_{2} … t_{n}).

Computations, runs and languages A computation of A is a sequence χ_{0} ⟶^{t_{1}} χ_{1} ⟶^{t_{2}} … ⟶^{t_{n}} χ_{n}. We also write χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} to indicate that there is a computation labelled t_{1}t_{2} … t_{n} from χ_{0} to χ_{n}. Notice that χ_{0} and t_{1}t_{2} … t_{n} uniquely determine all the intermediate configurations χ_{1}, χ_{2}, …, χ_{n}. If the transition sequence is not relevant, we just write χ_{0} ⟹ χ_{n}. As usual, χ ⟹^{t_{1}t_{2}...t_{n}} denotes that there exists χ′ such that χ ⟹^{t_{1}t_{2}...t_{n}} χ′ and χ ⟹ denotes that there exists χ′ such that χ ⟹ χ′.

For K ∈ ℕ, a K-run of A is a computation χ_{0} ⟹ χ_{n} where C(χ_{0}) ≤ K for each C ∈ Γ.

If δ is a string over Σ ∪ Γ^{±}, δ ↾_{Σ} denotes the subsequence of letters from Σ in δ. Let w = a_{1}a_{2} … a_{k} be a string over Σ. A run of A over w is a 0-run χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} where Q(χ_{0}) = q_{in} and α(t_{1}t_{2} … t_{n})↾_{Σ} = w. The run is said to be accepting if Q(χ_{n}) ∈ F. The string w is accepted by A if A has an accepting run over w. The language accepted by A, denoted L(A), is the set of all strings over Σ accepted by A.

A language over Σ is said to be message-passing recognisable if there is a message-passing automaton with input alphabet Σ that accepts this language.

Example 2.1. Let L_{ge} ⊆ {a, b}^{∗} be given by {a^{m}b^{n} | m ≥ n}. This language is message-passing recognisable. Here is an automaton for L_{ge}. The initial state is indicated by ⇓ and the final states have an extra circle around them.

a C^{+}  b  C^{−} b ⇓

The following result is basic to analysing the behaviour of message-passing automata. It follows from the fact that any infinite sequence of N-tuples of natural numbers contains an infinite increasing subsequence. We omit the proof.

Lemma 2.2. Let X be a set with M elements and ⟨x_{1}, f_{1}⟩, ⟨x_{2}, f_{2}⟩, …, ⟨x_{m}, f_{m}⟩ be a sequence over X × ℕ^{N} such that each coordinate of f_{1} is bounded by K and for i ∈ [1..m−1], f_{i} and f_{i+1} differ on at most one coordinate and this difference is at most 1. There is a constant ℓ which depends only on M, N and K such that if m ≥ ℓ, then there exist i, j ∈ [1..m] with i < j, x_{i} = x_{j} and f_{i} ≤ f_{j}.

Weak pumping constant We call the bound ℓ for M, N and K from the preceding lemma the weak pumping constant for (M, N, K), denoted π_{M,N,K}.

It is easy to see that if ⟨M′, N′, K⟩ ≤ ⟨M, N, K⟩, then π_{M′,N′,K′} ≤ π_{M,N,K}.

3 A Contraction Lemma

Lemma 3.1 (Contraction). For every message-passing automaton A, there is a constant k such that if χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} is a computation of A, with m > k, then

there exist i and j, m−k ≤ i < j ≤ m, such that χ′_{0} ⟹^{t_{1}...t_{i}t_{j+1}...t_{m}} χ′_{m−(j−i)} is also

a computation of A, with with χ′_{ℓ} = χ_{ℓ} for ℓ ∈ [0..i] and Q(χ_{ℓ}) = Q(χ′_{ℓ−(j−i)}) for all ℓ ∈ [j..m].

Proof Sketch. Let A have M states and N counters. We show that k can be chosen to be π_{M,N,0}. Let χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be a computation of A, with m > π_{M,N,0}. We define a sequence f_{m}, f_{m−1}, …, f_{0} of functions from Γ to ℕ as follows:

f_{m}(C) = 0, for all C ∈ Γ
For i ∈ [0..m−1], f_{i}(C) = \{ \begin{matrix}f_{i+1}(C) & if α(t_{i+1}) ∉ \{C^{+}, C^{−}\} \\ f_{i+1}(C)+1 & if α(t_{i+1}) = C^{−} \\ max(0, f_{i+1}(C)−1) & if α(t_{i+1}) = C^{+} \end{matrix}

We claim, without proof, that for each i, the function f_{i} represents the minimum counter values required to execute the transition sequence t_{i+1}t_{i+2} … t_{m}.

Claim: ∀i ∈ [1..m], (Q(χ_{i}), f) ⟹^{t_{i+1}t_{i+2}...t_{m}} iff f ≥ f_{i}.

Corollary to Claim: For each counter C and for each position i ∈ [1..m], C(χ_{i}) ≥ f_{i}(C).

Consider the sequence of N-tuples f_{m}, f_{m−1}, … f_{0}. Since its length exceeds π_{M,N,0}, by Lemma 2.2 there exist positions i and j, m ≥ j > i ≥ m−π_{M,N,0} such that f_{j} ≤ f_{i} and Q(χ_{j}) = Q(χ_{i}). By the Corollary to Claim, for each counter C,

C(χ_{i}) ≥ f_{i}(C) ≥ f_{j}(C). Thus, χ_{i} ⟹^{t_{j+1}t_{j+2}...t_{m}} whereby χ_{0} ⟹^{t_{1}t_{2}...t_{i}} χ_{i} ⟹^{t_{j+1}t_{j+2}...t_{m}}

χ′_{m−(j−i)} is a valid computation of A for some configuration χ′_{m−(j−i)}. Since

Q(χ_{j}) = Q(χ_{i}) and the computations χ_{j} ⟹^{t_{j+1}t_{j+2}...t_{m}} χ_{m} and χ_{i} ⟹^{t_{j+1}t_{j+2}...t_{m}}

χ′_{m−(j−i)} are labelled by the same sequence of transitions, it follows that Q(χ_{ℓ}) = Q(χ′_{ℓ−(j−i)}) for each ℓ ∈ [j..m], as required. □

Corollary 3.2. A message-passing automaton A with M states and N counters has an accepting computation iff it has an accepting computation whose length is bounded by π_{M,N,0}.

It is possible to provide an explicit upper bound for π_{M,N,K} for all values of M, N, and K. This fact, coupled with the preceding observation, yields the following result (which can also be derived from the decidability of the reachability problem for Petri nets).

Corollary 3.3. The emptiness problem for message-passing automata is decidable.

Corollary 3.4. Message-passing recognisable languages are not closed under complementation.

Proof Sketch. We saw earlier that L_{ge} = {a^{m}b^{n} | m ≥ n} is message-passing recognisable. We show that the language L_{lt} = {a^{m}b^{n} | m < n} is not messagepassing recognisable. Suppose that L_{lt} is accepted by an automaton A_{lt} with M states and N counters. Consider the string w = a^{J}b^{J+1} where J = π_{M,N,0} and let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} be an accepting run of A_{lt} on w. By applying the Contraction Lemma (repeatedly, if necessary) to ρ, we can obtain an accepting run ρ′ of A_{lt} over a word of the form a^{J}b^{K}, where K ≤ J, thus contradicting the assumption that L(A_{lt}) = L_{lt}. □

4 A Collection of Pumping Lemmas

Our main result is based on a series of pumping lemmas, which we present in this section. For reasons of space, we do not provide any proofs. More details may be found in [MNRS97,MNRS98].

Change vectors For a string w and a symbol x, let #_{x}(w) denote the number of times x occurs in w. Let v be a sequence of transitions. Recall that α(v) denotes the corresponding sequence of letters. For each counter C, define Δ_{C}(v) to be #_{C^{+}}(α(v)) − #_{C^{−}}(α(v)). The change vector associated with v, denoted Δv, is given by ⟨Δ_{C}(v)⟩_{C∈Γ}.

Proposition 4.1. Let A = (Q, Σ, Γ, T, q_{in}, F) be a message-passing automaton.

(i) For any computation χ ⟹^{v} χ′ of A and any counter C ∈ Γ, |Δ_{C}(v)| ≤ |v|.

(ii) For any configuration χ and sequence of transitions v, χ ⟹^{v} iff for each prefix u of v and each counter C ∈ Γ, C(χ) + Δ_{C}(u) ≥ 0.

(iii) Let χ ⟹^{u} χ′ ⟹^{v} with Q(χ) = Q(χ′) and n ∈ ℕ such that, for every counter

C ∈ Γ, either Δ_{C}(u) ≥ 0 or C(χ) ≥ n|u| + |v|. Then, χ ⟹^{u^{n}v}.

Proof.

(i) This follows from the fact that each move can change a counter value by at most 1.

(ii) This follows immediately from the definition of a computation.

(iii) The proof is by induction on n.

Basis: For n = 0, there is nothing to prove.

Induction step: Let n > 0 and assume the result holds for n−1. We will show

that χ ⟹^{u} χ′ ⟹^{u^{n−1}v}.

From the assumption, we know that χ ⟹^{u} χ′. To show that χ′ ⟹^{u^{n−1}v}, we examine the value of each counter C at χ′. If Δ_{C}(u) < 0, then C(χ) ≥ n|u| + v. Since C(χ′) = C(χ′) + Δ_{C}(u) and |Δ_{C}(u)| ≤ |u|, it follows that C(χ′) ≥ (n−1)|u| + v. From the induction hypothesis, we can then conclude

that χ′ ⟹^{u^{n−1}v}.

□

Pumpable decomposition Let A be a message-passing automaton with N counters and let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be a computation of A. A decomposition

χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⟹^{u_{3}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m} of ρ is said

to be pumpable if it satisfies the following conditions:

(i) n ≤ N. (ii) For each k ∈ [1..n], Q(χ_{i_{k}}) = Q(χ_{j_{k}}). (iii) For each v_{k}, k ∈ [1..n], Δv_{k} is non-zero and has at least one positive entry. (iv) Let C be a counter and k ∈ [1..n] such that Δ_{C}(v_{k}) is negative. Then, there

exists ℓ < k such that Δ_{C}(v_{ℓ}) is positive.

We refer to v_{1}, v_{2}, …, v_{n} as the pumpable blocks of the decomposition. We say that a counter C is pumpable if Δ_{C}(v_{i}) > 0 for some pumpable block v_{i}. The following lemma shows that all the pumpable counters of a pumpable decomposition are simultaneously unbounded. We omit the proof. (This is similar to a well-known result of Karp and Miller in the theory of vector addition systems [KM69].)

Lemma 4.2 (Counter Pumping). Let A be a message-passing automaton and ρ a K-run of A, K ∈ ℕ, with a pumpable decomposition of the form χ_{0} ⟹^{u_{1}}

χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m}. Then, for any

I, J ∈ ℕ, with I ≥ 1, there exist ℓ_{1}, ℓ_{2}, …, ℓ_{n} ∈ ℕ and a K-run ρ′ of A of the

form χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} χ′_{i′_{2}} ⟹^{v_{2}^{ℓ_{2}}} χ′_{j′_{2}} ⋯ ⟹^{u_{n}} χ′_{i′_{n}} ⟹^{v_{n}^{ℓn}} χ′_{j′_{n}} ⟹^{u_{n+1}} χ′_{p} such that

ρ′ satisfies the following properties:

(i) χ_{0} = χ′_{0}. (ii) Q(χ′_{p}) = Q(χ_{m}). (iii) For i ∈ [1..n], ℓ_{i} ≥ I. (iv) For every counter C, C(χ′_{p}) ≥ C(χ_{m}).

(v) Let Γ_{pump} be the set of pumpable counters in the pumpable decomposition of ρ. For each counter C ∈ Γ_{pump}, C(χ′_{p}) ≥ J.

Proof. The proof is by induction on n, the number of pumpable blocks in the decomposition.

Basis: If n = 0, there is nothing to prove.

Induction step: Let n > 0 and assume the lemma holds for all decompositions with n−1 pumpable blocks. For each counter C, let J_{C} = max(J, C(χ_{m})).

By the induction hypothesis, for all I′, J′ ∈ ℕ, I′ ≥ 1, we can transform the

prefix σ : χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} ⋯ ⟹^{v_{n−1}} χ_{j_{n−1}} ⟹^{u_{n}} χ_{i_{n}} of ρ into a K-run

σ′ : χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} ⋯ ⟹^{v_{n−1}^{ℓ_{n−1}}} χ′_{j′_{n−1}} ⟹^{u_{n}} χ′_{i′_{n}} satisfying the conditions of

the lemma. We shall choose I′ and J′ so that the transition sequence v_{n}^{ℓ_{n}}u_{n+1} can be appended to σ′ to yield the run claimed by the lemma.

To fix values for I′ and J′, we first estimate the value of ℓ_{n}, the number of times we need to pump v_{n} to satisfy all the conditions of the lemma. Let Γ_{pos}^{n} = {C | Δ_{C}(v_{n}) > 0}. It is sufficient if the number ℓ_{n} is large enough for each counter C ∈ Γ_{pos}^{n} to exceed J_{C} at the end of the new computation. For a counter C ∈ Γ_{pos}^{n} to be above J_{C} at the end of the computation, it is sufficient for C to have the value J_{C} + |u_{n+1}| after v_{n}^{ℓ_{n}}. By the induction hypothesis, the value of C before v_{n}^{ℓ_{n}} is at least C(χ_{i_{n}}). Hence, it would take ⌈\frac{J_{C}+|u_{n+1}|−C(χ_{in})}{Δ_{C}(v_{n})}⌉ iterations of v_{n} for C to reach the required value after v_{n}^{ℓ_{n}}. On the other hand, we should also ensure that ℓ_{n} ≥ I. Thus, it is safe to set ℓ_{n} to be the maximum of I and max_{C∈Γ_{pos}^{n}}⌈\frac{J_{C}+|u_{n+1}|−C(χ_{in})}{Δ_{C}(v_{n})}⌉.

We set I′ = I and estimate a value for J′ such that χ′_{i′_{n}} ⟹^{v_{n}^{ℓn} u_{n+1}} χ′_{p} with each counter C ∈ (Γ \ Γ_{pos}^{n}) achieving a value of at least C(χ_{m}) at χ′_{p} and each counter C ∈ (Γ_{pos} \ Γ_{pos}^{n}) achieving a value of at least J_{C} at χ′_{p}.

By the induction hypothesis, Q(χ′_{i′_{n}}) = Q(χ_{i_{n}}) and F (χ′_{i′_{n}}) ≥ F (χ_{i_{n}}). Since

χ_{i_{n}} ⟹^{v_{n}u_{n+1}}, it follows that χ′_{i′_{n}} ⟹^{v_{n}u_{n+1}}. By Proposition 4.1 (iii), to ensure that

χ′_{i′_{n}} ⟹^{v_{n}^{ℓn} u_{n+1}} χ′_{p}, it is sufficient to raise each counter C with Δ_{C}(v_{n}) < 0 to a value of at least ℓ_{n}|v_{n}| + |u_{n+1}| at χ′_{i′_{n}}. If Δ_{C}(v_{n}) < 0 then, by the definition of pumpable decompositions, Δ_{C}(v_{i}) > 0 for some i ∈ [1..n−1], so C gets pumped above J′ in σ′.

Any counter C such that Δ_{C}(v_{n}) ≥ 0 will surely exceed C(χ_{m}) at χ′_{p}. On the other hand, a counter C such that Δ_{C}(v_{n}) < 0 can decrease by at most ℓ_{n}|v_{n}| + |u_{n+1}| after χ′_{i′_{n}}.

Putting these two facts together, it suffices to set J′ to ℓ_{n}|v_{n}| + |u_{n+1}| + max_{{C|Δ_{C}(v_{n})<0}}J_{C}.

Let ρ′ : χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} ⋯ ⟹^{u_{n}} χ′_{i′_{n}} ⟹^{v_{n}^{ℓn}} χ′_{j′_{n}} ⟹^{u_{n+1}} χ′_{p}. By the

induction hypothesis, we know that χ′_{0} = χ_{0} and for i ∈ [1..n−1], ℓ_{i} ≥ I. By construction, ℓ_{n} ≥ I as well. We have also ensured that for every counter C, C(χ′_{p}) ≥ C(χ_{m}) and for every counter C ∈ Γ_{pos}, C(χ′_{p}) ≥ J. The fact that Q(χ′_{p}) = Q(χ_{m}) follows from the fact that each v_{n} loop brings the automaton back to Q(χ′_{i′_{n}}) = Q(χ_{i_{n}}), and the fact that both ρ and ρ′ go through the same sequence of transitions u_{n+1} at the end of the computation. □

Having shown that all pumpable counters of a pumpable decomposition can be simultaneously raised to arbitrarily high values, we describe a sufficient condition for a K-run to admit a non-trivial pumpable decomposition.

Strong pumping constant For each M, N, K ∈ ℕ, we define the strong pumping constant Π_{M,N,K} by induction on N as follows (recall that π_{M,N,K} denotes the weak pumping constant for (M, N, K)):

\begin{aligned}∀M, K ∈ ℕ. & Π_{M,0,K} & = & 1 \\ ∀M, N, K ∈ ℕ. & Π_{M,N+1,K} & = & Π_{M,N,π_{M,N+1,K}+K} + π_{M,N+1,K} + K \end{aligned}

Lemma 4.3 (Decomposition). Let A be a message-passing automaton with M states and N counters and let K ∈ ℕ. Let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be any Krun of A. Then, there is a pumpable decomposition χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}}

χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m} of ρ such that for every counter C,

if C(χ_{j}) > Π_{M,N,K} for some j ∈ [0..m], then there exists k ∈ [1..n], such that Δ_{C}(v_{k}) is positive.

To prove this lemma, we need the following result.

Proposition 4.4. Let A be a message-passing automaton with M states and N counters and let ρ : χ_{0} ⟹ χ_{n} be a K-run of A in which some counter value exceeds π_{M,N,K} + K. Then, there is a prefix σ : χ_{0} ⟹ χ_{s} of ρ such that:

– For each m ∈ [0..s] and every counter C, C(χ_{m}) < π_{M,N,K} + K.

– There exists r ∈ [0..s−1], such that σ : χ_{0} ⟹ χ_{r} ⟹ χ_{s}, Q(χ_{r}) = Q(χ_{s}) and F (χ_{r}) < F (χ_{s}).

Proof. Suppose that the lemma does not hold. Let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} be a computation of minimum length which fails to satisfy the lemma. Since the initial counter values in ρ are bounded by K and some counter value exceeds π_{M,N,K} + K in ρ, it must be the case that the length of ρ is at least π_{M,N,K}.

By the definition of π_{M,N,K}, there exist i and j, i < j ≤ π_{M,N,K} such that Q(χ_{i}) = Q(χ_{j}) and F (χ_{i}) ≤ F (χ_{j}). Since ρ is a K-run and j ≤ π_{M,N,K}, all counter values at the configurations χ_{0}, χ_{1}, …, χ_{j} must be bounded by π_{M,N,K} + K. If F (χ_{i}) < F (χ_{j}), ρ would satisfy the lemma with r = i and s = j, so it must be the case F (χ_{i}) = F (χ_{j}).

Since χ_{i} = χ_{j}, we can construct a shorter computation ρ′ = χ_{0} ⟹^{t_{1}t_{2}...t_{i}}

χ_{i} ⟶^{t_{j+1}} χ_{j+1} ⟶^{t_{j+2}} ⋯ ⟶^{t_{n}} χ_{n}. It is easy to see that the same counter whose value exceeded π_{M,N,K} + K in ρ must also exceed π_{M,N,K} + K in ρ′—the only configurations visited by ρ which are not visited by ρ′ are those in the interval χ_{i+1}, χ_{i+2}, … χ_{j}. However, we have already seen that all counter values in χ_{0}, χ_{1}, …, χ_{j} are bounded by π_{M,N,K} + K.

It is clear that if ρ′ satisfies the lemma, then so does ρ. On the other hand, if ρ′ does not satisfy the lemma, then ρ is not a minimum length counterexample to the lemma. In either case we obtain a contradiction. □

We now return to the proof of the Decomposition Lemma.

Proof. (of Lemma 4.3) The proof is by induction on N, the number of counters.

Basis: If N = 0, set n = 0 and u_{1} = ρ.

Induction step: Let Γ_{gt} denote the set of counters whose values exceed Π_{M,N,K} in the K-run ρ.

If Γ_{gt} = ∅, we set n = 0 and u_{1} = ρ.

Otherwise, by Proposition 4.4, we can find positions r and s in ρ such that χ_{0} ⟹^{u′} χ_{r} ⟹^{v′} χ_{s} ⟹ χ_{m}, with Q(χ_{r}) = Q(χ_{s}), F (χ_{r}) < F (χ_{s}) and all counter values at χ_{0}, χ_{1}, …, χ_{s} bounded by π_{M,N,K} + K.

Let Σ be the input alphabet of A and Γ its set of counters. Fix a counter C′ in which increases strictly between χ_{r} and χ_{s}—that is, C′(χ_{s}) > C′(χ_{r}). By our choice of χ_{r} and χ_{s}, such a counter must exist. Construct an automaton A′ with input alphabet Σ ∪ {C^{′+}, C^{′−}} and counters Γ \ {C′}. The states and transitions of A′ are the same as those of A. In other words, A′ behaves like A except that it treats moves involving the counter C′ as input letters.

Consider the computation χ_{s} ⟹^{t_{s+1}t_{s+2}...t_{m}} χ_{m} of A. It is easy to see that there is a corresponding computation ρ′ : χ′_{s} ⟹^{t_{s+1}t_{s+2}...t_{m}} χ′_{m} of A′ such that for each k ∈ [s..m], Q(χ_{k}) = Q(χ′_{k}) and for each counter C ≠ C′, C(χ_{k}) = C(χ′_{k}).

From Proposition 4.4, we know that ρ′ is in fact a (π_{M,N,K}+K)-run of A′. Further, for every counter C in Γ_{gt} \ {C′}, there exists a j ∈ [s..m], such that C(χ′_{j}) = C(χ_{j}) > Π_{M,N,K} > Π_{M,N−1,π_{M,N,K}+K}. (In the K-run ρ, no counter could have exceeded Π_{M,N,K} before χ_{s} because Proposition 4.4 guarantees that all counter values at χ_{0}, χ_{1}, …, χ_{s} are bounded by π_{M,N,K}+K.) By the induction hypothesis, we can find a pumpable decompostion

χ′_{s} ⟹^{u′_{1}} χ′_{i′_{1}} ⟹^{v′_{1}} χ′_{j′_{1}} ⟹^{u′_{2}} χ′_{i′_{2}} ⟹^{v′_{2}} χ′_{j′_{2}} ⟹^{u′_{3}} ⋯ ⟹^{u′_{p}} χ′_{i′_{p}} ⟹^{v′_{p}} χ′_{j′_{p}} ⟹^{u′_{p+1}} χ_{m}

of ρ′ such that if C is a counter with C(χ′_{j}) > Π_{M,N−1,π_{M,N,K}+K} for some j ∈ [s..m], then there exists k ∈ [1..p] such that Δ_{C}(v′_{k}) is positive.

Consider the corresponding computation

χ_{s} ⟹^{u′_{1}} χ_{i′_{1}} ⟹^{v′_{1}} χ_{j′_{1}} ⟹^{u′_{2}} χ_{i′_{2}} ⟹^{v′_{2}} χ_{j′_{2}} ⋯ ⟹^{u′_{p}} χ_{i′_{p}} ⟹^{v′_{p}} χ_{j′_{p}} ⟹^{u′_{p+1}} χ_{m}

of A. In this computation, for each k ∈ [1..p], Q(χ_{i′_{k}}) = Q(χ′_{i′_{k}}) = Q(χ′_{j′_{k}}) = Q(χ_{j′_{k}}). Further, for each C ∈ Γ_{gt} \{C′}, C(χ_{i′_{k}}) = C(χ′_{i′_{k}}) and C(χ_{j′_{k}}) = C(χ′_{j′_{k}}).

We prefix the computation χ_{s} ⟹^{u′_{1}v′_{1}...u′_{p+1}} χ_{m} with the K-run χ_{0} ⟹^{u′} χ_{r} ⟹^{v′} χ_{s} which we used to identify χ_{s} and χ_{r}. We then assert that the composite K-run

χ_{0} ⟹^{u′} χ_{r} ⟹^{v′} χ_{s} ⟹^{u′_{1}} χ_{i′′_{1}} ⟹^{v′_{1}} χ_{j′′_{1}} ⟹^{u′_{2}} χ_{i′′_{2}} ⟹^{v′_{2}} χ_{j′′_{2}} ⋯ ⟹^{u′_{p}} χ_{i′′_{p}} ⟹^{v′_{p}} χ_{j′′_{p}} ⟹^{u′_{p+1}} χ_{m}.

provides the decomposition

χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m}

of ρ claimed in the statement of the lemma. In other words, u_{1} = u′, v_{1} = v′, χ_{i_{1}} = χ_{r} and χ_{j_{1}} = χ_{s}, while for k ∈ [2..n], u_{k} = u′_{k−1}, v_{k} = v′_{k−1}, χ_{i_{k}} = χ_{i′_{k−1}} and χ_{j_{k}} = χ_{j′_{k−1}}.

Let us verify that this decomposition satisfies all the conditions required by the lemma.

First we verify that this decomposition is pumpable.

– Since p ≤ N−1, it is clear than n = p+1 ≤ N.

– By construction Q(χ_{i_{1}}) = Q(χ_{r}) = Q(χ_{s}) = Q(χ_{j_{1}}). For k ∈ [2..n], Q(χ_{i_{k}}) = Q(χ_{i′_{k−1}}) = Q(χ_{j′_{k−1}}) = Q(χ_{j_{k}}).

– We know that Δv_{1} = Δv′ is non-zero and strictly positive by the choice of v′. For k ∈ [2..n], we know that Δ_{C}(v_{k}) = Δ_{C}(v′_{k−1}) for C ≠ C′. Since we have already established that Δv′_{k−1} is non-zero and has at least one positive entry for k ∈ [2..n], it follows that the corresponding change vectors Δv_{k} are also non-zero and have at least one positive entry.

– Let C be a counter and k ∈ [1..n] such that Δ_{C}(v_{k}) is negative. Since Δv_{1} = Δv′ is positive by the choice of v, it must be that k ∈ [2..n]. If C ≠ C′, then Δ_{C}(v′_{k−1}) = Δ_{C}(v_{k}) is negative. In this case, we already know that there exists ℓ ∈ [2..k−1], such that Δ_{C}(v′_{ℓ−1}) = Δ_{C}(v_{ℓ}) is positive. On the other hand, if C = C′, it could be that Δ_{C′}(v′_{z}) is negative for all z ∈ [1..p], since C′ is treated as an input letter rather than as a counter in the automaton A′. However, we know that Δ_{C′}(v_{1}) = Δ_{C′}(v′) is positive by the choice of v′ and C′, so C′ also satisfies the condition of the lemma.

Finally, let C be a counter such that C(χ_{j}) > Π_{M,N,K} for some j ∈ [1..m]. If C ≠ C′, then C(χ_{j}) > Π_{M,N−1,π_{M,N,K}+K} for some j ∈ [s..m], so we already know that Δ_{C}(v′_{k−1}) = Δ_{C}(v_{k}) is positive for some k ∈ [2..n]. On the other hand, if C = C′, we know that Δ_{C}(v_{1}) = Δ_{C}(v′) is positive by the choice of v′ and C′.

□

The Counter Pumping Lemma allows us to pump blocks of transitions in a computation. However, it is possible for a pumpable block to consist solely of invisible transitions which increment and decrement counters. Using the Decomposition Lemma, we can prove a more traditional kind of pumping lemma, stated in terms of input strings. We omit the proof.

Lemma 4.5 (Visible Pumping). Let L be a message-passing recognisable language. There exists n ∈ ℕ such that for all input strings w, if w ∈ L and |w| ≥ n then w can be written as w_{1}w_{2}w_{3} such that |w_{1}w_{2}| ≤ n, |w_{2}| ≥ 1 and w_{1}w_{2}^{i}w_{3} ∈ L for all i ≥ 1.

Another consequence of Lemmas 4.2 and 4.3 is a strict hierarchy theorem for message-passing automata, whose proof we omit.

Lemma 4.6 (Counter Hierarchy). For k ∈ ℕ, let L_{k} be the set of languages recognisable by message-passing automata with k counters. Then, for all k, L_{k} ⊊ L_{k+1}.

5 Regularity of Message-Passing Recognisable Languages

Automata with bounded counters

Let A = (Q, Σ, Γ, T, q_{in}, F) be a message-passing automaton. For K ∈ ℕ, define A[K] = (Q[K], T [K], Q[K]_{in}, F [K]) to be the finite-state automaton over the alphabet Σ ∪ Γ^{±} given by:

– Q[K] = Q × \{f | f : Γ ⟶ [0..K]\}, with Q[K]_{in} = (q_{in}, \overline{0}).

– F [K] = F × {f | f : Γ ⟶ [0..K]}.

– If (q, d, q′) ∈ T, then ((q, f), d, (q′, f′)) ∈ T [K] where:

• If d ∈ Σ, f′ = f.

• If d = C^{+}, f′(C′) = f(C′) for all C′ ≠ C and

f′(C) = \{ \begin{matrix}f(C)+1 & if f(C) < K \\ K & otherwise. \end{matrix}

• If d = C^{−}, f′(C′) = f(C′) for all C′ ≠ C, f(C) ≥ 1 and

f′(C) = \{ \begin{matrix}f(C)−1 & if f(C) < K \\ K & otherwise. \end{matrix}

Each transition t = ((q, f), d, (q′, f′)) ∈ T [K] corresponds to a unique transition (q, d, q′) ∈ T, which we denote t^{−1}. For a sequence of transitions t_{1}t_{2} … t_{n}, we write (t_{1}t_{2} … t_{n})^{−1} for t_{1}^{−1}t_{2}^{−1} … t_{n}^{−1}. For any sequence t_{1}t_{2} … t_{n} of transitions

in T [K], α(t_{1}t_{2} … t_{n}) = α((t_{1}t_{2} … t_{n})^{−1}). Moreover, if (q_{0}, f′_{0}) ⟹^{t_{1}t_{2}...t_{n}} (q_{n}, f′_{n})

and (q_{0}, f_{0}) ⟹^{(t_{1}t_{2}...t_{n})^{−1}} χ_{n}, then Q(χ_{n}) = q_{n}.

Thus, the finite-state automaton A[K] behaves like a message-passing automaton except that it deems any counter whose value attains a value K to be “full” . Once a counter is declared to be full, it can be decremented as many times as desired. The following observations are immediate.

Proposition 5.1. (i) If (q_{0}, f′_{0}) ⟶^{t′_{1}} (q_{1}, f′_{1}) ⟶^{t′_{2}} ⋯ ⟶^{t′_{n}} (q_{n}, f′_{n}) is a computation of A then, (q_{0}, f_{0}) ⟶^{t_{1}} (q_{1}, f_{1}) ⟶^{t_{2}} ⋯ ⟶^{t_{n}} (q_{n}, f_{n}) is a computation of A[K] where

– t′_{1}t′_{2} … t′_{n} = (t_{1}t_{2} … t_{n})^{−1}.

– ∀C ∈ Γ. ∀i ∈ [1..n]. f_{i}(C) = \{ \begin{matrix}f′_{i}(C) & if f′_{j}(C) < K for all j ≤ i \\ K & otherwise \end{matrix}

(ii) Let (q_{0}, f_{0}) ⟶^{t_{1}} (q_{1}, f_{1}) ⟶^{t_{2}} ⋯ ⟶^{t_{n}} (q_{n}, f_{n}) be a computation of A[K]. Then there is a maximal prefix t_{1}t_{2} … t_{ℓ} of t_{1}t_{2} … t_{n} such that there is a

computation (q_{0}, f′_{0}) ⟶^{t_{1}^{−1}} (q_{1}, f′_{1}) ⟶^{t_{2}^{−1}} … ⟶^{t_{ℓ}^{−1}} (q_{ℓ}, f′_{ℓ}) of A with f_{0} = f′_{0}.

Moreover, if ℓ < n, then for some counter C, α(t′_{ℓ+1}) = C^{−}, f′_{ℓ}(C) = 0 and there is a j < ℓ such that f′_{j}(C) = K.

(iii) Let L(A[K]) be the language over Σ∪Γ^{±} accepted by A[K]. Let L_{Σ}(A[K]) = {w↾_{Σ} | w ∈ L(A[K])}. Then, L(A) ⊆ L_{Σ}(A[K]).

Synchronised products of message-passing automata

Product automata Let A_{i} = (Q_{i}, Σ_{i}, Γ_{i}, T_{i}, q_{in}^{i}, F_{i}), i = 1, 2, be a pair of message-passing automata. The product automaton A_{1} × A_{2} is the structure (Q_{1}×Q_{2}, Σ_{1}∪Σ_{2}, Γ_{1}∪Γ_{2}, T_{1}×T_{2}, (q_{in}^{1}, q_{in}^{2}), F_{1}×F_{2}), where ((q_{1}, q_{2}), d, (q′_{1}, q′_{2})) ∈ T_{1} × T_{2} iff one of the following holds:

– d ∈ (Σ_{1} ∪ Γ_{1}) ∩ (Σ_{2} ∪ Γ_{2}) and (q_{i}, d, q′_{i}) ∈ T_{i} for i ∈ {1, 2}.

– d ∈ (Σ_{1} ∪ Γ_{1}) \ (Σ_{2} ∪ Γ_{2}), (q_{1}, d, q′_{1}) ∈ T_{1} and q_{2} = q′_{2}.

– d ∈ (Σ_{2} ∪ Γ_{2}) \ (Σ_{1} ∪ Γ_{1}), (q_{2}, d, q′_{2}) ∈ T_{2} and q_{1} = q′_{1}.

For t = ((q_{1}, q_{2}), d, (q′_{1}, q′_{2})) ∈ T and i ∈ {1, 2}, let π_{i}(t) denote (q_{i}, d, q′_{i}) if d ∈ (Σ_{i} ∪ Γ_{i}) and the empty string ε otherwise. As usual, π_{i}(t_{1}t_{2} … t_{n}) is just π_{i}(t_{1})π_{i}(t_{2}) … π_{i}(t_{n}). Thus, for a sequence of transitions ρ = t_{1}t_{2} … t_{n} over T_{1}×T_{2}, π_{1}(ρ) and π_{2}(ρ) denote the projections of ρ onto the transitions of A_{1} and A_{2} respectively. Clearly, α(t_{1}t_{2} … t_{n})↾_{(Σ_{i}∪Γ_{i})} = α(π_{i}(t_{1}t_{2} … t_{n})) for i ∈ {1, 2}.

We shall often write a configuration ((q_{1}, q_{2}), f) of A_{1} × A_{2} as a pair of configurations ((q_{1}, f_{1}), (q_{2}, f_{2})) of A_{1} and A_{2}, where f_{1} and f_{2} are restrictions of f to Γ_{1} and Γ_{2} respectively.

The following observations are easy consequences of the definition of product automata.

Proposition 5.2. (i) ((q_{in}^{1}, \overline{0}), (q_{in}^{2}, \overline{0})) ⟹^{t_{1}t_{2}...t_{n}} ((q_{1}, f_{1}), (q_{2}, f_{2})) is a computa-

tion of A_{1}×A_{2} if and only if (q_{in}^{1}, \overline{0}) ⟹^{π_{1}(t_{1}t_{2}...t_{n})} (q_{1}, f_{1}) and (q_{in}^{2}, \overline{0}) ⟹^{π_{2}(t_{1}t_{2}...t_{n})}

(q_{2}, f_{2}) are computations of A_{1} and A_{2} respectively. (ii) If Σ_{1} = Σ_{2} and Γ_{1} ∩ Γ_{2} = ∅, then L(A_{1} × A_{2}) = L(A_{1}) ∩ L(A_{2}).

5.1 Regularity and closure under complementation

Our first characterisation of regular message-passing recognisable languages is the following.

Theorem 5.3. Let L be a language over Σ. L and \overline{L} are message-passing recognisable iff L is regular.

This result is related to the main result of [MNRS98] which states that if we record the behaviour of message-passing systems as tuples of sequences, every robust system is effectively finite-state. In the sequential setting, a language L would be robust in the sense of [MNRS98] if there were a single automaton A with accept and reject states such that for each word w ∈ L, every run of A on w leads to an accept state and for each word w ∉ L, every run of A on w leads to a reject state. Here, the requirement on L is much weaker—all we demand is that both L and \overline{L} be accepted independently by message-passing automata, possibly with very different state spaces.

To prove the theorem, we need an auxiliary result. Let L ⊆ Σ^{∗} be such that both L and its complement \overline{L} are message-passing recognisable. Let L = L(A) and \overline{L} = L(\overline{A}), where we may assume that A and \overline{A} use disjoint sets of counters.

The language accepted by A×\overline{A} must be empty. Let M be the number of states of A × \overline{A} and N be the number of counters that it uses. Let K be a number greater than Π_{M,N,0}, the strong pumping constant for (M, N, 0). Recall that A[K] = (Q[K], T [K], Q[K]_{in}, F [K]) is a finite-state automaton without counters working on the input alphabet Σ ∪ Γ^{±}.

Lemma 5.4. L(A[K] × \overline{A}) = ∅.

Proof. Let A[K] = (Q[K], T [K], Q[K]_{in}, F [K]) and \overline{A} = (\overline{Q}, Σ, \overline{Γ} , \overline{T} , \overline{q}_{in}\overline{F}). Each computation ρ of A[K]×\overline{A} is of the form ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟶^{u_{1}} ((q_{1}, f_{1}), (\overline{q}_{1}, \overline{f}_{1})) ⟶^{u_{2}}

⋯ ⟶^{u_{n}} ((q_{n}, f_{n}), (\overline{q}_{n}, \overline{f}_{n})), where, for i ∈ [0..n], u_{i} ∈ T [K] × \overline{T}.

By Propositions 5.1 and 5.2, corresponding to the sequence u_{1}u_{2} … u_{n} there exists a maximal sequence of transitions v_{1}v_{2} … v_{m} of A × \overline{A} where:

– Each v_{i} belongs to T × \overline{T}.

– For each i ∈ [1..m], π_{2}(v_{i}) = π_{2}(u_{i}).

– For each i ∈ [1..m], π_{1}(v_{i}) = \{ \begin{matrix}(π_{1}(u_{i}))^{−1} & if π_{1}(u_{i}) ≠ ε \\ ε & otherwise \end{matrix}

– ρ′ : ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟶^{v_{1}} ((q_{1}, f′_{1}), (\overline{q}_{1}, \overline{f}_{1})) ⟶^{v_{2}} ⋯ ⟶^{v_{m}} ((q_{m}, f′_{m}), (\overline{q}_{m}, \overline{f}_{m})) is

a computation of A × \overline{A}.

– If m < n, then for some Ĉ ∈ Γ, α(u_{m+1}) = Ĉ^{−}, f′_{m}(Ĉ) = 0 and f′_{j}(Ĉ) = K for some j ∈ [0..m].

Let us define the residue length of ρ to be n−m.

Suppose that L(A[K] × \overline{A}) is non-empty. Since L(A × \overline{A}) is empty, it is easy to see that any accepting run of A[K]×\overline{A} has a non-zero residue length. Without loss of generality, assume that the run ρ considered earlier is an accepting run of A[K] × \overline{A} whose residue length is minimal. Then, in the corresponding run ρ′ of A × \overline{A}, the counter Ĉ ∈ Γ attains the value K along ρ′ and then goes to 0 at the end of the run so that the move labelled Ĉ^{−} is not enabled at ((q_{m}, f′_{m}), (\overline{q}_{m}, \overline{f}_{m})).

Since K exceeds the strong pumping constant for A × \overline{A}, by Lemma 4.2 we

can find an alternative run ρ̂′ : ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟹^{v′_{1}v′_{2}...v′_{ℓ}} ((q′_{ℓ}, f′_{ℓ}), (\overline{q}′_{ℓ}, \overline{f}′_{ℓ})) with

(q′_{ℓ}, \overline{q}′_{ℓ}) = (q_{m}, \overline{q}_{m}), f′_{ℓ}(Ĉ) ≥ K, and all other counter values at (f′_{ℓ}, \overline{f}′_{ℓ}) at least as large as at (f_{m}, \overline{f}′_{m}). In particular, every counter which exceeded the cutoff value K along ρ′ is pumpable and thus exceeds K along ρ̂′ as well.

By Propositions 5.1 and 5.2, we can construct a corresponding sequence of transitions u′_{1}u′_{2} … u′_{ℓ} over T [K]×\overline{T} such that π_{1}(v′_{1}v′_{2} … v′_{ℓ}) = (π_{1}(u′_{1}u′_{2} … u′_{ℓ}))^{−1}

and π_{2}(v′_{1}v′_{2} … v′_{ℓ}) = π_{2}(u′_{1}u′_{2} … u′_{ℓ}), where ρ̂ : ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟹^{u′_{1}u′_{2}...u′_{ℓ}}

((q′′_{ℓ}, f′′_{ℓ}), (\overline{q}′_{ℓ}, \overline{f}′_{ℓ})) is a run of A[K] × \overline{A} with (q′′_{ℓ}, \overline{q}′_{ℓ}) = (q_{m}, \overline{q}_{m}) and f′′_{ℓ}(C) ≥ f_{m}(C) for each C ∈ Γ.

We already know that \overline{f}′_{ℓ}(C) ≥ \overline{f}_{m}(C) for each C ∈ \overline{Γ}. Further, since every counter which exceeded the cutoff value K along ρ′ also exceeds K along ρ̂′, we know that any counter which has become full along ρ would also have saturated along ρ̂. Thus, we can extend ρ̂ to an accepting run σ by appending the sequence of transitions u_{m+1}u_{m+2} … u_{n} which occur at the end of the accepting run ρ.

Recall that α(u_{m+1}) = Ĉ^{−} and f′_{ℓ}(Ĉ) ≥ 1 by our choice of ρ̂′. From this, it follows that the residue length of the newly constructed accepting run σ is at least one less than the residue length of ρ, which is a contradiction, since ρ was assumed to be an accepting run of minimal residue length. □

We can now prove Theorem 5.3.

Proof. (of Theorem 5.3) Let L = L(A) and \overline{L} = L(\overline{A}). Define A[K] as above. We claim that L_{Σ}(A[K]) = L(A). By Proposition 5.1, we know that L(A) ⊆ L_{Σ}(A[K]). On the other hand, from the previous lemma it follows that L_{Σ}(A[K])∩L(\overline{A}) = ∅. This implies that L_{Σ}(A[K]) ⊆ \overline{L(\overline{A})}, which means that L_{Σ}(A[K]) ⊆ L(A). So L(A) = L_{Σ}(A[K]). Since A[K] is a finite-state automaton, it follows that L(A) is regular. Therefore, if a language and its complement are message-passing recognisable then the language is regular.

The converse is obvious. □

Observe that our construction is effective—given message-passing automata A and \overline{A} for L and \overline{L} respectively, we can construct a finite-state automaton A[K] for L.

5.2 Regularity and determinacy

Our next characterisation of regularity is in terms of deterministic messagepassing automata.

Deterministic Message-Passing Automata A message-passing automaton A = (Q, Σ, Γ, T, q_{in}, F) is said to be deterministic if the following two conditions hold:

– If (q, d_{1}, q_{1}), (q, d_{2}, q_{2}) ∈ T, with d_{1}, d_{2} ∈ Σ, then d_{1} = d_{2} implies q_{1} = q_{2}.

– If (q, d_{1}, q_{1}), (q, d_{2}, q_{2}) ∈ T, with d_{1} ∈ Γ^{±}, then d_{1} = d_{2} and q_{1} = q_{2}.

Though this notion of determinism seems rather strong, any relaxation of the definition will allow deterministic automata to simulate non-deterministic automata in a trivial manner. If we permit the automaton to choose between a counter move and another transition (which may or may not be a counter move), we can add a spurious counter C and replace any non-deterministic choice between transitions t_{1} = (q, d, q_{1}) and t_{2} = (q, d, q_{2}) by a choice between t_{1} and a move (q, C^{+}, q_{C}) involving C which leads to a new state where t′_{2} = (q_{C}, d, q_{2}) is enabled.

The following result characterises languages accepted by deterministic messagepassing automata. Similar results have been demonstrated for deterministic Petri net languages [Pel87,V82].

Proposition 5.5. Let A be a deterministic message-passing automaton. Then, either L(A) is regular or there is a word w ∉ L(A) such that every extension of w also does not belong to L(A).

Proof Sketch. Let A be a deterministic message-passing automaton. We say that A is Γ -blocked on a word w if, while reading w, A gets stuck at a state with a single outgoing edge labelled C^{−}, for some counter C. If A is Γ -blocked on w, it is easy to see A is also Γ -blocked on w′ for any extension w′ of w, so every extension of w is outside L(A).

If A is not Γ -blocked for any word w, we construct a finite-state automaton A′ with ε-moves over Σ with the same state space as A. In A′, each counter move (q, d, q′), d ∈ Γ^{±}, is replaced by a ε-move (q, ε, q′). There is a natural correspondence between computations of A and runs of A′. It is easy to see that L(A) ⊆ L(A′). Using the fact that A is not Γ -blocked for any word w, we can show that any accepting run of A′ can be mapped back to an accepting run of A. Thus L(A′) ⊆ L(A). In other words, L(A′) = L(A), so L(A) is regular. □

The preceding characterisation implies that non-deterministic message-passing automata are strictly more powerful than deterministic message-passing automata. Consider the language L = {w | w = w_{1}a^{m}b^{n}aw_{2}} where w_{1}, w_{2} ∈ {a, b}^{∗} and m ≥ n ≥ 1. This language is message-passing recognisable but violates the condition of Proposition 5.5: L is not regular and for any word w ∉ L, we can always find an extension of w in L—for instance, waba ∈ L for all w ∈ {a, b}^{∗}.

Observe, however, that even deterministic message-passing automata are strictly more powerful than normal finite-state automata. For instance, the language L_{ge} of Example 2.1 is not regular but the automaton accepting the language is deterministic.

With these observations about deterministic automata behind us, we can now state our alternative characterisation of regularity. First, we need some notation. For a string w, let w^{R} denote the string obtained by reading w from right to left. For a language L, let L^{R} be the set of strings {w^{R} | w ∈ L}.

Theorem 5.6. Let L be a message-passing recognisable language such that L^{R} is recognised by a deterministic message-passing automaton. Then, L is regular.

The idea is to compute a constant τ which depends on the number of states M and the number of counters N of A and to then show that L is recognised by the finite-state automaton L[τ]. The proof is quite involved and we omit it due to lack of space.

6 Discussion

Other models for asynchronous commmunication Many earlier attempts to model asynchronous systems focus on the infinite-state case—for instance, the port automaton model of Panangaden and Stark [PS88] and the I/O automaton model of Lynch and Tuttle [LT87]. Also, earlier work has looked at issues far removed from those which are traditionally considered in the study of finite-state systems.

Recently, Abdulla and Jonsson have studied decision problems for distributed systems with asynchronous communication [AJ93]. However, they model channels as unbounded, fifo buffers, a framework in which most interesting questions become undecidable. The results of [AJ93] show that the fifo model becomes tractable if messages may be lost in transit: questions such as reachability of configurations become decidable. While their results are, in general, incomparable to ours, we remark that their positive results hold for our model as well.

Petri net languages Our model is closely related to Petri nets [G78,J86]. We can go back and forth between labelled Petri nets and message-passing networks while maintaining a bijection between the firing sequences of a net N and the computations of the corresponding automaton A.

There are several ways to associate a language with a Petri net [H75,J86,Pet81]. The first is to examine all firing sequences of the net. The second is to look at firing sequences which lead to a set of final markings. The third is to identify firing sequences which reach markings which dominate some final marking. The third class corresponds to message-passing recognisable languages.

A number of positive results have been established for the first class of languages—for instance, regularity is decidable [GY80,VV80]. On the other hand, a number of negative results have been established for the second class of languages—for instance, it is undecidable whether such a language contains all strings [VV80]. However, none of these results, positive or negative, carry over to the third class—ours is one of the few tangible results for this class of Petri net languages.

Directions for future work We believe that Theorem 5.6 holds even without the determinacy requirement on L^{R}. An interesting question is to develop a method for transforming sequential specifications in terms of message-passing automata into equivalent distributed specifications in terms of the message-passing network model of [MNRS98]. Another challenging question is the decidability of regularity for message-passing recognisable languages.

References

[AJ93] P.A. Abdulla and B. Jonsson: Verifying programs with unreliable channels, in Proc. 8th IEEE Symp. Logic in Computer Science, Montreal, Canada (1993).

[GY80] A. Ginzburg and M. Yoeli: Vector Addition Systems and Regular Languages, J. Comput. System. Sci. 20 (1980) 277–284

[G78] S.A. Greibach: Remarks on Blind and Partially Blind One-Way Multicounter Machines, Theoret. Comput. Sci 7 (1978) 311–324.

[H75] M. Hack: Petri Net Languages, C.S.G. Memo 124, Project MAC, MIT [H91] G.J. Holzmann: Design and validation of computer protocols, Prentice Hall

(1991).

[J86] M. Jantzen: Language Theory of Petri Nets, in W. Brauer, W. Reisig, G. Rozenberg (eds.), Petri Nets: Central Models and Their Properties, Advances in Petri Nets, 1986, Vol 1, Springer LNCS 254 (1986) 397–412.

[KM69] R.M. Karp and R.E. Miller: Parallel Program Schemata, J. Comput. System Sci., 3 (4) (1969) 167–195.

[LT87] N.A. Lynch and M. Tuttle: Hierarchical Correctness Proofs for Distributed Algorithms, Technical Report MIT/LCS/TR-387, Laboratory for Computer Science, MIT (1987).

[M78] A. Mazurkiewicz: Concurrent Program Schemes and their Interpretations, Report DAIMI-PB-78, Computer Science Department, Aarhus University, Denmark (1978).

[MNRS97] M. Mukund, K. Narayan Kumar, J. Radhakrishnan and M. Sohoni: Message-Passing Automata and Asynchronous Communication, Report TCS-97-4, SPIC Mathematical Institute, Madras, India (1997).

[MNRS98] M. Mukund, K. Narayan Kumar, J. Radhakrishnan and M. Sohoni: Robust Asynchronous Protocols are Finite-State, Proc. ICALP 98, Springer LNCS (1998) (to appear).

[PS88] P. Panangaden and E.W. Stark: Computations, Residuals, and the Power of Indeterminacy, in T. Lepisto and A. Salomaa (eds.), Proc. ICALP ’88, Springer LNCS 317 (1988) 439–454.

[Pel87] E. Pelz: Closure Properties of Deterministic Petri Nets, Proc. STACS 87, Springer LNCS 247, (1987) 371-382.

[Pet81] J.L. Peterson: Petri net theory and the modelling of systems, Prentice Hall (1981).

[VV80] R. Valk and G. Vidal-Naquet: Petri Nets and Regular Languages, J. Comput. System. Sci. 20 (1980) 299–325.

[V82] G. Vidal-Naquet: Deterministic languages for Petri nets, Application and Theory of Petri Nets, Informatik-Fachberichte 52, Springer-Verlag (1982).

[Z87] W. Zielonka: Notes on Finite Asynchronous Automata, R.A.I.R.O.—Inf. Théor. et Appl., 21 (1987) 99–135.