Automata, Languages and Programming, 25th International Colloquium Proceedings: Kim G. Larsen, Sven Skyum, Glynn Winskel (eds.) Springer Lecture Notes in Computer Science 1443 (1998), 188–199.

Robust Asynchronous Protocols Are Finite-State

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 consider networks of finite-state machines which communicate over reliable channels which may reorder messages. Each machine in the network also has a local input tape. Since channels are unbounded, the network as a whole is, in general, infinite-state.

An asynchronous protocol is a network equipped with an acceptance condition. Such a protocol is said to be robust if it never deadlocks and, moreover, it either accepts or rejects each input in an unambiguous manner. The behaviour of a robust protocol is insensitive to nondeterminism introduced by either message reordering or the relative speeds at which components read their local inputs.

Using an automata-theoretic model, we show that, at a global level, every robust asynchronous protocol has a finite-state representation. To prove this, we establish a variety of pumping lemmas. We also demonstrate a distributed language which does not admit a robust protocol.

1 Introduction

We analyze message-passing systems from a language-theoretic point of view. In such systems, computing agents run protocols to collectively process distributed inputs, using messages for coordination. These messages may undergo different relative delays and hence arrive out of order. Protocols need to be “robust” with respect to the irregular behaviour of the transmission medium.

Most protocols assume that the transmission medium has an unlimited capacity to hold messages—undelivered messages are assumed to be stored in a transparent manner in intermediate buffers. Can the unlimited capacity of the medium enhance the power of message passing protocols?

Unfortunately, the answer is no; we show that even for a benign medium which does not lose messages, a “robust” protocol cannot use unbounded buffers to its advantage. However, if a protocol need not always gracefully halt, then the medium can be exploited to accept a larger class of “distributed languages”.

⋆ 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.

Consider then a system of processes which interact independently with the environment and communicate internally via message-passing. The communication between the processes and the programs which they run impose restrictions on the distributed input—some interactions with the environment are valid and some are not. For instance, consider a banking network which is connected to the external world via a set of automated teller machines. The protocol may enforce a limit on the number of withdrawals by an individual across the network.

We are interested in finite-state processes, so we assume that the number of different types of messages used by the system is finite. This is not unreasonable if we distinguish “control” messages from “data” messages. In our model, channels may reorder or delay messages. For simplicity, we assume that 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 which have been sent along the channel but are as yet undelivered.

We say that an asynchronous protocol is robust if it never deadlocks on any distributed input and every distributed input is either accepted or rejected in a consistent manner. In other words finite delays, reordering of messages and nondeterministic choices made by the protocol do not affect the outcome of a robust protocol on a given distributed input.

Our main result is that every language of distributed inputs accepted by a robust asynchronous protocol can be “represented” by a regular sequential language. In other words, a robust asynchronous protocol always has a globally finite-state description. This implies that robust protocols essentially use messages only for “handshaking”. Since robust protocols can be modelled as finite-state systems, they may, in principle, be verified using automated tools [5].

The paper is organized as follows. In the next section, we define messagepassing networks. In Section 3 we state some basic results about these networks, including a Contraction Lemma which leads to the decidability of the emptiness problem. Section 4 develops a family of pumping lemmas which are exploited in Section 5 to prove our main result about robust protocols. We also describe a simple language for which no robust protocol exists. In the final section, we discuss the connection between our results and those in Petri net theory and point out directions for future work. We have had to omit detailed proofs in this extended abstract. Full proofs and related results can be found in [10].

