Automata, Languages and Programming, 21st International Colloquium, Proceedings, Serge Abiteboul, Eli Shamir (Eds.), Lecture Notes in Computer Science 820, Springer-Verlag (1994) 130–141.

Determinizing Asynchronous Automata

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

1 BRICS Center, Aarhus University, Ny Munkegade, DK 8000 Aarhus C, Denmark. E-mail: klarlund@daimi.aau.dk 2 School of Mathematics, SPIC Science Foundation, 92 G N Chetty Rd Madras 600 017, India. E-mail: {madhavan,sohoni}@ssf.ernet.in

Abstract. An asynchronous automaton consists of 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.

Zielonka’s theorem tells us that these automata can be determinized while retaining the synchronization structure. Unfortunately, this construction is indirect and yields a triple-exponential blow-up in size.

We present a direct determinization procedure for asynchronous automata which generalizes the classical subset construction for finite-state automata. Our construction is only double-exponential and thus is the first to essentially match the lower bound.

Introduction

Asynchronous automata, introduced by Zielonka [Zie1], are a natural generalization of finite-state automata for concurrent systems. An asynchronous automaton consists of a set of processes which periodically synchronize to process their input. Each letter a in the alphabet is associated with a subset θ(a) of processes which jointly decide on a move on reading a.

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

Alphabets equipped with independence relations, also called concurrent alphabets, were introduced by Mazurkiewicz for studying concurrent systems from the viewpoint of formal language theory [Maz]. Given a concurrent alphabet (Σ, I), I induces a equivalence relation ∼ on Σ^{∗}: for any two words w and w′, w ∼ w′ 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 ∼-consistent—i.e., for each w ∈ Σ^{∗}, if w is in L then all of [w] is contained in L. A trace language is recognizable if it is accepted by a conventional finite state automaton.

Asynchronous automata are natural machines for recognizing trace languages. Given a conventional finite automaton recognizing a trace language over (Σ, I),

⋆ The author is supported by a fellowship from the Danish Research Council. ⋆⋆ The author was partially supported by IFCPAR Project 502-1

we can construct a deterministic asynchronous automaton over a distributed alphabet (Σ, θ) recognizing the same language, such that the independence relation induced by θ is precisely I. This result was first proved by Zielonka [Zie1].

Contributions of this paper

In this paper, we generalize the classical subset construction of Rabin and Scott and obtain a direct procedure for determinizing an asynchronous automaton 𝔄. 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 indirect: 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. This route leads to a triple exponential blowup in general, even if we use the newer constructions of [CMZ, MS].

Our determinization construction is important for dealing with asynchronous automata over infinite traces [GP]. These automata generalize automata on infinite strings and lead to a nice theory of ω-regular trace languages. However, Büchi asynchronous automata [GP] are necessarily non-deterministic and lack an effective complementation construction. With a Muller acceptance condition, deterministic automata suffice [DM], but an effective determinization procedure is still missing. We believe that our subset construction will lead to direct constructions for determinizing and complementing these automata.

