Internal Report  TCS-93-5

October, 1993

Determinizing Asynchronous Automata

Nils Klarlund^{1}, Madhavan Mukund^{2}, Milind Sohoni^{2}

Abstract

A concurrent version of a finite-state automaton is a set of processes that cooperate in processing letters of the input. Each letter read prompts some of the processes to synchronize and decide on a joint move according to a non-deterministic transition relation. Such automata are known as asynchronous automata.

The question whether these automata can be determinized while retaining the synchronization structure has already been answered in the positive, but indirectly, by means of sophisticated algebraic techniques.

In this paper we present an elementary proof, which generalizes the classic subset construction for finite-state automata. The proof uses in an essential way an earlier finite-state construction by Mukund and Sohoni for maintaining each process’s latest knowledge about other processes.

Our construction is only double-exponential and thus is the first to essentially match the lower bound.

In conjunction with earlier results of Ochmanski and Pighizzini, our construction provides a new (and in a sense “classical”) proof of Zielonka’s theorem that every recognizable trace language is accepted by a deterministic asynchronous automaton whose structure precisely captures the independence relation of the given trace alphabet.

1Computer Science Department, Aarhus University, Ny Munkegade, DK 8000 Aarhus C, Denmark. E-mail: klarlund@daimi.aau.dk

2School of Mathematics, SPIC Science Foundation, 92 G N Chetty Road, T Nagar, Madras 600 017, India. E-mail: {madhavan,sohoni}@ssf.ernet.in

This report is also published as Report DAIMI PB-460, Computer Science Department, Aarhus University, Aarhus, Denmark.

Introduction

Asynchronous automata were introduced by Zielonka as a natural generalization of finitestate automata for concurrent systems [Zie]. An asynchronous automaton consists of a set of components, or processes, which periodically synchronize to process their input. Each letter a in the alphabet is associated with a subset θ(a) of processes. The processes in θ(a) synchronize on reading a and jointly decide on a move. The processes outside θ(a) remain unchanged during this move—in fact, they are oblivious to the occurrence of a.

A distributed alphabet of this type gives rise to an independence relation I between letters: (a, b) ∈ I iff θ(a) ∩ θ(b) = ∅. Thus a and b are independent when processed by disjoint sets of components.

An alphabet with an independence relation is also called a concurrent alphabet. This notion was introduced by Mazurkiewicz as a technique for studying concurrent systems from the viewpoint of formal language theory [Maz]. Given a concurrent alphabet (Σ, I), I induces a natural equivalence relation ∼ on Σ^{∗}: two words w and w′ are related by ∼ iff w′ can be obtained from w by a sequence of permutations of adjacent independent letters. The equivalence class [w] containing w is called a trace.

A language L ⊆ Σ^{∗} is said to be a trace language if L is closed under ∼—i.e., for each w ∈ Σ^{∗}, w is in L iff every word in [w] is L. A trace language is recognizable if it is accepted by a conventional finite state automaton.

However, since conventional automata are sequential, it is quite awkward to precisely characterize the class of automata which recognize trace languages. Asynchronous automata, on the other hand, are natural machines for recognizing these languages. If we distribute Σ in such a way that the induced independence relation is precisely I, we are guaranteed that the language accepted by the automaton is closed under ∼.

Despite this simple connection, it is hard to prove that the class of languages accepted by asynchronous automata coincides with the class of recognizable trace languages. This result was first established by Zielonka [Zie]. Given a conventional finite automaton recognizing a trace language over (Σ, I), he showed how to construct directly a deterministic asynchronous automaton over a distributed alphabet (Σ, θ) recognizing the same language, such that the independence relation induced by θ is precisely I. The proof involves combinatorics over partially commutative monoids and is quite difficult to grasp. A comprehensive survey of the theory of recognizable trace languages can be found in [Die].

Contributions of this paper

In this paper, we generalize the classic subset construction of Rabin and Scott in order to obtain a direct procedure for determinizing an asynchronous automaton 𝔄. To our knowledge, this construction is the first that involves only a double-exponential blow-up in the size of the state spaces. We also show that this bound is essentially optimal.

The only other known way to determinize a non-deterministic asynchronous automaton 𝔄 is to view it as a normal non-deterministic automaton at the level of “global states” and then apply Zielonka’s construction to obtain a deterministic asynchronous automaton.

Our construction is the last piece needed for a “classical” proof of Zielonka’s theorem that recognizable trace languages coincide with the languages accepted by (deterministic) asynchronous automata. Even before Zielonka’s result, Ochmanski had defined a class of rational expressions that precisely generate recognizable trace languages [Och]. Ochmanski’s characterization is effective—in particular, given a finite automaton recognizing a trace language we can construct a rational expression for the language. Recently, Pighizzini has shown how to construct, inductively, a non-deterministic automaton 𝔄(E) for any (Ochmanski)-rational expression E such that 𝔄(E) accepts exactly the rational subset of Σ^{∗} associated with E [Pig]. Further, the size of 𝔄(E) is polynomial in the length of E. Given our construction, we can now convert 𝔄(E) into a deterministic asynchronous automaton 𝔅(E) which also accepts the same set. This proof of Zielonka’s theorem is analogous to the “textbook” proof that sets defined by regular expressions coincide with sets recognized by deterministic finite state automata [HU].

The paper is organized as follows. We begin by describing asynchronous automata and fixing some notation that we use in the paper. Then, we describe the distinction between local and global views of a word over a distributed alphabet. In Section 3 we define local runs and show how to characterize global runs of asynchronous automata as special products of local runs. The rest of the paper is devoted to showing how to maintain finite sets of local runs which retain all the necessary information about global runs. The crucial notion is that of a frontier, defined in Section 4. Section 5 introduces primary and secondary events, which between them subsume the frontiers. The “gossip automaton” of [MS], which locally updates primary and secondary information is described in the next section. All these notions are finally put together in Section 7 which presents the overall determinization construction. In Section 8 we analyze the complexity of our construction and provide a simple lower bound.

1 Preliminaries

Distributed alphabet Let 𝒫 be a finite set of processes. A distributed alphabet is a pair (Σ, θ) where Σ is a finite set of actions and θ : Σ → 2^{𝒫} assigns a set of processes to each a ∈ Σ.

State spaces With each process p, we associate a finite set of states denoted V_{p}. Each state in V_{p} is called a local state. For P ⊆ 𝒫, we use V_{P} to denote the product ∏_{p∈P} V_{p}. An element v⃗ of V_{P} is called a P -state. A 𝒫-state is also called a global state. Given v⃗ ∈ V_{P}, and P′ ⊆ P, we use v_{P′} to denote the projection of v⃗ onto V_{P′}. Also, v⃗\overline{P′} abbreviates v_{P \P′}. For a singleton p ∈ P, we write v⃗_{p} rather than v⃗_{{p}}. For a ∈ Σ, we write V_{a} to mean V_{θ(a)} and V\overline{a} to mean V\overline{θ(a)}. Similarly, if v⃗ ∈ V_{P}, we write v⃗_{a} to denote v⃗_{θ(a)} and v⃗\overline{a} to denote v⃗\overline{θ(a)}.

Asynchronous automaton An asynchronous automaton 𝔄 over (Σ, θ) is of the form

({V_{p}}_{p∈𝒫} , {→_{a}}_{a∈Σ}, 𝒱_{0}, 𝒱_{F}),

where →_{a} ⊆ V_{a} × V_{a} is the local transition relation for a, and 𝒱_{0}, 𝒱_{F} ⊆ V_{𝒫} are sets of initial and final global states. Intuitively, each →_{a} specifies how the process θ(a) that meet on a may decide on a joint move. Other processes do not change their state. Thus we define the global transition relation ⇒ ⊆ V_{𝒫} × Σ × V_{𝒫} by v⃗ ⟹^{a} v′ if v⃗_{a} →_{a} v′_{a} and

v⃗\overline{a} = v′ ; \overline{a}.

𝔄 is called deterministic if the transition relation of 𝔄 is a function from V_{𝒫} × Σ to V_{𝒫} and if the set of initial states 𝒱_{0} is a singleton.