2 Message-passing networks

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. For \overline{m} = ⟨m_{1}, m_{2}, …, m_{k}⟩ and \overline{n} = ⟨n_{1}, n_{2}, …, n_{k}⟩, \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 (S_{a}, S_{t}, Σ, #, Γ, T, s_{in}) where:

– S_{a} and S_{t} are disjoint, non-empty, finite sets of active and terminal states, respectively. The initial state s_{in} belongs to S_{a}.

– Σ is a finite input alphabet and # is a special end-of-tape symbol which does not belong to Σ. Let Σ^{#} denote the set Σ ∪ {#}.

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

– T ⊆ (S_{a} ×(Σ ∪Γ^{±})×S_{a})∪(S_{a} ×{#}×S_{t})∪(S_{t} ×Γ^{±} ×S_{t}) is the transition relation.

A message-passing automaton begins reading its input in an active state. It remains within the set of active states until it reads the special end-of-tape symbol. At this point, the automaton moves into the set of terminal states where the only moves possible are those which increment or decrement counters.

Networks A message-passing network is a structure N = ({A_{i}}_{i∈[1..n]}, Acc, Rej) where:

– For i ∈ [1..n], A_{i} = (S_{a}^{i}, S_{t}^{i}, Σ_{i}, #_{i}, Γ_{i}, T_{i}, s_{in}^{i}) is a message-passing automaton. As before, for i ∈ [1..n], Σ_{i}^{#} denotes the set Σ_{i} ∪ {#_{i}}.

– For i, j ∈ [1..n], if i ≠ j then Σ_{i} ∩ Σ_{j} = ∅.

– A global state of N is an n-tuple ⟨s_{1}, s_{2}, …, s_{n}⟩ where s_{i} ∈ (S_{a}^{i} ∪ S_{t}^{i}) for i ∈ [1..n]. Let Q_{N} denote the set of global states of N. If q = ⟨s_{1}, s_{2}, …, s_{n}⟩ is a global state, then q_{i} denotes the i^{th} component s_{i}. The initial state of N is given by q_{in} = ⟨s_{in}^{1}, s_{in}^{2}, …, s_{in}^{n}⟩. The terminal states of N, denoted Q_{N}^{t}, are given by ∏_{i∈[1..n]} S_{t}^{i}. The sets Acc and Rej are disjoint subsets of Q_{N}^{t}; Acc is the set of accept states of N while Rej is the set of reject states. We do not insist that Q_{N}^{t} = Acc ∪ Rej—there may be terminal states which are neither accepting nor rejecting.

Counters may be shared across the network—shared counters represent channels along which components send messages to each other. Strictly speaking, a point-to-point channel would consist of a set of counters shared by two processes, where one process only increments the counters and the other only decrements the counters. Our definition permits a more generous notion of channels.

The assumption that local alphabets are pairwise disjoint is not critical—we can always tag each input letter with the location where it is read.

Let Σ_{N} denote ⋃_{i∈[1..n]} Σ_{i}^{#} and Γ_{N} denote ⋃_{i∈[1..n]} Γ_{i}.

Global transitions For a network N, we can define a global transition relation T_{N} as follows. For q, q′ ∈ Q_{N} and d ∈ Σ_{N} ∪Γ_{N}^{±}, (q, d, q′) belongs to T_{N} provided:

– For some i ∈ [1..n], d ∈ Σ_{i}^{#} ∪ Γ_{i}^{±} and (q_{i}, d, q′_{i}) ∈ T_{i}.

– For j ≠ i, q_{j} = q′_{j}.

Configurations A configuration of N is a pair (q, f) where q ∈ Q_{N} and f : Γ → ℕ 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 The network moves from configuration χ to configuration χ′ on d ∈ Σ_{N} ∪ Γ_{N}^{±} if (Q(χ), d, Q(χ′)) ∈ T_{N} and one of the following holds:

– d ∈ Σ_{N} 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_{N}. Given a sequence of transitions t_{1}t_{2} … t_{m} = (q_{1}, d_{1}, q_{2})(q_{2}, d_{2}, q_{3}) … (q_{m}, d_{m}, q_{m+1}), the corresponding sequence d_{1}d_{2} … d_{m} over Σ_{N} ∪ Γ_{N}^{±} is denoted α(t_{1}t_{2} … t_{m}).

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

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

If w is a string over a set X and Y ⊆ X, we write w ↾_{Y} to denote the subsequence of letters from Y in w.

An input to the network N is an n-tuple \overline{w} = ⟨w_{1}, w_{2}, …, w_{n}⟩—each component w_{i} is a word over the local alphabet Σ_{i}. As we shall see when we define the notion of a run, each component w_{i} of the input \overline{w} is assumed to be terminated by the end-of-tape symbol #_{i} which is not recorded as part of the input.

A run of N over \overline{w} is a 0-computation χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} where Q(χ_{0}) = q_{in}, Q(χ_{m}) ∈ Acc ∪ Rej and α(t_{1}t_{2} … t_{m})↾_{Σ_{i}^{#}} = w_{i}#_{i} for each i ∈ [1..n]. The run is said to be accepting if Q(χ_{m}) ∈ Acc and rejecting if Q(χ_{m}) ∈ Rej. The input \overline{w} is accepted by N if N has an accepting run over \overline{w}.

A 0-computation starting from the initial state which reads the entire input is not automatically a run—a run must end in an accept or a reject state. As usual, an input \overline{w} is not accepted if all runs on \overline{w} end in reject states—in particular, if the network does not admit any runs on \overline{w}, then \overline{w} is not accepted by N.

Languages A tuple language over ⟨Σ_{1}, Σ_{2}, …, Σ_{n}⟩ is a subset of ∏_{i∈[1..n]} Σ_{i}^{∗}. The language accepted by N, denoted L(N), is the set of all inputs accepted by N. A tuple language L is said to be message-passing recognizable if there is a network N = {A_{i}}_{i∈[1..n]} with input alphabets {Σ_{i}}_{i∈[1..n]} such that L = L(N).

We will also be interested in the connection between sequential languages over Σ_{N} and tuple languages accepted by message-passing networks. We say that a word w over Σ_{N} represents the tuple ⟨w_{1}, w_{2}, …, w_{n}⟩ if w↾_{Σ_{i}^{#}} = w_{i}#_{i} for each i ∈ [1..n]. We call the word ⟨w ↾_{Σ_{1}} , w ↾_{Σ_{2}} , …, w ↾_{Σ_{n}} ⟩ represented by w the N -projection of w. Let L_{s} ⊆ Σ_{N}^{∗} and L ⊆ ∏_{i∈[1..n]} Σ_{i}^{∗}. We say that L_{s} represents L if the following conditions hold:

– For each word w in L_{s}, the N -projection of w belongs to L.

– For each tuple \overline{w} = ⟨w_{1}, w_{2}, …, w_{n}⟩ in L, there is a word w in L_{s} which represents \overline{w}.

Example 2.1. Let Σ_{1} = {a} and Σ_{2} = {b}. Let L_{ge} denote the language {⟨a^{ℓ}, b^{m}⟩ | ℓ ≥ m}. Figure 1 shows a network which accepts L_{ge}. The initial state of each component is marked ⇓ while the terminal states are marked by double circles. There is one accept state, ⟨s, s⟩, and no reject state.

a A^{+} ⇓ D^{+}  #_{1} s  ⇓ D^{−}  A^{−} b  s #^{2} Fig. 1.

Each time the second process reads b it has to consume a message generated by the first process after reading a. Thus, the second process can read at most as many b’s as the first process does a’s. The counter D is used to signal that the first process’s input has been read completely.

Robustness In general, an asynchronous protocol may process the same distributed input in many different ways because of variations in the order in which components read their local inputs, reordering of messages due to delays in transmission as well as local nondeterminism at each component. Intuitively, a protocol is robust if its behaviour is insensitive to these variations—for each distributed input, all possible runs lead either to acceptance or rejection in a consistent manner. Further, a robust protocol should never deadlock along any computation—in other words, every input is processed fully and clearly identified as “accept” or “reject”. This motivates following definition.

Robust networks Let N be a message-passing network. We say that N is robust if the following hold:

– For each input \overline{w} = ⟨w_{1}, w_{2}, …, w_{n}⟩, N admits at least one run over \overline{w}. Moreover, if ρ and ρ′ are two different runs of N over \overline{w}, either both are accepting or both are rejecting.

– Let \overline{w} = ⟨w_{1}, w_{2}, …, w_{n}⟩ be any input and ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} a 0-computation of N such that Q(χ_{0}) = q_{in}. If α(t_{1}t_{2} … t_{m})↾_{Σ_{i}^{#}} is a prefix of w_{i}#_{i} for each i ∈ [1..n], then ρ can be extended to a run on \overline{w}.

It is easy to observe that if we interchange the accept and reject states of a robust network N, we obtain a robust network for the complement of L(N).

The network in Example 2.1 is not robust—if the number of b’s exceeds the number of a’s, the network hangs.

Example 2.2. We can make the network of Example 2.1 robust by changing the interaction between the processes. Rather than having the first process send a count of the number of inputs it has read, we make the processes read their inputs alternately, with a handshake in-between.

As before, let Σ_{1} = {a}, Σ_{2} = {b} and L_{ge} = {⟨a^{ℓ}, b^{m}⟩ | ℓ ≥ m}. Figure 2 shows is a robust network for L_{ge}. The initial states are marked ⇓ and the terminal states of each component are marked by double circles. There is one accept state, ⟨s, s⟩, and one reject state ⟨s, r⟩. The terminal states ⟨s, t⟩, ⟨t, r⟩, ⟨t, s⟩ and ⟨t, t⟩ are neither accepting nor rejecting.

a  A^{+} #_{1} ⇓  ⇓ b t  s  t C^{+}  #_{2}  #_{2} r D^{−} C^{−} #_{1}  B^{+} A^{−}  b s D^{+} B^{−}  #_{2} a  b Fig. 2.

The loops enclosed by dashes represent the phase when the processes read their inputs alternately. This phase ends either when either process reads its end-of-tape symbol. If the loop ends with first process reading #_{1}, the second process must immediately read #_{2}. If the loop ends with the second process reading #_{2}, the first process can go on to read any number of a’s.

3 Analyzing Message-Passing Networks

The next two sections contain technical results about message-passing networks that we need to prove our main theorem. Many of these results have analogues in Petri net theory [13]—a detailed discussion is presented in the final section.

The following result is basic to analyzing the behaviour of message-passing networks. 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 3.1. 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}.

Using the weak pumping constant, we can identify when a run of a network can be contracted by eliminating a sequence of transitions. We omit the proof.

Lemma 3.2 (Contraction). Let N be a message-passing network with M global states and N counters. For any K-computation χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} with m >

π_{M,N,K}, there exist i and j, m−π_{M,N,K} ≤ i < j ≤ m, such that χ′_{0} ⟹^{t_{1}...t_{i}t_{j+1}...t_{m}}

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

Corollary 3.3. A message-passing network with M global states and N counters has an accepting run iff it has an accepting run 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.

Corollary 3.4. The emptiness problem for message-passing networks is decidable.

4 A Collection of Pumping Lemmas

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∈Γ_{N}}.

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

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

to be pumpable if it satisfies the following conditions:

(i) y ≤ N. (ii) For each k ∈ [1..y], Q(χ_{i_{k}}) = Q(χ_{j_{k}}). (iii) For each v_{k}, k ∈ [1..y], Δv_{k} has at least one positive entry. (iv) Let C be a counter and k ∈ [1..y] 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_{y} as the pumpable blocks of the decomposition. We say that C is a pumpable counter if Δ_{C}(v_{k}) > 0 for some pumpable block v_{k}. 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 [7].)

Lemma 4.1 (Counter Pumping). Let N be a network and ρ a K-computation of N, K ∈ ℕ, with a pumpable decomposition of the form χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}}

χ_{j_{1}} ⋯ ⟹^{u_{y}} χ_{i_{y}} ⟹^{v_{y}} χ_{j_{y}} ⟹^{u_{y+1}} χ_{m}. Then, for any I, J ∈ ℕ, with I ≥ 1, there

exist ℓ_{1}, ℓ_{2}, …, ℓ_{y} ∈ ℕ and a K-computation ρ′ of N of the form χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}}

χ′_{j′_{1}} ⋯ ⟹^{u_{y}} χ′_{i′_{y}} ⟹^{v_{y}^{ℓy}} χ′_{j′_{y}} ⟹^{u_{y+1}} χ′_{p} such that ρ′ satisfies the following properties:

(i) χ_{0} = χ′_{0}. (ii) Q(χ′_{p}) = Q(χ_{m}). (iii) For i ∈ [1..y], ℓ_{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.

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-computation 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.2 (Decomposition). Let N be a network with M global states and N counters and let K ∈ ℕ. Let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be any K-computation of N. Then, there is a pumpable decomposition χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⋯ ⟹^{u_{y}} χ_{i_{y}} ⟹^{v_{y}} χ_{j_{y}} ⟹^{u_{y+1}} χ_{m} of ρ such that for every counter C, if C(χ_{j}) > Π_{M,N,K} for some j ∈ [0..m], then C is a pumpable counter in this decomposition.

Proof Sketch: The proof is by induction on N, the number of counters. In the induction, the key step is to identify a prefix ρ′ of ρ containing two configurations χ_{r} and χ_{s} such that Q(χ_{r}) = Q(χ_{s}), F (χ_{r}) < F (χ_{s}) and, moreover, no counter value exceeds π_{M,N,K} + K within ρ′.

Having found such a prefix, we fix a counter C which increases between χ_{r} and χ_{s} and construct a new network N′ which treats {C^{+}, C^{−}} as input letters. Since N′ has N−1 counters, the induction hypothesis yields a decomposition u_{2}v_{2}u_{3}v_{3} … u_{y}v_{y}u_{y+1} of the suffix of ρ after ρ′. We then set u_{1} to be the segment from χ_{0} to χ_{r} and v_{1} to be the segment from χ_{r} to χ_{s} and argue that the resulting decomposition u_{1}v_{1}u_{2}v_{2} … u_{y}v_{y}u_{y+1} of ρ satisfies the conditions of the lemma.

⊓ ⊔

The Decomposition Lemma plays a major role in the proof of our main result.

5 Robustness and Regularity

The main technical result of this paper is the following.

Theorem 5.1. Let N be a robust message-passing network. Then, there is a regular sequential language L_{s} over Σ_{N} which represents the tuple language L(N).

This means that at a global level, any robust asynchronous protocol can be substituted by an equivalent finite-state machine. To prove this result, we need some technical machinery.

Networks with bounded counters Let N = ({A_{i}}_{i∈[1..n]}, Acc, Rej) be a message-passing network. For K ∈ ℕ, define N [K] = (Q[K], T [K], Q[K]_{in}, F [K]) to be the finite-state automaton over the alphabet Σ_{N} ∪ Γ_{N}^{±} given by:

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

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

– If (q, d, q′) ∈ T_{N}, then ((q, f), d, (q′, f′)) ∈ T [K] where: • If d ∈ Σ_{N}, f′ = f.

• If d = C^{+}, f′(C′) = f(C′) for 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 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_{N}, which we denote t^{−1}. For any sequence t_{1}t_{2} … t_{m} of transitions

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

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

Thus, the finite-state automaton N [K] behaves like a message-passing network 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.2. (i) If (q_{0}, f′_{0}) ⟶^{t′_{1}} ⋯ ⟶^{t′_{m}} (q_{n}, f′_{m}) is a computation of N then, (q_{0}, f_{0}) ⟶^{t_{1}} ⋯ ⟶^{t_{m}} (q_{m}, f_{m}) is a computation of N [K] where

– t′_{1} … t′_{m} = t_{1}^{−1} … t_{m}^{−1}.

– ∀C ∈ Γ. ∀i ∈ [1..m]. 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}} ⋯ ⟶^{t_{m}} (q_{m}, f_{m}) be a computation of N [K]. There is a max-

imum prefix t_{1} … t_{ℓ} of t_{1} … t_{m} such that N has a computation (q_{0}, f′_{0}) ⟶^{t_{1}^{−1}}

… ⟶^{t_{ℓ}^{−1}} (q_{ℓ}, f′_{ℓ}) with f_{0} = f′_{0}. Moreover, if ℓ < m, then for some counter C, α(t_{ℓ+1}^{−1}) = C^{−}, f′_{ℓ}(C) = 0 and for some j < ℓ, f′_{j}(C) = K.

(iii) Let L_{seq}(N) denote the set of all words over Σ_{N} which arise in accepting runs of N —in other words, w ∈ L_{seq}(N) if there is an accepting run

χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} of N such that w = α(t_{1}t_{2} … t_{m})↾_{Σ_{N}} . Let L_{Σ_{N}} (N [K]) =