Recently, Muscholl [Mus] has described a subset construction for asynchronous cellular automata [Zie2], as part of a complementation procedure for Büchi asynchronous cellular automata. Though asynchronous cellular automata are expressively equivalent to asynchronous automata, the operational intuition underlying the two models is quite different and there appears to be no obvious way to connect the construction in [Mus] to the one presented here.

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 nonempty 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} for 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} and θ(a) ⊆ P, we write v⃗_{a} for v⃗_{θ(a)} and v⃗\overline{a} for 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. Each relation →_{a} specifies how the processes θ(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 global 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 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 recognized by 𝔄, is the set of words accepted by 𝔄. The problem For a given non-deterministic asynchronous automaton 𝔄 over (Σ, θ), construct a deterministic asynchronous automaton 𝔅 over (Σ, θ), such that L(𝔄) = L(𝔅).

For sequential finite automata, the determinization problem can be solved using the classical subset construction of Rabin and Scott. At the end of any word u, the subset automaton maintains the set of possible states that the original (non-deterministic) automaton could be in after reading u.

To determinize a non-deterministic asynchronous automaton 𝔄, we have to modify the subset construction to work at the level of local states. The main hurdle is the following: In general, the set of reachable global states of 𝔄 after reading u is not just the product of the subsets of reachable local states of the individual processes.

For instance, suppose we have two processes p and q with local state spaces V_{p} = {0_{p}, 1_{p}, 2_{p}} and V_{q} = {0_{q}, 1_{q}, 2_{q}}. Let a be a letter such that θ(a) = {p, q} and →_{a}= {(⟨0_{p}, 0_{q}⟩, ⟨1_{p}, 1_{q}⟩), (⟨0_{p}, 0_{q}⟩, ⟨2_{p}, 2_{q}⟩)}. Suppose p and q start in the local states 0_{p} and 0_{q} respectively. After reading a, the state of p could be either 1_{p} or 2_{p}. Similarly, local state of q could either be 1_{q} or 2_{q}. However, the set of possible {p, q}-states after reading a is not the naïve product {1_{p}, 2_{p}}×{1_{q}, 2_{q}}— the only reachable {p, q}-states are ⟨1_{p}, 1_{q}⟩ and ⟨2_{p}, 2_{q}⟩.

So, to determinize an asynchronous automaton 𝔄, we need to record more than just the subset of reachable local states for each process in order to keep track of the valid global states of 𝔄. We also have to “remember” how each current local state arose. We then need to compose these histories so that each consistent composition of histories yields a valid global state of 𝔄 and, moreover, all the reachable global states of 𝔄 can be obtained in this manner.

2 Local and global views

We represent words as labelled partial orders. The notions we use are essentially those of trace theory [Maz]. Events With u : [1..m] → Σ, we associate a set of events ℰ_{u}. Each event e 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}. If e = (i, a) is an event, then we may use e instead of a in abbreviations such as V_{e}, which stands for V_{a}, i.e., V_{θ(a)}, or →_{e}, which is just →_{a}. For p ∈ 𝒫 and e ∈ ℰ, we write p ∈ e to denote that p ∈ θ(u(i)) when e = (i, u(i)); for e = 0, we define p ∈ e to hold for all p ∈ 𝒫. If p ∈ e, then we say that e is a p-event. Ordering relations on ℰ The word u imposes a total order on events: define e < f if e ≠ f and either e = 0 or e = (i, u(i)), f = (j, u(j)), and i < j. We write e ≤ f if e = f or e < f. Moreover, each process p orders the events in which it participates: define ◁_{p} to be the strict ordering

e ◁_{p} f iff e < f, p ∈ e ∩ f and for all e < g < f, p ∉ g.

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

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

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; •; p; q; r; s; b; a; c; b; a; c; d; e_{0}; e_{1}; e_{2}; e_{3}; e_{4}; e_{5}; e_{6}; e_{7}]

Fig. 1. An example

Example 1. Consider the word bacbacd over the alphabet (Σ, θ) for 𝒫 = {p, q, r, s}, where Σ = {a, b, c, d} and θ(a) = {p, q}, θ(b) = {q, r}, θ(c) = {r, s} and θ(d) = {p}. The set of events ℰ_{u} is then {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}, e_{7}} = {0, (1, b), (2, a), (3, c), (4, b), (5, a), (6, c), (7, d)}.

Figure 1 describes (ℰ_{u}, ⊑^{∗}). The arrows between the events indicate the relations ◁_{p}, ◁_{q}, ◁_{r} and ◁_{s}. For example, e_{0} ◁_{r} e_{1} holds, but e_{0} ◁_{p} e_{1} does not hold.

The set of events e_{7}↓ is {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{7}} while e_{6}↓ is {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{6}}. Thus e_{6}↓ ∪ e_{7}↓= ℰ. The neighbourhood of e_{5}, nbd(e_{5}), is {e_{2}, e_{4}, e_{5}}.

Ideals I ⊆ ℰ is called an (order) ideal if I is closed with respect to ⊑^{∗}—i.e., e ∈ I and f ⊑^{∗} e implies f ∈ I as well.

Clearly, the entire set ℰ is an ideal, as is e↓ for any e ∈ ℰ. 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.