Runs Let u ∈ Σ^{∗} be of length of m. It is convenient to think of u as a function u : [1..m] → Σ, where for natural numbers i < j, [i..j] abbreviates the set {i, i+1, …, j}.

A (global) run of 𝔄 on u is a function ρ : [0..m] → V_{𝒫} such that ρ(0) ∈ 𝒱_{0} and for

i ∈ [1..m], ρ(i − 1) ⟹^{u(i)} ρ(i).

The word u is accepted by 𝔄 if there is a run ρ of 𝔄 on u such that ρ(m) ∈ 𝒱_{F}. L(𝔄), the language accepted by 𝔄, is the set of words u accepted by 𝔄.

The problem Given a non-deterministic asynchronous automaton 𝔄 over (Σ, θ), we shall construct a deterministic asynchronous automaton 𝔅 over (Σ, θ), such that L(𝔄) = L(𝔅).

2 Local and global views

Events Given u : [1..m] → Σ, we associate a set of events 𝒳_{u}. Each event x is of the form (i, u(i)), where i ∈ [1..m]. In addition, we define an initial event denoted 0. The initial event marks the beginning when all processes synchronize and agree on an initial global state. Usually, we will write 𝒳 for 𝒳_{u}. We write p ∈ x to denote that p ∈ θ(u(i)) when x = (i, u(i)); for x = 0, we define p ∈ x to hold for all p ∈ 𝒫. If p ∈ x, then we say that x is a p-event.

If x = (i, a) is an event, then we may use x instead of a in abbreviations such as V_{x}, which stands for V_{a}, i.e., V_{θ(a)}.

Example: Consider the word u = abcd over the alphabet (Σ, θ) for 𝒫 = {p, q, r, s}, where Σ = {a, b, c, d} and θ(a) = {p, q}, θ(b) = {q, r, s}, θ(c) = {r, s}, and θ(d) = {p, q}. The set 𝒳_{u} of events is then

{x_{0}, x_{1}, x_{2}, x_{3}, x_{4}} = {0, (1, a), (2, b), (3, c), (4, d)}

.

Ordering relations on 𝒳 A word u imposes a total order on events: define x < y if x ≠ y and either x = 0 or x = (i, u(i)), y = (j, u(j)), and i < j. We write x ≤ y if x = y or x < y. Moreover, each process p orders the events in which it participates: define ◁_{p} to be the strict ordering

x ◁_{p} y if x < y, p ∈ x ∩ y and for all x < z < y, p ∉ z.

The set of all p-events in 𝒳 is totally ordered by ◁_{p}^{∗}, the reflexive, transitive closure of ◁_{p}.

Define x ⊏ y if for some p, x ◁_{p} y and x ⊑ y if x = y or x ⊏ y. The causality relation ⊑^{∗} is the transitive closure of ⊑. If x ⊑^{∗} y then we say that x is below y. Note that 0 is below any event. The set of events below x is denoted x↓. These represent the only synchronizations in 𝒳 that may have affected the state of the processes in x when x occurs. The neighbourhood of x, nbd(x), consists of x together with all its “⊏-predecessors”—i.e., nbd(x) = {x} ∪ {y | y ⊏ x}.

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; x_{4}; p; q; r; s; b; c; a; d; x_{3}; x_{2}; x_{1}; x_{0}]

Figure 1: An example

Example: Continuing our example, in Figure 1 an arrow has been drawn between each pair of events related by ⊏; the vertical dashed lines further partition these arrows into ◁_{p}, ◁_{q}, ◁_{r} and ◁_{s}. For example, x_{0} ◁_{p} x_{1} holds, but x_{0} ◁_{r} x_{1} does not hold. x_{4}↓, the x_{4}-cone, is the set {x_{0}, x_{1}, x_{2}, x_{4}} and x_{3}↓, the x_{3}-cone, is {x_{0}, x_{1}, x_{2}, x_{3}}. Thus x_{3}↓ ∪ x_{4}↓= 𝒳. nbd(x_{4}), the neighbourhood of x_{4}, is {x_{1}, x_{2}, x_{4}}.

Ideals A set of events I ⊆ 𝒳 is called an ideal if I is closed with respect to ⊑^{∗}—i.e., x ∈ I and y ⊑^{∗} x implies y ∈ I as well. Clearly the entire set 𝒳 is an ideal, as is x↓ for any x ∈ 𝒳.

P -views Let I be an ideal. The ⊑^{∗}-maximum p-event in I is denoted max_{p}(I). The p-view of I is the set I|_{p} = max_{p}(I)↓. So, I|_{p} is the set of all events in I which p can “see”. For P ⊆ 𝒫, the P -view of I, denoted I|_{P}, is ⋃_{p∈P} I|_{p}. Notice that I|_{P} is always an ideal. In particular, we have I|_{𝒫} = I. Also notice that if y ∈ I|_{P} for some P ⊆ 𝒫, then nbd(y) ⊆ I|_{P} as well.

Example: In the example of Figure 1, max_{q}(𝒳) = x_{4}. So 𝒳|_{q} = x_{4}↓= {x_{4}, x_{2}, x_{1}, x_{0}}. On the other hand, max_{s}(𝒳) = x_{3} and 𝒳|_{s} = x_{3}↓= {x_{3}, x_{2}, x_{1}, x_{0}}.

3 Local runs and histories

Local runs Let I be an ideal. A local run on I is a function r that assigns to each y ∈ I a y-state—i.e., a state in V_{y}—such that r(0) ∈ 𝒱_{0} and for all y ≠ 0, r is consistent with →_{y} in the neighbourhood nbd(y). In other words, for y ≠ 0 we have v⃗ →_{y} r(y), where v⃗ the y-state such that for all q ∈ y, v⃗_{q} = r(z)_{q}, where z ◁_{q} y. Let ℛ(I) denote the set of all local runs on I.

So, a local run on 𝒳 is an assignment of a y-state to each y ∈ 𝒳 such that all neighbourhoods in 𝒳 are consistently labelled.

Proposition 1 Given u : [1..m] → Σ, there is a 1-1 correspondence between local runs on 𝒳_{u} and global runs on u.

Proof For i ∈ [1..m] let w_{i} denote the prefix of u up to i. Also, for i ∈ [1..m] let x_{i} denote the event (i, u(i)) in 𝒳_{u}.

Given a local run r on 𝒳_{u}, we define a global run ρ : [0..m] → V_{𝒫} on u by ρ(0) = r(0) and for i ∈ [1..m], ρ(i)_{p} = r(max_{p}(𝒳_{w_{i}}))_{p} for all p ∈ 𝒫.

Given a global run ρ : [0..m] → V_{𝒫} on u , we define a local run r on 𝒳_{u} by r(0) = ρ(0) and for i ∈ [1..m], r(x_{i}) = ρ(i)_{θ(u(i))}. □

Histories Let I be an ideal. A history on I is a partial function h such that dom(h) ⊆ I and h(y) ∈ V_{y} for each y ∈ dom(h). A history h is reachable if there is some local run r on I such that h(y) = r(y) for all y ∈ dom(h). Let ℋ(I) denote the set of all histories on I. Clearly, ℛ(I) ⊆ ℋ(I).

Choices Let I be an ideal. Given a collection {H_{p}}_{p∈P} of sets of histories on the p-views I|_{p}, a P -choice {h_{p}}_{p∈P} of {H_{p}}_{p∈P} assigns to each p ∈ P, a history h_{p} from H_{p}. The choice is consistent if for each p, q ∈ P, for every y ∈ dom(h_{p}) ∩ dom(h_{q}), h_{p}(y) = h_{q}(y).

Let {H_{p}}_{p∈P} be a collection of sets histories for P ⊆ 𝒫. We define the product ⨂_{p∈P} H_{p} as follows.

⨂_{p∈P} H_{p} = \{h ∈ ℋ(I|_{P}) | \begin{matrix}There exists a consistent P -choice \{h_{p}\}_{p∈P} of \\ \{H_{p}\}_{p∈P} such that dom(h) = ⋃_{p} dom(h_{p}) and \\ ∀p ∈ P. ∀y ∈ dom(h_{p}). h(y) = h_{p}(y)\} \end{matrix}

So each element in ⨂_{p∈P} H_{p} is a history on I|_{P} pieced together from a choice of mutually consistent histories on I|_{p} from the sets H_{p}, for p ∈ P.