{w↾_{Σ_{N}} | w ∈ L(N [K])}. Then, L_{seq}(N) ⊆ L_{Σ_{N}} (N [K]).

We can now prove our main result.

Proof Sketch: (of Theorem 5.1) Let N be a robust network with M global states and N counters. By interchanging the accept and reject states, we obtain a robust network \overline{N} for \overline{L(N)} with the same state-transition structure as N. Let K denote Π_{M,N,0}, the strong pumping constant for N (and \overline{N}). Consider the finite-state automaton N [K] generated from N by ignoring all counter values above K.

We know that L_{seq}(N) is a subset of L_{Σ_{N}} (N [K]). We claim that there is no word w ∈ L_{Σ_{N}} (N [K]) which represents an input ⟨w_{1}, w_{2}, …, w_{n}⟩ from L(\overline{N}).

Assuming the claim, it follows that for every word w in L_{Σ_{N}} (N [K]), the N -projection ⟨w ↾_{Σ_{1}} , w ↾_{Σ_{2}} , …, w ↾_{Σ_{n}} ⟩ belongs to L(N). On the other hand, since L_{seq}(N) is a subset of L_{Σ_{N}} (N [K]), every tuple ⟨w_{1}, w_{2}, …, w_{n}⟩ in L(N) is represented by some word in L_{Σ_{N}} (N [K]). Thus, L_{Σ_{N}} (N [K]) represents the language L(N). Since N [K] is a finite-state automaton, the result follows.