Example 2. In the example of Figure 1, max_{r}(ℰ) = e_{6}. So ℰ|_{r} = e_{6} ↓= {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{6}}. On the other hand, max_{p}(ℰ) = e_{7} and ℰ|_{p} = e_{7} ↓= {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{7}}.

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 e ∈ I an e-state—i.e., a state in V_{e}—such that r(0) ∈ 𝒱_{0} and for all e ≠ 0, r is consistent with →_{e} in nbd(e). In other words, for e ≠ 0 we have v⃗ →_{e} r(e), where v⃗ is the e-state such that for all q ∈ e, v⃗_{q} = r(f)_{q}, where f ◁_{q} e.

So, a local run on ℰ assigns an e-state to each e ∈ ℰ in such a way that all neighbourhoods in ℰ are consistently labelled. Let ℛ(I) denote the set of all local runs on I. The following is easy to verify.

Proposition 1. Given u : [1..m] → Σ, there is a 1-1 correspondence between ℛ(ℰ_{u}), the set of local runs on ℰ_{u}, and the set of global runs on u.

Example 3. Let 𝔄 = ({V_{p}}_{p∈𝒫} , {→_{a}}_{a∈Σ}, 𝒱_{0}, 𝒱_{F}) be an asynchronous automaton over (Σ, θ), where 𝒫 and (Σ, θ) are as in our previous example. Each process has four local states. Thus, V_{p} = {1_{p}, 2_{p}, 3_{p}, 4_{p}}, V_{q} = {1_{q}, 2_{q}, 3_{q}, 4_{q}} etc.

Let the local transition relations of 𝔄 be defined as in the table below:

→_{a}  →_{b}  →_{c}  →_{d}
{(⟨1_{p}, 2_{q}⟩, ⟨3_{p}, 3_{q}⟩) {(⟨1_{q}, 1_{r}⟩, ⟨2_{q}, 2_{r}⟩) {(⟨2_{r}, 1_{s}⟩, ⟨4_{r}, 4_{s}⟩) {(⟨3_{p}⟩, ⟨4_{p}⟩)
(⟨1_{p}, 3_{q}⟩, ⟨4_{p}, 4_{q}⟩) (⟨1_{q}, 1_{r}⟩, ⟨3_{q}, 3_{r}⟩) (⟨2_{r}, 3_{s}⟩, ⟨4_{r}, 4_{s}⟩) (⟨4_{p}⟩, ⟨3_{p}⟩)}
(⟨3_{p}, 2_{q}⟩, ⟨4_{p}, 4_{q}⟩) (⟨3_{q}, 4_{r}⟩, ⟨2_{q}, 2_{r}⟩) (⟨2_{r}, 4_{s}⟩, ⟨1_{r}, 1_{s}⟩)
(⟨4_{p}, 2_{q}⟩, ⟨3_{p}, 3_{q}⟩)} (⟨4_{q}, 3_{r}⟩, ⟨2_{q}, 2_{r}⟩)} (⟨3_{r}, 1_{s}⟩, ⟨3_{r}, 3_{s}⟩)}

𝒱_{0} = {⟨1_{p}, 1_{q}, 1_{r}, 1_{s}⟩} and 𝒱_{F} = {⟨4_{p}, 3_{q}, 1_{r}, 1_{s}⟩, ⟨3_{p}, 4_{q}, 4_{r}, 4_{s}⟩}.

Then, the local runs corresponding to the only two possible global runs of 𝔄 on u = bacbacd are shown in Figure 2. The left half of each event is labelled by the first run and the right half by the second run. Neither run leads to a state in 𝒱_{F} so 𝔄 does not accept u.

[figure: p; q; r; s; b; a; c; b; a; c; d; e_{0}; e_{1}; e_{2}; e_{3}; e_{4}; e_{5}; e_{6}; e_{7}; 1_{p}; 1_{p}; 3_{p}; 4_{p}; 4_{p}; 3_{p}; 3_{p}; 4_{p}; 1_{q}; 1_{q}; 2_{q}; 3_{q}; 3_{q}; 4_{q}; 2_{q}; 2_{q}; 4_{q}; 3_{q}; 1_{r}; 1_{r}; 2_{r}; 3_{r}; 4_{r}; 3_{r}; 2_{r}; 2_{r}; 1_{r}; 4_{r}; 1_{s}; 1_{s}; 4_{s}; 3_{s}; 1_{s}; 4_{s}]