In particular, for P ⊆ 𝒫 we may form the product ⨂_{p∈P} ℛ(I|_{p}), which generates the set ℛ(I|_{P}) of local runs on I|_{P}:

Lemma 2 Let I be an ideal and P ⊆ 𝒫. ℛ(I|_{P}) = ⨂_{p∈P} ℛ(I|_{p})

Proof Let r ∈ ℛ(I|_{P}). Then for each p ∈ P, clearly r restricted to I|_{p} is a local run r_{p} on I|_{p}. So, using the consistent P -choice {r_{p}}_{p∈P} of {ℛ(I|_{p})}_{p∈P} we get r ∈ ⨂_{p∈P} ℛ(I|_{p}).

On the other hand, let r ∈ ⨂_{p∈P} ℛ(I|_{p}) where the consistent P -choice is {r_{p}}_{p∈P}. Clearly dom(r) = I|_{P}. We just have to check that nbd(y) is labelled consistently by r for each y ∈ I|_{P}. But, any y ∈ I|_{P} must also belong to I|_{p} for some p ∈ P. We know that y ∈ I|_{p} implies nbd(y) ⊆ I|_{p}. Since r_{p} is a local run on I|_{p}, r_{p} must have assigned consistent values to nbd(y). But r agrees with r_{p} on all events in I|_{p}, so r must assign the same values to nbd(y) and we are done. □

An infinite-state deterministic automaton

The preceding lemma tells us that we can reconstruct ℛ(I|_{𝒫} ) = ℛ(I) by taking the product ⨂_{p∈𝒫} ℛ(I|_{p})—i.e., we can recover all the local runs on 𝒳 by taking the product of local runs on 𝒳|_{p}. We already know that local runs on 𝒳 correspond precisely to the global runs on u.

This immediately gives us an infinite-state deterministic asynchronous automaton 𝔄′ = ({V′_{p}}_{p∈𝒫} , {→′_{a}}_{a∈Σ}, 𝒱′_{0}, 𝒱′_{F}) which accepts L(𝔄). For p ∈ 𝒫, V′_{p} = {ℛ(𝒳_{u}|_{p}) | u ∈ Σ^{∗}}. In other words, each local state of p consists of the set of local runs on 𝒳_{u}|_{p} for each word u.

Initially, each process starts off in the state {⟨0 ↦ v⃗⟩ | v⃗ ∈ 𝒱_{0}}. The global initial state 𝒱′_{0} is the cross product of these initial states.

The transition relations →′_{a} are defined in the natural way. Suppose w = ua. Let x_{a} be the new event associated with a—i.e., {x_{a}} = 𝒳_{w} \ 𝒳_{u}. Clearly, for p ∉ θ(a), 𝒳_{w}|_{p} = 𝒳_{u}|_{p} and, as desired, the local state of p does not change—ℛ(𝒳_{w}|_{p}) = ℛ(𝒳_{u}|_{p}). For p ∈ θ(a), it is easy to check that 𝒳_{w}|_{p} = 𝒳_{u}|_{θ(a)} ∪ {x_{a}}. So, any run r_{p} ∈ ℛ(𝒳_{w}|_{p}) consists of a local run on 𝒳_{u}|_{θ(a)} together with an assignment of a θ(a)-state to x_{a} which is consistent with →_{a} in the neighbourhood nbd(x_{a}). But, by Lemma 2, ℛ(𝒳_{u}|_{θ(a)}) is precisely the product ⨂_{p∈θ(a)} ℛ(𝒳_{u}|_{p}). So, when the processes in θ(a) synchronize, they can pool their information and compute for each p ∈ θ(a) the new state ℛ(𝒳_{w}|_{p}). In fact, for all p ∈ θ(a), the new local state ℛ(𝒳_{w}|_{p}) will be identical.

To decide whether to accept u, we have to check if 𝔄 could have been in an accepting global state after u. By Lemma 2 and Proposition 1, we can associate with each local run r ∈ ⨂_{p∈𝒫} ℛ(𝒳_{u}|_{p}) a global run ρ on u. The global state v⃗ of 𝔄 after r is obtained by setting v⃗_{p} = r(max_{p}(𝒳_{u}))_{p} for each p ∈ 𝒫. Since ⨂_{p∈P} ℛ(𝒳_{u}|_{p}) generates exactly the set of local runs on 𝒳_{u}, we can compute all reachable global states after u in this manner. So, a global state in our new automaton is accepting if one of the global states it generates is an accepting state for 𝔄.

In the following, we formulate a finite-state version of the automaton above. We do not store the entire set ℛ(𝒳_{u}|_{p}) in each p. Instead, at any ideal I, each p will keep track of the set of reachable histories on a special bounded subset of I|_{p}. This bounded subset will be such that the product of reachable histories across this subset will also be reachable. In this manner, we ensure that the processes retain enough global information about runs to compute exactly the reachable global states after I.

4 Finite histories and frontiers

Frontiers Let I be an ideal and p, q, s ∈ 𝒫. We say that event y is an s-sentry for p with respect to q if y ◁_{s} z for some z ∈ I|_{q} \ (I|_{p} ∩ I|_{q}). Thus it is an event known to p and q, but whose s-successor is known only to q. Notice that for some s ∈ 𝒫, there may be no s-sentry for p with respect to q.

Define frontier_{pq}(I) to be the set of all s-sentries which exist for p with respect to q. Notice that this definition is asymmetric—frontier_{pq}(I) ≠ frontier_{qp}(I).

Example: In the example of Figure 1, 𝒳|_{p} ∩ 𝒳|_{s} = {x_{0}, x_{1}, x_{2}}. frontier_{ps}(𝒳) = {x_{2}}, whereas frontier_{sp}(𝒳) = {x_{1}, x_{2}}. Notice that x_{2} belongs to both frontiers—it is an r-sentry and an s-sentry in frontier_{ps}(𝒳) and a q-sentry in frontier_{sp}(𝒳).

As our example shows, an event y ∈ frontier_{pq}(I) could simultaneously be an s-sentry for several different s. The following observation guarantees that frontier_{pq}(I) is always a bounded set.

Lemma 3 Let I be an ideal and p, q ∈ 𝒫, For each s ∈ 𝒫 there is at most one s-sentry y ∈ frontier_{pq}(I).

Proof Suppose not. Then we have y, y′ ∈ frontier_{pq}(I) and z, z′ such that y ◁_{s} z and y′ ◁_{s} z′. We know that all events involving s are totally ordered by ◁_{s}. So either y ◁_{s}^{∗} y′ or y′ ◁_{s}^{∗} y. Without loss of generality assume that y ◁_{s}^{∗} y′. Then we must have y ◁_{s} z ◁_{s}^{∗} y′ ◁_{s} z′. Since y′ ∈ I|_{p} ∩ I|_{q} and z ⊑^{∗} y′, z ∈ I|_{p} ∩ I|_{q} as well. But this contradicts the assumption that z ∈ I|_{q} \ (I|_{p} ∩ I|_{q}). □

For P ⊆ 𝒫 and p ∈ P, the P -frontier of p at I is the set

⋃_{q∈P \{p}} frontier_{pq}(I) ∪ frontier_{qp}(I).

Lemma 4 Let I be an ideal and {h_{p}}_{p∈P} be a consistent P -choice of {ℋ(I|_{p})}_{p∈P} such that for each p ∈ P:

• h_{p} is reachable; and

• the P -frontier of p is included in dom(h_{p}).

Then ⨂_{p∈P} h_{p} is a reachable history in ℋ(I|_{P}).

Proof Let us order the processes in P as p_{1}, p_{2}, …, p_{k}. For i ∈ [1..k], let P_{i} = ⋃_{j∈[1..i]} p_{j}. By assumption, for each p_{i}, h_{p_{i}} is a reachable history. So, we have a local run r_{p_{i}} on I|_{p_{i}} which agrees with h_{p_{i}} on dom(h_{p_{i}}). To show that h = ⨂_{p∈P} h_{p} is reachable, we must construct a local run r on I|_{P} which agrees with h on dom(h) = ⋃_{p∈P} dom(h_{p}).

Define r as follows:

• For all y ∈ I|_{p_{1}}, r(y) = r_{p_{1}}(y).

• For i ∈ [2..k], for all y ∈ I|_{p_{i}} \ I|_{P_{i−1}}, r(y) = r_{p_{i}}(y).

So, we “sweep across” I|_{P} starting from I|_{p_{1}} and ending at I|_{p_{k}}, assigning states according to r_{p_{1}}, r_{p_{2}}, …, r_{p_{k}} in k “stages” as we go along. Clearly dom(r) = I|_{P} and r agrees with h on dom(h). We have to show that r is a local run; i.e., we have to show that r is consistent with →_{y} across nbd(y) for each y ∈ I|_{P}.

Let y ∈ I|_{P}. We know that r(y) was assigned at some stage i ∈ [1..k]. Clearly, y ∈ I|_{p_{i}} and so nbd(y) ⊆ I|_{p_{i}} as well. If nbd(y) ⊆ I|_{p_{i}} \ I|_{P_{i−1}}, then all the events in nbd(y) are assigned r values at stage i according to r_{p_{i}}. Since r_{p_{i}} is a local run on I, these values must be consistent with →_{y}.

The crucial case is when some z ∈ nbd(y) lies in I|_{P_{i−1}} and so has already been assigned a value according to r_{p_{j}} for some j ∈ [1..i−1]. But then z ∈ I|_{P_{i−1}} ∩ I|_{p_{i}} which is the same as ⋃_{j∈[1..i−1]}(I|_{p_{j}} ∩ I|_{p_{i}}). In other words, for some p_{j}, j ∈ [1..i−1], z belongs to frontier_{p_{j}p_{i}}(I). So z ∈ dom(h_{p_{j}}) ∩ dom(h_{p_{i}}), by assumption. Therefore, the value r(z) must agree with h_{p_{j}}(z) = h_{p_{i}}(z) and hence must agree with r_{p_{i}}(z) as well. In other words, even though z ∈ nbd(y) has already been assigned a value before stage i, the value agrees with r_{p_{i}}. So, effectively, nbd(y) is assigned values as given by r_{p_{i}} and these must be consistent with →_{y} since r_{p_{i}} is a local run on I. □

This is a finite version of Lemma 2 above. Suppose that at the end of a word u, each process p maintains all reachable histories on a finite (bounded) set of events spanning the 𝒫-frontier of p in 𝒳_{u} together with the maximum p-event max_{p}(𝒳_{u}). By the previous lemma, the product of these histories will generate all the reachable global states of 𝔄 after u. Since the 𝒫-frontier of p in any ideal is a finite set, the set of all reachable histories that p has to keep track of is also finite. So, using a bounded amount of information in each process, we can reconstruct all possible global states of 𝔄 after u.

The problem now is with maintaining frontier information locally—i.e., how can a process p compute and locally update its frontier? This is done using slightly larger, but still bounded, sets of events called primary and secondary information, which between them subsume the frontier. It turns out that these sets can be updated locally with each synchronization between processes. These then will be the domains of the histories maintained by each process.

5 Primary and secondary information

Primary information Let I be an ideal and p, q ∈ 𝒫. Then latest_{p→q}(I) denotes the maximum q-event in I|_{p}. So, latest_{p→q}(I) is the latest q-event in I that p knows about.

The primary information of p after I, primary_{p}(I), is the set {latest_{p→q}(I)}_{q∈𝒫} . As usual, for P ⊆ 𝒫, primary_{P} (I) = ⋃_{p∈P} primary_{p}(I).

Remark: Since q ∈ 0 ∈ I|_{p} for all q ∈ 𝒫, the set {y ∈ I|_{p} | q ∈ y} is always nonempty. Since all q-events are linearly ordered by ◁_{q}, the maximum q-event in I|_{p} is well-defined. Notice that latest_{p→p}(I) = max_{p}(I).

Secondary information The secondary information of p after I, secondary_{p}(I), is the set ⋃_{q∈𝒫} primary_{q}(latest_{p→q}(I)↓). In other words, this is the latest information that p has in I about the primary information of q, for each q ∈ 𝒫. Once again, for P ⊆ 𝒫, secondary_{P} (I) = ⋃_{p∈P} secondary_{p}(I).

Each event in secondary_{p}(I) is of the form latest_{q→s}(latest_{p→q}(I)↓) for some q, s ∈ 𝒫. This is the latest s-event which q knows about upto the event latest_{p→q}(I). We abbreviate latest_{q→s}(latest_{p→q}(I)↓) by latest_{p→q→s}(I). Notice that each primary event latest_{p→q}(I) is also a secondary event latest_{p→p→q}(I). In other words, primary_{p}(I) ⊆ secondary_{p}(I).

Example: In Figure 1, latest_{s→p}(𝒳) = x_{1} whereas latest_{p→s}(𝒳) = x_{2}. Also, latest_{s→p→r}(𝒳) = x_{0} while latest_{p→s→r}(𝒳) = x_{2}.

Lemma 5 Let I be an ideal, p, q ∈ 𝒫 and y ∈ frontier_{pq}(I) an s-sentry. Then y = latest_{p→s}(I). Also, for some s′ ∈ 𝒫, y = latest_{q→s′→s}(I). So, y ∈ primary_{p}(I) ∩ secondary_{q}(I).

Proof Since y is an s-sentry, for some z ∈ I|_{q} \ I|_{p}, y ◁_{s} z. Suppose that latest_{p→s}(I) = y′ ≠ y. Since all s-events are linearly ordered by ◁_{s}, we must have y ◁_{s}^{∗} y′. However, y ◁_{s} z as well, so we have y ◁_{s} z ◁_{s}^{∗} y′. This means that z ∈ I|_{p}, which is a contradiction.

Next, we must show that y = latest_{q→s′→s}(I) for some s′ ∈ 𝒫. We know that there is a path y ⊏ z_{1} ⊏ … ⊏ max_{p}(I), since y ∈ I|_{p}. This path starts inside I|_{p} ∩ I|_{q}.

If this path never leaves I|_{p} ∩ I|_{q} then max_{p}(I) ∈ I|_{q}. Since max_{p}(I) is the maximum p-event in I, it must be the maximum p-event in I|_{q}. So, y = latest_{q→p→s}(I) and we are done.

If this path does leave I|_{p} ∩ I|_{q}, we can find an event y′ ∈ frontier_{qp}(I) along the path such that y′ is an s′-sentry for some s′ ∈ 𝒫—in other words, for some z′, y ⊑^{∗} y′ ◁_{s′} z′ ⊑^{∗} max_{p}(I). We know by our earlier argument that y′ = latest_{q→s′}(I). It must be the case that y = latest_{s′→s}(y′↓). For, if latest_{s′→s}(y′↓) = y′′ ≠ y, then y ◁_{s}^{∗} y′′ ⊑^{∗} y′ ⊑^{∗} max_{p}(I). This implies that y ◁_{s}^{∗} y′′ and y′′ ∈ I|_{p}, which contradicts the fact that y = latest_{p→s}(I). So, y = latest_{s′→s}(y′↓) = latest_{q→s′→s}(I) and we are done. □

So, for every p ∈ 𝒫 and u ∈ Σ^{∗}, each process p maintains all reachable histories over the finite set secondary_{p}(𝒳_{u}). (Recall that primary_{p}(𝒳_{u}) ⊆ secondary_{p}(𝒳_{u}).) By the preceding lemma, this set includes all events in the 𝒫-frontier of 𝒳_{u} as well as the maximal event max_{p}(𝒳_{u}) = latest_{p→p→p}(𝒳_{u}).

We now need to show that these sets may be updated locally—i.e., if w = ua, then secondary_{p}(w) may be computed from secondary_{p}(u) for each process p ∈ θ(a) using only the information available with the processes in θ(a). This involves running the “gossip automaton” [MS] in the background. In order to make this presentation self-contained, we describe the procedure of [MS] for comparing and updating primary and secondary information.

Comparing primary information

Lemma 6 Let I be an ideal and p, q, s ∈ 𝒫. Let y_{p} = latest_{p→s}(I) and y_{q} = latest_{q→s}(I). Then y_{p} ⊑^{∗} y_{q} iff y_{p} ∈ secondary_{q}(I).