To complete the proof, we must verify the claim. Suppose that there is a word w in L_{Σ_{N}} (N [K]) which represents a tuple ⟨w_{1}, w_{2}, …, w_{n}⟩ in L(\overline{N}). There must be a run ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} of N [K] on w which leads to a final state (q, f), where q is an accept state of N and hence a reject state of \overline{N}.

Since \overline{N} has the same structure as N, by Proposition 5.2 it is possible to mimic ρ in \overline{N}. However, since ⟨w_{1}, w_{2}, …, w_{n}⟩ ∈ L(\overline{N}) and \overline{N} is robust, it is not possible to mimic all of ρ in \overline{N} —otherwise, \overline{N} would admit both accepting and rejecting runs on ⟨w_{1}, w_{2}, …, w_{n}⟩. So, \overline{N} must get “stuck” after some prefix ρ_{1} : χ_{0} ⟹^{t_{1}t_{2}...t_{ℓ}} χ_{ℓ} of ρ—for some counter C, t_{ℓ+1} is a C^{−} move with C(χ_{ℓ}) = 0.

We call the residual computation ρ_{2} : χ_{ℓ} ⟹^{t_{ℓ+1}t_{ℓ+2}...t_{m}} χ_{m} the stuck suffix of ρ. Without loss of generality, assume that ρ has a stuck suffix of minimum length among all accepting runs over words in L_{Σ_{N}} (N [K]) representing tuples in L(\overline{N}).