Fig. 2. Local runs

Histories Let I be an ideal. A history on I is a partial function h which assigns states to some of the events in I; i.e., domain(h) ⊆ I and h(e) ∈ V_{e} for each e ∈ domain(h). A history h is reachable if there is some local run r on I such that h(e) = r(e) for all e ∈ domain(h). Let ℋ(I) denote the set of all histories on I. Clearly, every local run on I is a history; i.e., ℛ(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 e ∈ domain(h_{p}) ∩ domain(h_{q}), h_{p}(e) = h_{q}(e).

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

⨂_{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 domain(h) = ⋃_{p} domain(h_{p}) and \\ ∀p ∈ P. ∀e ∈ domain(h_{p}). h(e) = h_{p}(e)\}. \end{matrix}

So, ⨂_{p∈P} H_{p} contains all the histories on I|_{P} which may be pieced together using mutually consistent histories from the sets H_{p}.

Example 4. Consider the local runs shown in Figure 2. For p, let h_{p}^{1} and h_{p}^{2} be two histories where

h_{p}^{1} = {(e_{3} ↦ ⟨4_{r}, 4_{s}⟩, e_{4} ↦ ⟨2_{q}, 2_{r}⟩, e_{5} ↦ ⟨4_{p}, 4_{q}⟩, e_{7} ↦ ⟨3_{p}⟩)}, and h_{p}^{2} = {(e_{3} ↦ ⟨3_{r}, 3_{s}⟩, e_{4} ↦ ⟨2_{q}, 2_{r}⟩, e_{5} ↦ ⟨3_{p}, 3_{q}⟩, e_{7} ↦ ⟨4_{p}⟩)}.

For s, let h_{s}^{1} and h_{s}^{2} be two histories where h_{s}^{1} = {(e_{2} ↦ ⟨3_{p}, 3_{q}⟩, e_{4} ↦ ⟨2_{q}, 2_{r}⟩, e_{6} ↦ ⟨4_{r}, 4_{s}⟩)}, and h_{s}^{2} = {(e_{2} ↦ ⟨4_{p}, 4_{q}⟩, e_{4} ↦ ⟨2_{q}, 2_{r}⟩, e_{6} ↦ ⟨1_{r}, 1_{s}⟩)}.

All four of these histories are reachable. There are four possible {p, s}-choices for {{h_{p}^{1}, h_{p}^{2}}, {h_{s}^{1}, h_{s}^{2}}}. Each of these choices is consistent. However, only two of the runs in {h_{p}^{1}, h_{p}^{2}} ⨂{h_{s}^{1}, h_{w}^{2}} are reachable—those generated by the choices (h_{p}^{1}, h_{s}^{1}) and (h_{p}^{2}, h_{s}^{2}). The “bad” choice (h_{p}^{2}, h_{s}^{1}) implies that ⟨4_{p}, 3_{q}, 1_{r}, 1_{s}⟩ is a valid global state of 𝔄 after u, which leads to the erroneous conclusion that 𝔄 accepts u. The task is to rule out such bad choices by maintaining reachable histories whose products are also reachable.

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 ⊆ 𝒫. Then, ℛ(I|_{P}) = ⨂_{p∈P} ℛ(I|_{p}).

Proof The fact that ℛ(I|_{P}) ⊆ ⨂_{p∈P} ℛ(I|_{p}) is obvious.

To show the converse, let r ∈ ⨂_{p∈P} ℛ(I|_{p}) where the consistent P -choice is {r_{p}}_{p∈P}. Clearly domain(r) = I|_{P}. We just have to check that nbd(e) is labelled consistently by r for each e ∈ I|_{P}. But, if e ∈ I|_{P} then e ∈ I|_{p} for some p ∈ P and so nbd(e) ⊆ I|_{p} as well. Since r = r_{p} on I|_{p} and r_{p} is a local run on I|_{p}, r_{p} must have assigned consistent values to nbd(e). □

4 Finite histories and frontiers

Frontiers Let I be an ideal and p, q, s ∈ 𝒫. We say that event e ∈ I|_{p} is an s-sentry for p with respect to q if e ∈ I|_{p} ∩ I|_{q} and e ◁_{s} f for some f ∈ I|_{q} − I|_{p}. Thus e is an event known to p and q whose s-successor is known only to q.

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

Example 5. In the example of Figure 1, ℰ|_{p} ∩ ℰ|_{s} = {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}}. Then frontier_{ps}(ℰ) = {e_{3}, e_{4}}, whereas frontier_{sp}(ℰ) = {e_{2}, e_{4}}. So, e_{4} belongs to both frontiers—it is an r-sentry in frontier_{ps}(ℰ) and a q-sentry in frontier_{sp}(ℰ).