Proof

(⇐) Suppose y_{p} ∈ secondary_{q}(I). Then, y_{p} ∈ I|_{q} and so y_{p} ⊑^{∗} y_{q} ∈ I|_{q} by the definition of latest_{q→s}(I).

(⇒) If y_{p} = y_{q}, y_{p} ∈ primary_{q}(I) ⊆ secondary_{q}(I) and there is nothing to prove. If y_{p} ≠ y_{q}, then, y_{p} ◁_{s}^{∗} y_{q} and so y_{p} ∈ I|_{p} ∩ I|_{q}. Let y′ be the s-successor of y. We know that y′ ∈ I|_{q} \ I|_{p}, so y_{p} is an s-sentry in frontier_{pq}(I). But then, by our previous lemma, y_{p} ∈ primary_{p}(I) ∩ secondary_{q}(I) and we are done. □

Suppose p and q synchronize at an action a after u. At this point they “share” their primary and secondary information. If q can find the event latest_{p→s}(𝒳_{u}) in its set of secondary events secondary_{q}(𝒳_{u}), q knows that its latest s-event latest_{q→s}(𝒳_{u}) is at least as recent as latest_{p→s}(𝒳_{u}). So, after the synchronization, latest_{q→s}(𝒳_{ua}) is the same as latest_{q→s}(𝒳_{u}), whereas p inherits this information from q—i.e., latest_{p→s}(𝒳_{ua}) = latest_{q→s}(𝒳_{u}). In this way, for each s ∈ 𝒫, p and q can locally update their primary information about s in 𝒳_{ua}. Clearly latest_{p→q}(𝒳_{ua}) = latest_{q→p}(𝒳_{ua}) = x_{a}, where x_{a} is the new event—i.e., 𝒳_{ua} \ 𝒳_{u} = {x_{a}}.

This procedure generalizes to any arbitrary set P ⊆ 𝒫 which synchronize after u. The processes in P share their primary and secondary information and compare this information pairwise. Using Lemma 6, for each q ∈ 𝒫 \ P they decide who has the “latest information” about q. Each process then comes away with the best primary information from P. Notice, that all processes in P will always have the same primary information after they synchronize.

Once we have compared primary information, updating secondary information is automatic. Clearly, if latest_{q→s}(I) is better than latest_{p→s}(I), then every secondary event latest_{q→s→s′}(I) must also be better than latest_{p→s→s′}(I). So, secondary information can be locally updated too. In other words, to consistently update primary and secondary information, it suffices to to correctly compare primary information, which is achieved by Lemma 6.

From the preceding argument, it is clear that each new event belongs to the primary (and hence secondary) information of the processes which synchronize at that event. Further, if an event disappears from the secondary information of all the processes, it will never reappear as secondary information at some later stage. This is captured formally in the following proposition.

Proposition 7 Let u, w ∈ Σ^{∗} such that w = ua for some a ∈ Σ. Let x_{a} denote the new event in w—i.e., 𝒳_{w} \ 𝒳_{u} = {x_{a}}. Then:

• x_{a} ∈ secondary_{𝒫} (𝒳_{w}).

• secondary_{𝒫} (𝒳_{w}) ⊆ {x_{a}} ∪ secondary_{𝒫} (𝒳_{u}).

6 Locally updating primary/secondary information

To make Lemma 6 effective, we must make the assertions “locally checkable”—e.g., if y_{p} = latest_{p→s}(I), processes p and q must be able to decide if y_{p} ∈ secondary_{q}(I). This is achieved by labelling each action in u in such a way that primary and secondary information can be maintained as sets of labelled actions.

We may naïvely assume that events in 𝒳_{u} are locally assigned distinct labels—in effect, at each action a, the processes in θ(a) assign a time-stamp to the new occurrence of a. In this manner, the processes in 𝒫 can easily assign consistent local time-stamps for each action which will let them compute the relations between events which we are interested in.

The problem with this approach is that we will need an unbounded set of time-stamps, since u could get arbitrarily large. Instead we would like a scheme which uses only a finite set of labels to distinguish events. This would mean that several different occurrences of the same action will eventually end up with the same label. We have to ensure that this does not lead to any confusion when we try to update primary and secondary information.

However, from Lemma 6, we know that to compare primary information, we only need to look at the events in the primary and secondary sets of each process. So, it is sufficient if the labels assigned to these sets are consistent across the system—i.e., if the same label appears in primary or secondary information of different processes, the corresponding event is actually the same.

Suppose we have such a labelling on u and we want to extend this to a labelling on w = ua—i.e., we need to assign a label to the new a-event. By Proposition 7, it suffices to use a label which is distinct from the labels of all the a-events currently in the secondary information of 𝒳_{u}.

Unfortunately, the processes in θ(a) cannot directly see all the a-events which belong to the secondary information of the entire system. An a-event y may be part of the secondary information of processes outside θ(a)—i.e., y ∈ secondary\overline{a}(𝒳_{u}) \ secondary_{a}(𝒳_{u}). To enable the processes in θ(a) to know about all a events in secondary_{𝒫} (𝒳_{u}), we need to maintain tertiary information.

Tertiary information The tertiary information of p after I, tertiary_{p}(I), is the set ⋃_{q∈𝒫} secondary_{q}(latest_{p→q}(I) ↓). In other words, this is the latest information that p has in I about the secondary information of q, for all q ∈ 𝒫. As before, for P ⊆ 𝒫, tertiary_{P} (I) = ⋃_{p∈P} tertiary_{p}(I).

Each event in tertiary_{p}(I) is of the form latest_{q→s→s′}(latest_{p→q}(I)↓) for some q, s, s′ ∈ 𝒫. We abbreviate latest_{q→s→s′}(latest_{p→q}(I)↓) by latest_{p→q→s→s′}(I). Just as primary_{p}(I) ⊆ secondary_{p}(I), clearly secondary_{p}(I) ⊆ tertiary_{p}(I) since each secondary event latest_{p→q→s}(I) is also a tertiary event latest_{p→p→q→s}(I).

Lemma 8 Let I be an ideal and p ∈ 𝒫. If y ∈ secondary_{p}(I) then for every q ∈ y, y ∈ tertiary_{q}(I).

Proof Let y ∈ secondary_{p}(I) and q ∈ y. We know that y ∈ I|_{p} ∩ I|_{q} and there is a path y ⊏ z_{1} ⊏ … ⊏ max_{p}(I) leading from y to max_{p}(I).

Suppose this path never leaves I|_{p} ∩ I|_{q}. Then max_{p}(I) ∈ I|_{q} and so max_{p}(I) = latest_{q→p}(I). This means that y ∈ secondary_{p}(latest_{q→p}(I)↓) ⊆ tertiary_{q}(I) and we are done.

Otherwise, the path from y to max_{p}(I) does leave I|_{p} ∩ I|_{q} at some stage. Concretely, let y = latest_{p→p′→p′′}(I) for some p′, p′′ ∈ 𝒫. So the path from y to max_{p}(I) passes through y′ = latest_{p→p′}(I).

If y′ ∉ I|_{p} ∩ I|_{q} then for some z, z′ ∈ 𝒳 and some s ∈ 𝒫 we have z ∈ I|_{p} ∩ I|_{q}, z′ ∈ I|_{p} \ I|_{q} and y ⊑^{∗} z ◁_{s} z′ ⊑^{∗} y′. This means that z ∈ frontier_{qp}(I) is an s-sentry and by our earlier argument we know that z = latest_{q→s}(I). So y = latest_{q→s→p′′}(I) = latest_{q→q→s→p′′}(I) ∈ tertiary_{q}(I).

On the other hand, if y′ ∈ I|_{p} ∩ I|_{q} we can find an s-sentry z ∈ frontier_{qp}(I) on the path from y′ to max_{p}(I), for some s ∈ 𝒫. We once again get z = latest_{q→s}(I) and so y = latest_{q→s→p′→p′′}(I) ∈ tertiary_{q}(I).

□

The “gossip” automaton Using our analysis of primary, secondary and tertiary information of processes, we can now design a deterministic asynchronous automaton to keep track of the “latest gossip”—i.e., consistently to update primary, secondary and tertiary information whenever a set of processes synchronize.