Let u be the prefix of w which has been read in ρ_{1} and v be the suffix of w which is yet to be read. Let ⟨u_{1}, u_{2}, …, u_{n}⟩ and ⟨v_{1}, v_{2}, …, v_{n}⟩ be the N - projections of u and v, respectively. Clearly, u_{i} is a prefix of w_{i}#_{i} for each i ∈ [1..n]. Since \overline{N} is robust, there must be an extension of ρ_{1} to a run over ⟨w_{1}, w_{2}, …, w_{n}⟩—this run must be accepting since ⟨w_{1}, w_{2}, …, w_{n}⟩ ∈ L(\overline{N}).

Since N [K] can decrement C after ρ_{1} while \overline{N} cannot, C must have attained the value K along ρ_{1}. By Lemmas 4.1 and 4.2, we can transform ρ_{1} into a computation ρ′_{1} of \overline{N} which reaches a configuration χ_{ρ′_{1}} with Q(χ_{ρ′_{1}}) = Q(χ_{ℓ}), C(χ_{ρ′_{1}}) > 0 and F (χ_{ρ′_{1}}) ≥ F (χ_{ℓ}).

Let ⟨u′_{1}, u′_{2}, …, u′_{n}⟩ be the input read along ρ′_{1}. Since ρ_{1} could be extended to an accepting run of \overline{N} over ⟨u_{1}v_{1}, …, u_{n}v_{n}⟩, ρ′_{1} can be extended to an accepting run of \overline{N} over ⟨u′_{1}v_{1}, …, u′_{n}v_{n}⟩. On the other hand, we can extend ρ′_{1} in N [K] to a successful run over u′v, where u′ is the sequentialization of ⟨u_{1}, u_{2}, …, u_{n}⟩ along ρ′_{1}. This means that u′v ∈ L_{Σ_{N}} (N [K]) represents a tuple in L(\overline{N}).