In general, e ∈ frontier_{pq}(I) could simultaneously be an s-sentry for several different s. However, frontier_{pq}(I) is always a bounded set, since for each s ∈ 𝒫 there is at most one s-sentry e ∈ frontier_{pq}(I). For P ⊆ 𝒫 and p ∈ P, define the P -frontier of p at I to be the set

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

Lemma 3. 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,

(i) h_{p} is reachable; and
(ii) the P -frontier of p is included in domain(h_{p}).

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

Proof 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 domain(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 domain(h) = ⋃_{p∈P} domain(h_{p}).

Define r as follows:

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

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

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”. Clearly domain(r) = I|_{P} and r agrees with h on domain(h). We have to show that r is a local run; i.e., we have to show that r is consistent with →_{e} across nbd(e) for each e ∈ I|_{P}.

Let e ∈ I|_{P}. We know that r(e) was assigned at some stage i ∈ [1..k]. Clearly, e ∈ I|_{p_{i}} and so nbd(e) ⊆ I|_{p_{i}} as well. If nbd(e) ⊆ I|_{p_{i}} −I|_{P_{i−1}}, then all the events in nbd(e) 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 →_{e}.

The crucial case is when some f ∈ nbd(e) lies in I|_{P_{i−1}} and so has already been assigned a value. But then f ∈ 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_{ℓ}, ℓ ∈ [1..i−1], f belongs to frontier_{p_{ℓ}p_{i}}(I). So f ∈ domain(h_{p_{ℓ}}) ∩ domain(h_{p_{i}}), by assumption. Therefore, the value r(f) must agree with h_{p_{ℓ}}(f) = h_{p_{i}}(f) and hence must agree with r_{p_{i}}(f) as well. So, even though f ∈ nbd(e) has already been assigned a value before stage i, the value agrees with r_{p_{i}}. Thus, effectively, nbd(e) is assigned values as given by r_{p_{i}} and these must be consistent with →_{e} 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}. Then, by the previous lemma, the product of these histories will generate all the reachable global states of 𝔄 after u. Further, the number of possible histories on a bounded set is also finite.

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

Example 6. In Figure 1, latest_{s→p}(ℰ) = e_{2} whereas latest_{p→s}(ℰ) = e_{3}. Also, latest_{s→p→r}(ℰ) = e_{1} while latest_{p→s→r}(ℰ) = e_{3}.

The following result, which is proved in [KMS, MS], lets us identify all the frontier events in ℰ using primary and secondary information.

Lemma 4. Let I be an ideal, p, q, s ∈ 𝒫 and e ∈ frontier_{pq}(I) an s-sentry. Then e = latest_{p→s}(I). Also, for some s′ ∈ 𝒫, e = latest_{q→s′→s}(I).

So, for every p ∈ 𝒫 and u ∈ Σ^{∗}, each process p maintains all reachable histories over the finite set 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. (Note that secondary_{𝒫} (ℰ_{ua}) is a subset of secondary_{𝒫} (ℰ_{u}) together with the new a-event.)