Each process maintains sets of primary, secondary and tertiary information. Each event in these sets is represented by a pair ⟨P, ℓ⟩, where P is the subset of processes that synchronized at the event and ℓ ∈ ℒ, a finite set of labels.

By Lemma 8, each p-event that appears in some primary or secondary set in the system also appears in the tertiary information of p. When a new event x occurs after u, the processes participating in x assign a label to this event which does not appear in tertiary_{x}(𝒳_{u}). Proposition 7 guarantees that the new event is assigned a label which is distinct from those assigned to secondary_{𝒫} (𝒳_{u}). Since each process keeps track of N^{3} tertiary events, there need be only O(N^{3}) labels in ℒ.

The processes participating in x now compare their primary information about each process s ∉ x by checking labels of events across their primary and secondary sets. Each process then updates its primary, secondary and tertiary sets according to the new information it receives. (Notice that tertiary information, like secondary information, can be locally updated once the processes have decided who has the best primary information.)

To implement this algorithm as a deterministic asynchronous automaton, we just observe that each local state of p will consist of its primary, secondary and tertiary information for p, stored as an collection of indexed labels. The initial state is the global state where for all processes p, these sets all contain only the initial event 0. The local transition relations →_{a} modify the local states for processes in θ(a) as described above. This automaton does not have any final states—it simply runs in the “background”.

7 The determinization algorithm

We are now ready to present our deterministic asynchronous automaton

𝔅 = ({V_{p}^{𝔅}}_{p∈𝒫} , {→_{a}^{𝔅}}_{a∈Σ}, 𝒱_{0}^{𝔅}, 𝒱_{F}^{𝔅})

corresponding to our original non-deterministic asynchronous automaton 𝔄 such that L(𝔄) = L(𝔅).

Let us assume we have a sufficiently large but finite set of labels ℒ. Formally, a state in V_{p}^{𝔅} consists of the following information:

• A labelling λ_{p} : (𝒫 × 𝒫 × 𝒫) → (𝒫 × ℒ), which is partially injective, in that for each q, q′, r, r′ ∈ 𝒫, λ_{p}(q, q, r) = λ_{p}(q′, q′, r′) implies q = q′ and r = r′.

• A set of histories ℛℋ_{p} where each h ∈ ℛℋ_{p} is a function from 𝒫 × 𝒫 to P -states, P ⊆ 𝒫.

Intuitively, after reading a word u, the automaton represents the tertiary event latest_{p→q→r→s}(𝒳_{u}) as λ_{p}(q, r, s).

In this representation, several copies exist of each primary and secondary event. For instance, the primary event latest_{p→q}(𝒳_{u}) corresponds to λ_{p}(q, q, q), λ_{p}(p, q, q) and λ_{p}(p, p, q). We choose canonical representatives for each primary and secondary event. So, we shall regard λ_{p}(q, q, q) as the label of the primary event latest_{p→q}(𝒳_{u}) and λ_{p}(q, q, r) as the label of the secondary event latest_{q→r}(𝒳_{u}) as λ_{p}(q, q, r). The partially injectivity of λ_{p} ensures that all labels assigned to primary and secondary events are distinct.

The set ℛℋ_{p} is supposed to contain all reachable histories over the secondary events secondary_{p}(𝒳_{u}). Since these events are injectively labelled by λ_{p}, we can also view ℛℋ_{p} as a function from 𝒫 × ℒ to P -states.

Initially, each p ∈ 𝒫 stores the following:

• ∀⟨q, r, s⟩ ∈ 𝒫^{3}. λ_{p}(q, r, s) = ⟨𝒫, 0⟩, where 0 ∈ ℒ is some arbitrary but fixed label.

• For each v⃗ ∈ 𝒱_{0}, the set of initial states of 𝔄, we have a history h ∈ ℛℋ_{p} such that h(q, r) = v⃗ for all ⟨q, r⟩ ∈ 𝒫^{2}.

The initial state 𝒱_{0}^{𝔅} of 𝔅 is the product of the initial states of all p ∈ 𝒫. The transition rule →_{a}^{𝔅} is described in the following. Suppose 𝔅 reads a when the global state of 𝔅 is {⟨λ_{p}, ℛℋ_{p}⟩}_{p∈𝒫} . Then we have the following procedure for updating the local states of processes in θ(a).

• For each p ∈ θ(a), we construct a new labelling function λ′_{p} : 𝒫^{3} → 𝒫 × ℒ. Fix a new label ℓ ∈ ℒ such that ⟨θ(a), ℓ⟩ is not in the range of λ_{p} for any p ∈ θ(a). For each p ∈ θ(a), assign λ′_{p}(q, r, s) = ⟨θ(a), ℓ⟩ for all q, r, s ∈ 𝒫 such that {q, r, s} ⊆ θ(a). The other values of λ′_{p} for each p ∈ θ(a) are computed as they would be by the gossip automaton. In other words, for all p ∈ θ(a), for all q, r, s ∈ 𝒫 such that {q, r, s} ⊈ θ(a), the new value λ′_{p}(q, r, s) is copied from the old value λ_{p′}(q, r, s) assigned by the process p′ ∈ θ(a) which had the best primary information λ_{p′}(q, q, q).

• Compute new histories ℛℋ′_{p} for each p ∈ θ(a) as follows. Consider h_{a} ∈ ⨂_{p∈θ(a)}{ℛℋ_{p}}. Let v⃗ be the global a-state corresponding to h_{a}—i.e., v⃗_{p} = h_{p}(p, p) for each p ∈ θ(a). Let 𝒱_{h_{a}} = {v′ | v⃗ →_{a} v′}. So, 𝒱_{h_{a}} is the set of all possible a-states v′ which can be used to extend h_{a} to cover the new event x_{a} so that nbd(x_{a}) is consistently labelled with respect to →_{a}. Now each element v′ ∈ 𝒱_{h_{a}} together with h_{a} generates a history h′_{p} in ℛℋ′_{p} as follows:

∀⟨q, r⟩ ∈ 𝒫^{2}. h′_{p}(q, r) = \{ \begin{matrix}v′ & if λ′_{p}(q, q, r) = ⟨θ(a), ℓ⟩ \\ h_{a}(λ′_{p}(q, q, r)) & otherwise \end{matrix}

So, the new a-event is assigned the a-tuple v′ while the other secondary events of p (after reading a) inherit their h′_{p} values from h_{a}. Repeat this procedure for each h_{a} ∈ ⨂_{p∈θ(a)}{ℛℋ_{p}} to generate the entire set ℛℋ′_{p} for each p ∈ θ(a).

Having described the transition functions →_{a}^{𝔅}, we now need to define the final states of 𝔅. Let σ⃗ be a global state of 𝔅, where σ⃗_{p} = ⟨λ_{p}, ℛℋ_{p}⟩ for each p ∈ 𝒫. Each h ∈ ⨂_{p∈𝒫} ℛℋ_{p} gives rise to a global state v⃗ of 𝔄 as follows: for each p ∈ 𝒫, v⃗_{p} = h(λ_{p}(p, p, p)). Let subset(σ⃗) denote the set of global states of 𝔄 generated from σ⃗ in this manner. Then we can define

𝒱_{F}^{𝔅} = {σ⃗ | subset(σ⃗) ∩ 𝒱_{F} ≠ ∅}.

Theorem 9 L(𝔄) = L(𝔅).

Proof For u ∈ Σ^{∗}, let σ⃗ be the global state of 𝔅 after reading u such that σ⃗_{p} = ⟨λ′_{p}, ℛℋ′_{p}⟩ for each p ∈ 𝒫. We claim the following:

Claim For each p ∈ 𝒫, λ′_{p} labels precisely the events in tertiary_{p}(𝒳_{u}) and ℛℋ′_{p} is precisely the set of all reachable histories on the set of events secondary_{p}(𝒳_{u}).

Assuming the claim, we know from Proposition 1 and Lemmas 2, 4 and 5 that the global states in subset(σ⃗) are precisely the global states that 𝔄 could be in after u. So, 𝔅 accepts u iff subset(σ⃗) ∩ 𝒱_{F} ≠ ∅ iff there is a run of 𝔄 on u leading to a final state iff 𝔄 accepts u and we are done.

Proof of Claim To prove the claim, we proceed by induction on |u|.

The base case is when u = ε, the empty word. The claim is trivially true at this state since all the tertiary events in 𝒳_{u} are the initial event 0 and each process maintains a set of histories which assign all possible initial states of 𝔄 to the initial event.

Suppose u = wa and, inductively, after reading w, the local state ⟨λ_{p}, ℛℋ_{p}⟩ for each p ∈ 𝒫 satisfies the Claim. We have to argue that the procedure for updating the local states of p ∈ θ(a) maintains the property asserted in the Claim.

Look at the definition of →_{a}^{𝔅}. Proposition 7 and Lemma 8 guarantee that the label ⟨θ(a), ℓ⟩ we assign to the new event does not clash with any labels already assigned to events in secondary_{𝒫} (𝒳_{w}). Lemma 6 then ensures that the computation of λ′_{p} from λ_{p} is correct—i.e., λ′_{p} labels precisely the events in tertiary_{p}(𝒳_{u}).

Now, assume ℛℋ_{p} contains all reachable histories over secondary_{p}(𝒳_{w}) for each p ∈ θ(a). We have to show that ℛℋ′_{p} contains all reachable histories over secondary_{p}(𝒳_{u}). For all p ∈ θ(a), 𝒳_{u}|_{p} = 𝒳_{w}|_{θ(a)} ∪ {x_{a}}, where x_{a} is the new a-event. So, any local run on 𝒳_{u}|_{p} consists of a local run on 𝒳_{w}|_{θ(a)} extended to cover x_{a} such that nbd(x_{a}) is consistently labelled.

We argue that the product ⨂_{p∈θ(a)} ℛℋ_{p} is precisely the projection of ℛ(𝒳_{w}|_{θ(a)}) onto secondary_{θ(a)}(𝒳_{w}). By Lemma 4, every history h ∈ ⨂_{p∈θ(a)} ℛℋ_{p} is a reachable history on 𝒳_{w}|_{θ(a)} and so is the projection of some local run on 𝒳_{w}|_{θ(a)} onto secondary_{θ(a)}(𝒳|_{w}).

Conversely, consider any local run r on 𝒳_{w}|_{θ(a)}. Decompose r into local runs r_{p} over 𝒳_{w}|_{p} for each p ∈ θ(a) by looking at r restricted to 𝒳_{w}|_{p}. Since ℛℋ_{p} has all reachable histories on secondary_{p}(𝒳_{w}), the projection h_{p} of r_{p} on secondary_{p}(𝒳_{w}) belongs to ℛℋ_{p}. So, the projection of r onto secondary_{θ(a)}(𝒳_{w}) belongs to ⨂_{p∈θ(a)} ℛℋ_{p}.

So, we can reconstruct all possible a-moves of 𝔄 after w by looking at ⨂_{p∈θ(a)} ℛℋ_{p}. The procedure for updating ℛℋ_{p} to ℛℋ′_{p} in the definition of →_{p}^{𝔅} then guarantees that ℛℋ′_{p} contains all reachable p-histories over secondary_{p}(𝒳_{u}) for each p ∈ θ(a).

□

8 The complexity of determinization

Analysis of the construction

Theorem 10 Let 𝔄 = ({V_{p}}_{p∈𝒫} , {→_{a}}_{a∈Σ}, 𝒱_{0}, 𝒱_{F}) be a non-deterministic asynchronous automaton with N processes such that max_{p∈𝒫} |V_{p}| = M. Then, in the corresponding deterministic automaton 𝔅 that we construct, each process has at most 2^{M^{O(N^{3})}} states.

Proof Each local state of 𝔅 is of the form ⟨λ_{p}, ℛℋ_{p}⟩. We have already argued that we can maintain labels with a set ℒ of size O(N^{3}). So, each entry ⟨P, ℓ⟩ in λ_{p} requires O(N) bits to write down P and O(log N) bits to write down ℓ—i.e., O(N) bits in all. Since there are N^{3} entries in λ_{p}, all of λ_{p} may be written down using O(N^{4}) bits.

We now need to maintain histories over secondary events. Each history h consists of N^{2} P -states. Since a P -state can be written down using N log M bits, h can be written down using N^{3} log M bits. The number of different histories possible over N^{2} is

(M^{O(N)})^{N^{2}} = M^{O(N^{3})}—each event could be assigned an arbitrary P -state and the number of distinct P -states is bounded by ∑_{i∈[1..N]} M^{i} which is M^{O(N)}. So, ℛℋ_{p} can be written down using M^{O(N^{3})} · N^{3} log M bits.

So, overall, each local state of 𝔅 can be written down using M^{O(N^{3})} bits. Therefore, the number of local states of each process in 𝔅 is bounded by 2^{M^{O(N^{3})}}. □

In certain cases, we can slightly improve the estimate given above. Let T be the size of the transition relation of 𝔄—i.e., T = ∑_{a∈Σ} | →_{a} | where | →_{a} |, the size of →_{a}, is just the number of pairs in the relation →_{a}. Then, we know that the P -states assigned by each history h must elements of →_{a} for some a ∈ Σ. So, the number of P -states we can assign is bounded by T. In general, T and M^{N} are not directly related, so a more accurate bound for the number of histories possible over N^{2} nodes is max(T, M^{O(N)})^{N^{2}}. Therefore, the number of local states of a process in 𝔅 is bounded by 2^{max(T^{N^{2}},M^{O(N^{3})})}.

Unlike conventional finite state automata, where determinization results in an exponential blowup in the number of states, our algorithm exhibits a superexponential blowup (at the level of local states). A simple argument shows that this cannot be avoided, in general.

A superexponential lower bound for determinization

Theorem 11 There is a sequence of languages L_{K^{N}} over distributed alphabets (Σ_{K^{N}} , θ_{K^{N}}), K, N ≥ 2, such that L_{K^{N}} is recognized by a non-deterministic asynchronous automaton whose local state spaces and transition relations are polynomial in size as functions of K and N, whereas L_{K^{N}} cannot be recognized by a deterministic asynchronous automaton unless it has at least one process with 2^{K^{N} /N} states.

Proof For Σ = {a, b}, let L_{m}^{1} be the set of words whose m^{th} letter from the right is a b. Recall that L_{m}^{1} can be recognized by an NFA with O(m) states whereas a DFA requires 2^{m} states to recognize this language. We generalize L_{m}^{1} to L_{m}^{k} for k ≥ 1—L_{m}^{k} is the set of words whose km^{th} last letter is a b. Let L_{m} = ⋃_{k≥1} L_{m}^{k}. It is not difficult to see that L_{m} is also regular and the exponential separation between NFAs and DFAs recognizing L_{m}^{1} continues to hold for L_{m} as well.

Consider L_{K^{N}} —i.e., L_{m}, where m = K^{N}—for some K, N ≥ 2. We look at a variant of L_{K^{N}} which we call L′_{K^{N}}. We show that L′_{K^{N}} can be recognized by a small nondeterministic asynchronous automaton—the states of each component will be quadratic in K and the transition relation will be polynomial in K and N. On the other hand, it will turn out that the smallest deterministic asynchronous automaton recognizing this language has at least one process with O(2^{K^{N} /N}) states.

The idea is to implement a N-digit counter to the base K using N processes named [1..N]. When the counter value is m, process i holds the value of the i^{th} digit in the base K representation of m.

To count efficiently using asynchronous automata, we need to introduce carry letters {c_{i}}_{i∈[1..N]} into our alphabet. So, c_{1} corresponds to a carry at the least significant digit, whereas c_{N} corresponds to an “overflow” carry at the most significant digit of our counter. Given a word w ∈ Σ^{∗}, we intersperse the carry bits as follows: every K^{th} letter from Σ is immediately followed by a c_{1} and every K^{th} c_{i} is immediately followed by a c_{i+1} for each i ∈ [1..N−1]. We call the new string C(w), the carry-extension of w.

Let Σ′ = {a, b} ∪ {c_{i}}_{i∈[1..N]}. Let θ′ be a distribution of Σ′ such that θ′(a) = θ′(b) = {1}, θ′(c_{N}) = {N} and θ′(c_{i}) = {i, i+1} for i ∈ [1..N−1]. This introduces a natural independence relation over Σ′ as we have already seen. As described in the Introduction, this independence relation can be lifted to finite words in the obvious way—w ∼ w′ iff w′ can be obtained from w by a finite sequence of permutations of adjacent independent letters. It is easy to check that ∼ is an equivalence relation. The equivalence classes induced by ∼ are usually called traces [Maz]. Let [w] denote the trace generated by a word w ∈ Σ^{′∗}.

The language we will work with is the set of traces generated by carry-extended words from L_{K^{N}}. Formally, we shall look at L′_{K^{N}} = {w ∈ Σ^{′∗} | ∃w′ ∈ L′′_{KN}. w ∈ [w′]}, where L′′_{KN} = {C(w) | w ∈ L_{K^{N}} }.

A deterministic asynchronous automaton recognizing L′_{KN} must have at least one process with a state space of size 2^{K^{N} /N}. To see this, consider a normal DFA recognizing L′_{K^{N}}. Let u and u′ be two distinct words over Σ of length K^{N}. Without loss of generality, we can assume that there is a position i such that u(i) = b and u′(i) = a. Then, there is a word v over Σ of length at most K^{N} such that uv ∈ L_{K^{N}} and u′v ∉ L_{K^{N}}.

Let w be the string such that C(u)w = C(uv). Clearly C(u)w = C(uv) ∈ L′_{K^{N}}. Notice that w ≠ C(v) in general. However, it is the case that w ↓_{{a,b}}—the string obtained by erasing all letters other than a and b from w—is just v. Now consider C(u′)w— there are two cases to look at. If C(u′)w is not trace equivalent to any valid carryextended word, then clearly C(u′)w does not belong to L′_{K^{N}}. On the other hand, if C(u′)w is trace equivalent to some carry-extended word w′, w′ ↓_{{a,b}} must be equal to C(u′)↓_{{a,b}} concatenated with w↓_{{a,b}}, since a and b are not independent in (Σ′, θ′). But C(u′)↓_{{a,b}} w↓_{{a,b}}= u′v. Since u′v ∉ L_{K^{N}}, C(u′v) ∉ L′′_{K^{N}} and so C(u′)w ∉ L′_{K^{N}} either.

So the canonical right invariant equivalence relation R_{L′_{K^{N}}} generated by L′_{K^{N}} has

at least 2^{K^{N}} equivalence classes. By the Myhill-Nerode Theorem, the minimal DFA recognizing L′_{K^{N}} has at least 2^{K^{N}} states. Thus any deterministic asynchronous automaton recognizing L′_{K^{N}} must have at least one component with ^{N} \sqrt{2^{K^{N}}} = 2^{K^{N} /N} states.

We now describe a small non-deterministic asynchronous automaton 𝔄 accepting L′_{K^{N}}. 𝔄 keeps counting letters in its input, using the carry letters to increment higher order digits of the counter. At some point, on reading a b, 𝔄 non-deterministically decides to copy its current counter value into a register. Meanwhile, 𝔄 continues to count letters from where it left off—it does not restart its counter when it sets the register. At the end of its input, it checks to see if the current counter value is the same as the one saved in the register. If so, the number of letters read after the b is a multiple of K^{N} and the input is accepted.

For each process i, the set of local states V_{i} is given by [0..K] × [0..K−1] × {N, Y }. The first component of the state is a digit in the running counter—the value K indicates a pending carry. The second component represents a “frozen” register value. The third component indicates whether or not the register value has been loaded. Initially, each process is in the state ⟨0, 0, N⟩. The final states are those where each process is in a state of the form ⟨j, j, Y ⟩ where j ∈ [0..K−1]—different processes could have different values of j.

The transition relations are as follows:

• →_{a}: (Affects only process 1)

⟨i, 0, N⟩ →_{a} ⟨i+1, 0, N⟩, provided i < K.

⟨i, j, Y ⟩ →_{a} ⟨i+1, j, Y ⟩, provided i < K.

• →_{b}: (Affects only process 1)

⟨i, 0, N⟩ →_{b} ⟨i+1, 0, N⟩, provided i < K.

⟨i, j, Y ⟩ →_{b} ⟨i+1, j, Y ⟩, provided i < K.

⟨i, 0, N⟩ →_{b} ⟨i+1, i, Y ⟩, provided i < K.

• →_{c_{i}}, i < N: (Affects processes i+1 and i. Each transition is of the form (v, w) →_{c_{i}} (v′, w′) where v and v′ are states of process i+1 and w and w′ are states of process i.)

(⟨i, 0, N⟩, ⟨K, 0, N⟩) →_{c_{i}} (⟨i+1, 0, N⟩, ⟨0, 0, N⟩), provided i < K

(⟨i, j, Y ⟩, ⟨K, j′, Y ⟩) →_{c_{i}} (⟨i+1, j, Y ⟩, ⟨0, j′, Y ⟩), provided i < K.

(⟨i, 0, N⟩, ⟨K, j′, Y ⟩) →_{c_{i}} (⟨i+1, i, Y ⟩, ⟨0, j′, Y ⟩), provided i < K.

• →_{c_{N}}: (Affects only process N)

⟨K, 0, N⟩ →_{c_{N}} ⟨0, 0, N⟩.

⟨K, j, Y ⟩ →_{c_{N}} ⟨0, j, Y ⟩.

So, after K a’s and b’s have been read process 1 gets stuck—a c_{1} must occur to propagate a carry before the next a or b can be read. After K c_{1}’s have occurred, a c_{2} must be read before the next c_{1}. However, since c_{2} is independent of a and b, this c_{2} need not be read immediately after the K^{th} c_{1}. In general, 𝔄 permits higher digit carries to propagate asynchronously while the first component continues to read a’s and b’s from the input. However, it is easy to check that 𝔄 ensures that after every K c_{i}’s, a c_{i+1} is read before the next c_{i}.

At some point, on reading a b, process 1 non-deterministically copies its counter value into the register and sets the third component of its state to Y. In the next round of carries, all the other processes get a signal to load their registers. Eventually all digits of the counter value when b occurred are stored in the register. Meanwhile, the counter continues to run freely on the remaining input. At the end of a word u, 𝔄 accepts u if each process has loaded its register and has the same value stored in the current counter as in the register.

Given this, it is straightforward, though tedious, to verify that 𝔄 does indeed accept L′_{K^{N}}.

Each process has O(K^{2}) states. The total number of entries in the transition relations of 𝔄 is O(NK^{3}). So, 𝔄 can be described in space polynomial in K and N. By our earlier analysis, if we determinize 𝔄 using our construction, we obtain an automaton whose local state space is 2^{(KN)^{O(N^{2})}}.

(Notice that we can implement a much simpler N-digit counter by allowing all N processes to synchronize on a and b. Then, we can eliminate the carry bits embedded in the input word—carries can be propagated “internally” when the processes synchronize. However, this naïve counter has O(K^{N}) entries in its transition table and so is much larger, in real terms, than the counter we have described.) □

References

[Die] V. Diekert: Combinatorics on Traces, LNCS 454 (1990).

[HU] J. Hopcroft, J.D. Ullman: Introduction to automata, languages and computation, Addison-Wesley (1979).

[Maz] A. Mazurkiewicz: Basic notions of trace theory, in: J.W. de Bakker, W.- P. de Roever, G. Rozenberg (eds.), Linear time, branching time and partial order in logics and models for concurrency, LNCS 354, (1989) 285–363.

[MS] M. Mukund, M. Sohoni: Keeping track of the latest gossip: Bounded time-stamps suffice, to appear in Proc. FST&TCS ’93, LNCS 761. Also available as Report TCS-93-3, School of Mathematics, SPIC Science Foundation, Madras (1993).

[Och] E. Ochmanski: Regular behaviour of concurrent systems, EATCS Bulletin, 27 (1985) 56–67.

[Pig] G. Pighizzini: Synthesis of nondeterministic asynchronous automata, in V. Diekert, W. Ebinger eds., Proc. ASMICS Workshop on Infinite Traces, Report 4/92, Fakultät Informatik, Universität Stuttgart, Germany (1992).

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