Since the counter C has a non-zero value after ρ′_{1}, we can extend ρ′_{1} in \overline{N} to execute some portion of the stuck suffix ρ_{2} of ρ. If this extension of ρ′_{1} gets stuck, we have found a run which has a shorter stuck suffix than ρ, contradicting our assumption that ρ had a stuck suffix of minimum length.

On the other hand, if we can extend ρ′_{1} to mimic the rest of ρ, we find that \overline{N} has an accepting run on ⟨u′_{1}v_{1}, …, u′_{n}v_{n}⟩ as well as a rejecting run on ⟨u′_{1}v_{1}, …, u′_{n}v_{n}⟩. This contradicts the robustness of \overline{N}.

Thus it must be the case that there is no word w which is accepted by N [K] but which represents a tuple in L(\overline{N}).

⊓ ⊔

Example 5.3. Consider a network with two processes where Σ_{1} = {a, c} and Σ_{2} = {b, d}. Let L = {⟨a^{i}c^{k}, b^{j}d^{ℓ}⟩ | i ≥ ℓ and j ≥ k}. We can modify the network in Example 2.1 to accept L—we use two counters A and B to store the number of a’s and b’s read, respectively. We then decrement B each time c is read and A each time d is read to verify if the input is in L.

However, there is no robust protocol for L. If L has a robust protocol, there must be a regular language L_{s} which represents L. Let A be a finite-state automaton for L_{s} with n states. Choose a string w ∈ L_{s} which has at least n occurrences each of c and d. It is easy to see that either all d’s in w occur after all a’s or all c’s in w occur after all b’s. We can then pump a suffix of w so that either the number of d’s exceeds the number of a’s or the number of c’s exceeds the number of b’s, thereby generating a word u ∈ L_{s} with ⟨u↾_{Σ_{1}} , u↾_{Σ_{2}} ⟩ ∉ L.

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 [12] and the I/O automaton model of Lynch and Tuttle [8]. 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 [1]. However, they model channels as unbounded, fifo buffers, a framework in which most interesting questions become undecidable. The results of [1] 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 [3, 6]. 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 network N.