Since we are manipulating events, in general, we require a mechanism for assigning “unambiguous” labels to the events in ℰ_{u} while u is being read. In our context, “unambiguous” means that distinct events in secondary_{𝒫} (ℰ_{u}) are assigned distinct labels. It turns out that we can maintain such a labelling using a finite set of labels ℒ and simultaneously update the labels assigned to secondary_{𝒫} (ℰ_{u}) in a consistent way with each local synchronization. This involves running the “gossip automaton” [MS] in the background. We will suppress the details here but assume that there is an asynchronous automaton 𝔄_{G} with the same structure as the automaton 𝔄 which works as follows.

Let u ∈ Σ^{∗}. Each process p in 𝔄_{G} inductively maintains a labelling function λ_{p}(u) : 𝒫 × 𝒫 → ℒ such that:

1. Let q, s ∈ 𝒫. Then for all q′, q′′, s′, s′′ ∈ 𝒫, λ_{q}(u)(q′, q′′) = λ_{s}(u)(s′, s′′) iff latest_{q→q′→q′′}(ℰ_{u}) = latest_{s→s′→s′′}(ℰ_{u}).

2. If w = ua and q, q′, q′′, s, s′, s′′ ∈ 𝒫 such that latest_{q→q′→q′′}(ℰ_{w}) = latest_{s→s′→s′′}(ℰ_{u}) then λ_{q}(w)(q′, q′′) = λ_{s}(u)(s′, s′′).

So, after reading u, each process p in 𝔄_{G} maintains a labelling λ_{p}(u) of secondary_{p}(ℰ_{u}) such that, across the system, distinct events in secondary_{𝒫} (ℰ_{u}) are assigned distinct labels. The map λ_{p}(u) is a finite object and can be incorporated into the local state of p. Further, all the processes which synchronize on an action a can consistently update their primary and secondary information and extend the labellings {λ_{p}(u)}_{p∈a} to new labellings {λ_{p}(ua)}_{p∈a} which maintain the inductive assertion. The second condition ensures that the new labellings {λ_{p}(ua)}_{p∈a} do not reassign fresh labels to “old” events in secondary_{𝒫} (ℰ_{ua}).

6 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(𝔅). 𝔅 will incorporate the gossip automaton 𝔄_{G}.

Formally, a state in V_{p}^{𝔅} consists of the following information:

– A labelling λ_{p} : (𝒫 × 𝒫) → ℒ.

– A set of histories ℛℋ_{p} where each h ∈ ℛℋ_{p} is a partial function on ℒ that maps a label ℓ to a P -state (where P ⊆ 𝒫 is the set of processes that participated in the event that ℓ was assigned to) such that domain(h) = range(λ_{p}).

Intuitively, after reading a word u, process p has computed λ_{p} as the labelling of secondary_{p}(ℰ_{u}) given by the gossip automaton 𝔄_{G}. Thus, the label λ_{p}(q, r) represents the secondary event latest_{p→q→r}(ℰ_{u}).

The set ℛℋ_{p} is supposed to contain all reachable histories over the secondary events secondary_{p}(ℰ_{u}). Since distinct events in secondary_{p}(ℰ_{u}) are assigned distinct labels, each history in ℛℋ_{p} is a function from range(λ_{p}) to P -states.

Initially, each p ∈ 𝒫 stores the following:

– For each pair of processes q, r ∈ 𝒫, λ_{p}(q, r) = ℓ_{0}, where ℓ_{0} is some arbitrary but fixed label from ℒ.

– For each initial state v⃗ of 𝔄, there is a history h in ℛℋ_{p} such that h(ℓ_{0}) = v⃗.

The initial state 𝒱_{0}^{𝔅} is the product of the initial states of the individual processes. We now describe the transition rules {→_{a}^{𝔅}}_{a∈Σ}. Suppose 𝔅 reads a when the global state of 𝔅 is {⟨λ′_{p}, ℛℋ′_{p}⟩}_{p∈𝒫} . Then the local states of processes in a are updated as follows.

– For each p ∈ a, construct a new labelling function λ′′_{p} : 𝒫 × 𝒫 → ℒ. This is done by the gossip automaton, 𝔄_{G}. For the new event e_{a}, let λ′′_{p}(e_{a}) = ℓ_{a}.