There are several ways to associate a language with a Petri net [4, 6, 13]. 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. A third possibility is to identify firing sequences which reach markings which dominate some final marking. The third class corresponds to message-passing recognizable languages.

A number of positive results have been established for the first class of languages—for instance, regularity is decidable [2, 14]. 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 [14]. 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 A challenging problem is to synthesize a distributed protocol from a description in terms of global states. In systems with synchronous communication, this is possible using an algorithm whereby each process maintains the latest information about the rest of the system [11, 15]. This algorithm has been extended to message-passing systems and could help in solving the synthesis problem [9]. Another important question is to be able to decide whether a given protocol is robust. We believe the problem is decidable.

References

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

2. A. Ginzburg and M. Yoeli: Vector addition systems and regular languages, J. Comput. System. Sci. 20 (1980) 277–284

3. S.A. Greibach: Remarks on blind and partially blind one-way multicounter machines, Theoret. Comput. Sci 7 (1978) 311–324.

4. M. Hack: Petri Net Languages, C.S.G. Memo 124, Project MAC, MIT (1975).

5. G.J. Holzmann: Design and validation of computer protocols, Prentice Hall (1991).

6. M. Jantzen: Language theory of Petri nets, in W. Brauer, W. Reisig, G. Rozenberg (eds.), Advances in Petri Nets, 1986, Vol 1, Springer LNCS 254 (1986) 397–412.

7. R.M. Karp and R.E. Miller: Parallel program schemata, J. Comput. System Sci., 3 (4) (1969) 167–195.

8. N.A. Lynch and M. Tuttle: Hierarchical correctness proofs for distributed algorithms, MIT/LCS/TR-387, Laboratory for Computer Science, MIT (1987).

9. M. Mukund, K. Narayan Kumar and M. Sohoni: Keeping track of the latest gossip in message-passing systems, Proc. Structures in Concurrency Theory (STRICT), Berlin 1995, Workshops in Computing Series, Springer-Verlag (1995) 249–263.

10. M. Mukund, K. Narayan Kumar, J. Radhakrishnan and M. Sohoni: Counter automata and asynchronous communication, Report TCS-97-4, SPIC Mathematical Institute, Madras, India (1997).

11. M. Mukund and M. Sohoni: Gossiping, asynchronous automata and Zielonka’s theorem, Report TCS-94-2, School of Mathematics, SPIC Science Foundation, Madras, India (1994).

12. P. Panangaden and E.W. Stark: Computations, residuals, and the power of indeterminacy, Proc. ICALP ’88, Springer LNCS 317 (1988) 439–454.

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

14. R. Valk and G. Vidal-Naquet: Petri nets and regular languages, J. Comput. System. Sci. 23 (3) (1981) 299–325.

15. W. Zielonka: Notes on finite asynchronous automata, R.A.I.R.O.—Inf. Théor. et Appl., 21 (1987) 99–135.