– 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, p)))_{p} for each p ∈ a (recall that latest_{p→p→p}(I) = max_{p}(I)). 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 e_{a} so that nbd(e_{a}) is consistently labelled with respect to →_{a}. Each element v′ ∈ 𝒱_{h_{a}} together with h_{a} generates a history h′_{p} in ℛℋ′′_{p}:

∀ℓ ∈ range(λ′′_{p}). h′_{p}(ℓ) = \begin{cases}v′ & if ℓ = ℓ_{a} \\ h_{a}(ℓ) & otherwise \end{cases}

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∈)}{ℛℋ′_{p}} to generate the entire set ℛℋ′′_{p} for each p ∈ a.

We now define the final states of 𝔅. Let σ⃗ be a global state of 𝔅, where σ⃗_{p} = ⟨λ′_{p}, ℛℋ′_{p}⟩ for each p ∈ 𝒫. Each history 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 5. 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} 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, 3 and 4 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|. (|u| = 0). Then u = ε, the empty word. The claim is trivially true at this state since all the secondary events in ℰ_{u} are the initial event 0 and each process maintains a set of histories which assigns all possible initial states of 𝔄 to the initial event. (|u| > 0). Let u = wa and assume inductively that after reading w, the local states {⟨λ′_{p}, ℛℋ′_{p}⟩}_{p∈𝒫} satisfy the Claim. We have to argue that the procedure for updating the local states of p ∈ a maintains the property asserted in the Claim.

Now, assume ℛℋ′_{p} contains all reachable histories over secondary_{p}(ℰ_{w}) for each p ∈ a. The gossip automaton 𝔄_{G} guarantees that λ′′_{p} labels precisely the events in secondary_{p}(ℰ_{u}). We have to show that ℛℋ′′_{p} contains all reachable histories over secondary_{p}(ℰ_{u}).

For all p ∈ a, ℰ_{u}|_{p} = ℰ_{w}|_{a} ∪ {e_{a}}, where e_{a} is the new a-event. So, any local run on ℰ_{u}|_{p} consists of a local run on ℰ_{w}|_{a} extended to cover e_{a} such that nbd(e_{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 3, 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. □

7 The complexity of determinization

Theorem 6. 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}⟩. From [MS], 𝔄_{G} can maintain and update λ_{p} consistently using O(N^{3} log N) 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} events is (M^{O(N)})^{N^{2}} = M^{O(N^{3})}. A set of histories can therefore be written down using M^{O(N^{3})} bits. So, in total we need M^{O(N^{3})} + O(N^{3} log N) = M^{O(N^{3})} bits. □

The upper bound we describe above is essentially optimal because of the following double-exponential lower bound, which is proved in [KMS].

Theorem 7. 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 with local state spaces and transition relations whose sizes are polynomial in K and N, whereas any deterministic asynchronous automaton recognizing L_{K^{N}} must have at least one process with 2^{K^{N} /N} states.

References

[CMZ] R. Cori, Y. Metivier, W. Zielonka: Asynchronous mappings and asynchronous cellular automata, Inf. and Comput., 106 (1993) 159–202.

[DM] V. Diekert, A. Muscholl: Deterministic asynchronous automata for infinite traces, Proc. STACS ’93, LNCS 665 (1993) 617–628.

[GP] P. Gastin, A. Petit: Asynchronous cellular automata for infinite traces, Proc. ICALP ’92, LNCS 623 (1992) 583–594.

[KMS] N. Klarlund, M. Mukund, M. Sohoni: Determinizing asynchronous automata, Report DAIMI-PB 460, Computer Science Department, Aarhus University, Aarhus, Denmark (1993).

[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: Gossiping, asynchronous automata and Zielonka’s theorem, Report TCS-94-2, School of Mathematics, SPIC Science Foundation, Madras (1994). See also “Keeping track of the latest gossip: Bounded timestamps suffice”, Proc. FST&TCS ’93, LNCS 761 (1993) 388–399.

[Mus] A. Muscholl: On the complementation of Büchi asynchronous cellular automata, Proc. ICALP 1994.

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

[Zie2] W. Zielonka: Safe executions of recognizable trace languages, in Logic at Botik, LNCS 363 (1989) 278–289.