BRICS RS-95-58 Klarlund et al.: Determinizing Asynchronous Automata on In�nite Inputs

BRICS

Basic Research in Computer Science

Determinizing Asynchronous Automata on In�nite Inputs

Nils Klarlund Madhavan Mukund Milind Sohoni

BRICS Report Series RS-95-58 ISSN 0909-0878 November 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Determinizing Asynchronous Automata on Infinite Inputs

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

Abstract

Asynchronous automata are a natural distributed machine model for recognizing trace languages—languages defined over an alphabet equipped with an independence relation.

To handle infinite traces, Gastin and Petit introduced Büchi asynchronous automata, which accept precisely the class of ω-regular trace languages. Like their sequential counterparts, these automata need to be non-deterministic in order to capture all ω-regular languages. Thus complementation of these automata is non-trivial. Complementation is an important operation because it is fundamental for treating the logical connective “not” in decision procedures for monadic secondorder logics.

Subsequently, Diekert and Muscholl solved the complementation problem by showing that with a Muller acceptance condition, deterministic automata suffice for recognizing ω-regular trace languages. However, a direct determinization procedure, extending the classical subset construction, has proved elusive.

In this paper, we present a direct determinization procedure for Büchi asynchronous automata, which generalizes Safra’s construction for sequential Büchi automata. As in the sequential case, the blow-up in the state space is essentially that of the underlying subset construction.

1BRICS Centre, Aarhus University, Ny Munkegade, DK 8000 Aarhus C, Denmark.

E-mail: klarlund@daimi.aau.dk. The author is supported by a fellowship from the Danish Research Council.

2School of Mathematics, SPIC Science Foundation, 92 G N Chetty Rd, Madras 600 017, India. E-mail: madhavan@ssf.ernet.in.

3Department of Computer Science and Engineering, Indian Institute of Technology, Bombay 400 076, India. E-mail: sohoni@cse.iitb.ernet.in.

Introduction

Finite-state automata are, by definition, sequential. To describe finite-state concurrent computations, Zielonka introduced asynchronous automata [Zie1]. An asynchronous automaton consists of a set of independent processes which cooperate to read their input. Each letter a in the alphabet is associated with a subset θ(a) of processes which jointly decide on a move when a is read.^{1} The distribution function θ introduces an independence relation I between letters: (a, b) ∈ I iff a and b are read by disjoint sets of processes.

Earlier, Mazurkiewicz had proposed a framework for studying concurrent systems where the alphabet Σ comes equipped with a pre-specified independence relation I, describing the concurrency in the system [Maz]. In this setting, two words w and w′ describe the same computation iff w′ can be obtained from w by a finite sequence of permutations of adjacent independent letters. This gives rise to an equivalence relation on words over Σ. The equivalence class [w] containing w is called a trace. A set of words L is said to be a trace language if it obeys the equivalence relation generated by I— for each word w in L, all of [w] is contained in L.

Zielonka proved that any regular trace language over a concurrent alphabet (Σ, I) can be recognized by a deterministic asynchronous automaton over a distributed alphabet (Σ, θ), such that the independence relation generated by θ is exactly I.

Gastin and Petit have extended the connection between asynchronous automata and trace languages to the setting of infinite inputs. In [GP], they introduce the class of Büchi asynchronous automata which accept precisely the class of ω-regular trace languages.

Like automata over infinite strings, Büchi asynchronous automata have close connections to logic [EM, Thi]. In order to exploit these connections— for instance, to automate verification of formulae defined using these logics— we need to develop techniques for manipulating these automata. Basic operations include complementation, which in logic is the equivalent of replacing a second-order existential quantifier with a second-order universal quantifier, and determinization, which is equivalent to replacing a second-order quantifier by first-order quantifiers.

1Calling these automata asynchronous is, in a sense, misleading. The processes communicate synchronously. The asynchrony refers to the fact that different components of the network can proceed independently while reading the input.

As in the sequential case, complementing Büchi asynchronous automata is non-trivial, since they are necessarily non-deterministic: deterministic Büchi asynchronous automata cannot recognize all ω-regular trace languages [GP]. With a Muller acceptance condition, deterministic automata suffice [DM], but a direct determinization procedure has so far been elusive.

Contributions of this paper

We extend the subset construction for asynchronous automata [KMS] to a direct determinization construction for Büchi asynchronous automata, based on Safra’s technique for determinizing Büchi automata on infinite strings [Saf]. The determinized automaton we construct has an acceptance condition described in terms of “Rabin pairs”. As in the sequential case, we can easily complement the determinized automaton by viewing the Rabin condition as a Streett condition. This Streett automaton can then be converted efficiently into a non-deterministic Büchi asynchronous automaton. So, we also have a direct complementation construction for Büchi asynchronous automata. In both the determinized Rabin automaton and the complementary Büchi automaton, the number of local states of each process is exponential in the number of global states of the original automaton. As in Safra’s original construction, this blow-up is essentially that of the underlying subset construction for these automata.

In related work, Muscholl [Mus] has described a complementation construction for Büchi asynchronous cellular automata, which are an alternative distributed model for recognizing trace languages [Zie2]. Her construction does not involve determinization—she makes use of progress measures [Kla] and directly constructs a non-deterministic complement automaton.

An asynchronous cellular automaton allocates a separate process for each letter in the input alphabet—even when the underlying system is completely sequential, a cellular automaton will have a number of components. Processes communicate using a non-standard variant of a shared memory. As a result, though both the approaches are formally equivalent, asynchronous automata seem to be more natural models for describing distributed systems.

Converting between asynchronous automata and asynchronous cellular automata involves a blow-up in the state space of each process which is exponential in |Σ|, the size of the input alphabet. However, since |Σ| could itself be exponential in the size of the global state space of the automaton, there is effectively a double exponential blow-up in this translation. So, complementing asynchronous automata directly using our construction can be significantly more efficient than complementing them indirectly via the construction described in [Mus].

In general, it appears to be advantageous to work directly with asynchronous automata for automating decision procedures in logic, instead of using asynchronous cellular automata. Incorporating the alphabet into the state space of the automaton is known to be expensive in such applications— for example, the decision procedure for monadic second-order logic on strings generates alphabets that are exponential in the number of free variables in the input formula; see [HJJ] for techniques which allow automata with exponentially sized alphabets to be represented and manipulated within polynomial bounds.

Working directly with asynchronous automata is also relevant to model checking—a technique for mechanically verifying if a program satisfies a property specified in a logical language. If the same kind of automata are used both for describing the program and for checking satisfiability, the model checking problem reduces to a simple intersection problem involving the automata [VW]. Since asynchronous automata are a natural model for distributed programs, automata-theoretic model checking can be applied to the logics considered in [EM, Thi].

The paper is organized as follows. We begin with some definitions regarding asynchronous automata. In Section 2 we introduce Büchi and Rabin asynchronous automata and formulate the problem. The next three sections recapitulate some basic techniques developed in [KMS, MS] for manipulating asynchronous automata. In Section 6 we show how to apply these techniques to determinize Büchi asynchronous automata. To preserve continuity, some detailed explanations, examples and proofs have been moved from the main text into separate Appendices.

1 Preliminaries

The following definitions are essentially those of [KMS] adapted to the setting of infinite inputs.

Distributed alphabets Let 𝒫 be a finite set of processes, where the size of 𝒫 is N. A distributed alphabet is a pair (Σ, θ) where Σ is a finite set of actions and θ : Σ → 2^{𝒫} assigns a non-empty 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 ⊆ 𝒫, V_{P} denotes the product ∏_{p∈P} V_{p}. An element v⃗ of V_{P} is a tuple or joint state that determines a local state for each p in P. We refer to a joint state from V_{P} as a P -state. A 𝒫-state is also called a global state.

Given v⃗ ∈ V_{P}, and P′ ⊆ P, v_{P′} denotes 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 automata An asynchronous automaton 𝔄 over (Σ, θ) is of the form ({V_{p}}_{p∈𝒫} , {→_{a}}_{a∈Σ}, 𝒱_{0}), where →_{a} ⊆ V_{a} × V_{a} is the local transition relation for a, and 𝒱_{0} ⊆ V_{𝒫} is a set of initial 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 α be an infinite word over Σ. It is convenient to think of α as a function of time; i.e., α : N → Σ. (We use N to denote the set {1, 2, …} and N_{0} for {0, 1, 2, …}.) We shall also deal with finite words over Σ. Let u ∈ Σ^{∗} be a word of length m. We denote u as a function u : [1..m] → Σ, where [i..j] abbreviates the set {i, i+1, …, j}.

A global run of 𝔄 on a word α : N → Σ is a function ρ : N_{0} → V_{𝒫} such that ρ(0) ∈ 𝒱_{0} and, for i ∈ N, ρ(i−1) ⟹^{α(i)} ρ(i). Similarly, a global run of 𝔄 on a finite word u : [1..m] → Σ is a function ρ : [0..m] → V_{𝒫} such that

ρ(0) ∈ 𝒱_{0} and, for i ∈ [1..m], ρ(i−1) ⟹^{u(i)} ρ(i).

For P ⊆ 𝒫, ρ_{P} denotes the projection of ρ onto the P -components. Note that ρ_{P} is a sequence of P -states. As usual, inf (ρ_{P}) denotes the set of P -states which occur infinitely often in ρ_{P}; i.e., inf (ρ_{P}) = {v⃗ ∈ V_{P} | for infinitely many i, ρ_{P} (i) = v⃗}.

2 Asynchronous automata on infinite inputs

To define how an asynchronous automaton accepts an infinite input α, we have to analyze the communication pattern between processes in the limit, as α is being processed.

Limit graphs With each infinite word α, we associate an undirected graph 𝒢_{α} = (𝒫, E_{α}) called the limit graph of α. The graph has an edge between processes p and q provided they synchronize infinitely often while 𝔄 processes α. In other words, (p, q) ∈ E_{α} iff for infinitely many i, {p, q} ⊆ θ(α(i)). Let Conn_{α} denote the maximal connected components of 𝒢_{α}.

Let Finite_{α} denote the set of processes which move only finitely often while 𝔄 reads α—i.e., p belongs to Finite_{α} if there are only finitely many i such that p ∈ θ(α(i)). Clearly, if p ∈ Finite_{α} then the singleton {p} belongs to Conn_{α}.

Büchi asynchronous automata A Büchi asynchronous automaton is a pair B𝔄 = (𝔄, 𝒯_{B}) where 𝔄 is an asynchronous automaton and 𝒯_{B} is a Büchi acceptance table. The table 𝒯_{B} is a list (τ_{1}, τ_{2}, …, τ_{k}). Each entry τ_{i} in 𝒯_{B} is of the form (C, T, {(p_{C}, G_{C})}_{C∈C}), where C is a partition of 𝒫, T is a subset of 𝒫 and, for each subset C ∈ C, p_{C} is a designated process from C and G_{C} is a set of p_{C}-states. We call the processes {p_{C}}_{C∈C} the signalling processes in τ_{i}.

A run ρ of the automaton B𝔄 = (𝔄, 𝒯_{B}) on an input α is said to satisfy an entry τ = (C, T, {(p_{C}, G_{C})}_{C∈C}) in 𝒯_{B} provided C = Conn_{α}, T = Finite_{α} and, for each signalling process p_{C}, inf (ρ_{p_{C}}) ∩ G_{C} ≠ ∅. The automaton accepts α if there is a run ρ on α and a table entry τ such that ρ satisfies τ.

Recall that every process p in Finite_{α} constitutes a separate singleton component in Conn_{α}. For a signalling process p ∈ T, the set G_{p} denotes the set of possible terminating states for p. On the other hand, for a signalling process p which does not belong to T, G_{p} is a set of recurring states, one of which must be visited infinitely often by 𝔄 for ρ to satisfy τ.

Our definition of Büchi asynchronous automata is adapted from [Mus] and differs from the original formulation of Gastin and Petit [GP]. We discuss the relationship between the two definitions in Appendix A. The crucial part of our definition is the extra information we record about Conn_{α} in each entry of the acceptance table. This allows us to separate the processes in 𝔄 into independent groups. After a finite prefix of α has been read, there will be no further synchronizations between processes in different connected components of 𝒢_{α}. So, in the limit, each subset C ∈ Conn_{α} moves as a separate, independent unit.

As in the case of Büchi automata on infinite strings, non-deterministic Büchi asynchronous automata are strictly more powerful than their deterministic counterparts [GP]. So, to determinize these automata, we have to strengthen the acceptance condition. We shall work with a generalization of the “pairs” condition proposed by Rabin [Rab].

Rabin asynchronous automata A Rabin asynchronous automaton is a pair R𝔄 = (𝔄, 𝒯_{R}) where 𝔄 is an asynchronous automaton and 𝒯_{R} is a Rabin acceptance table. The table 𝒯_{R} is a list (τ_{1}, τ_{2}, …, τ_{k}). Each entry τ_{i} in 𝒯_{R} is of the form (C, T, {(p_{C}, pairs_{C})}_{C∈C}), where C, T and p_{C} are as in a Büchi acceptance table and, for each signalling process p_{C}, pairs_{C} is a list {(G_{C}^{j}, R_{C}^{j})}_{j∈[1..k_{C}]} such that for each pair (G_{C}^{j}, R_{C}^{j}), both G_{C}^{j} and R_{C}^{j} are subsets of V_{p_{C}}.

The automaton R𝔄 = (𝔄, 𝒯_{R}) accepts an input α if there is a run ρ of 𝔄 on α such that for some entry τ = (C, T, {(p_{C}, pairs_{C})}_{C∈C}) in the table 𝒯_{R}, C = Conn_{α}, T = Finite_{α} and, for each signalling process p_{C}, there is an entry (G_{C}^{j}, R_{C}^{j}) in pairs_{C} such that inf (ρ_{p_{C}})∩G_{C}^{j} ≠ ∅ and inf (ρ_{p_{C}})∩R_{C}^{j} = ∅.

The problem For a given non-deterministic Büchi asynchronous automaton B𝔄 = (𝔄, 𝒯_{B}) over (Σ, θ), construct a deterministic Rabin asynchronous automaton R𝔅 = (𝔅, 𝒯_{R}) over (Σ, θ), such that B𝔄 and R𝔅 accept the same set of infinite words over Σ.

Notice that an asynchronous automaton where 𝒫 is a singleton {p} is just a conventional sequential finite state automaton. Further, if 𝒫 = {p}, our definitions of Büchi and Rabin asynchronous automata reduce to the standard formulations of these automata in the setting of infinite strings [Tho].

For sequential Büchi automata, Safra has described an elegant determinization construction [Saf]—see Appendix B for a brief sketch of the construction. To determinize Büchi asynchronous automata, we shall apply Safra’s construction in a distributed setting. Let B𝔄 = (𝔄, 𝒯_{B}) be a Büchi asynchronous automaton. Our strategy will be to construct a deterministic Rabin automaton R𝔅_{τ} = (𝔅_{τ}, 𝒯_{R_{τ}}) corresponding to each entry τ in the table 𝒯_{B}. The automaton R𝔅_{τ} accepts an input α provided there is a run ρ of B𝔄 which satisfies τ. We can then combine the individual automata {R𝔅_{τ}}_{τ∈𝒯_{B}} into a deterministic Rabin automaton R𝔅 which accepts exactly the same infinite strings as B𝔄.

To construct the automaton R𝔅_{τ} corresponding to the table entry τ = (C, T, {(p_{C}, G_{C})}_{C∈C}), we have to check that for each signalling process p_{C}, ρ_{p_{C}} ∩ G_{C} ≠ ∅. To do this, we run Safra’s construction for each signalling process p_{C}, using the subset construction for asynchronous automata [KMS] in place of the classical subset construction for sequential automata.

The catch is that each signalling process p_{C} may meet its recurring set G_{C} infinitely often along a different run. So, we have to further ensure that the accepting runs detected by the independent copies of Safra’s construction at each signalling process are mutually consistent. This will involve some analysis of the way information is passed between the components before they branch out as independent groups.

3 Local and global views

We represent words over a distributed alphabet as labelled partial orders. The notions we use are essentially those of trace theory [Maz]. Appendix C has a few examples illustrating the ideas introduced in the next couple of sections.

Events With α : N → Σ, we associate a set of events ℰ_{α}. Each event (i, α(i)) consists of a letter α(i) together with the time i of its occurrence. 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 ℰ_{α}. 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 = (i, a), we write p ∈ e to denote that p ∈ θ(a) when e ≠ 0; 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 α naturally imposes a total order ≤ on events: e ≤ f if e happens at time i and f happens at time j with i ≤ j.

Each process p imposes a total order ≤_{p} on the events in which is participates. Thus e ≤_{p} f if p participates in both e and f and e ≤ f. If e is the p-event that immediately precedes the p-event f, then we write e ◁_{p} f. Thus e ◁_{p} f if e ≤_{p} f and no g with e < g < f is a p-event.

The asynchronous nature of the automaton is reflected more accurately by the partial order generated by the relations {◁_{p}}_{p∈𝒫} than by the temporal order ≤. We say that e is an immediate predecessor of f and write e ◁ f if e ◁_{p} f for some p. Let ⊑ be the reflexive and transitive closure of ◁. If e ⊑ f, then we say e is below f. Note that the initial event 0 is below any event. The set of events below e is denoted e↓. They represent the only synchronizations that may have affected the state of 𝔄 at e.

Ideals An ideal I is any set of events closed with respect to ⊑. Ideals represent possible partial computations of the system. We assume that every ideal I we consider is non-empty—i.e., 0 always belongs to I. Let α_{m} denote the prefix of α of length m. Then the events {(i, α(i)) | i ≤ m} ∪ {0} form an ideal. Conversely, every ideal gives rise to a subword of α—if I is the finite ideal {0, (i_{1}, a_{1}), (i_{2}, a_{2}), …, (i_{m}, a_{m})}, then α[I] : [1..m] → Σ is the word α(i_{1})α(i_{2}) ⋯ α(i_{m}) = a_{1}a_{2} ⋯ a_{m}. Similarly, we can associate infinite ideals in ℰ with infinite subsequences of α. Even when I is finite, α[I] is not, in general, a prefix of α because of the asynchronous manner in which α is processed. Clearly the entire set ℰ is an ideal, as is the set e↓ for any event e ∈ ℰ.

P -views Let I be an ideal. The p-view of I, ∂_{p}(I), is the set {e ∈ I | ∃f ∈ I. p ∈ f and e ⊑ f}. So, ∂_{p}(I) is the set of all events in I which p can “see”. If the number of p-events in I is finite—for instance, if I itself is finite—it is easy to see that ∂_{p}(I) = max_{p}(I)↓, where max_{p}(I) is the maximum p-event in I with respect to ⊑.

For P ⊆ 𝒫, the P -view of I, denoted ∂_{P} (I), is ⋃_{p∈P} ∂_{p}(I). Notice that ∂_{P} (I) is always an ideal. In particular, we have ∂_{𝒫} (I) = I.

4 Local runs and histories

For the rest of this section, we fix a (non-determinstic) asynchronous automaton 𝔄 = ({V_{p}}_{p∈𝒫} , {→_{a}}_{a∈Σ}, 𝒱_{0}).

Neighbourhoods The neighbourhood of an event e, nbd(e), consists of e together with its immediate predecessors; i.e., nbd(e) = {e} ∪ {f | f ◁ e}. Notice that if e ∈ ∂_{P} (I) for some P ⊆ 𝒫, then nbd(e) ⊆ ∂_{P} (I) as well.

Local runs A local run on an ideal I assigns a joint state to each event in I in such a way that all neighbourhoods are consistently labelled. More precisely, a local run on I is a function r that assigns to each e ∈ I an estate—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 the following sense: suppose that v⃗ is the e-state whose p-component, for each p ∈ e, is the same as the p-component of r(f_{p}), where f_{p} is the immediate p-predecessor of e. In other words, for each p ∈ e, v⃗_{p} = r(f_{p})_{p}, where f_{p} ◁_{p} e. Then r is such that v⃗ →_{e} r(e). Given a local run r, there is a natural “last” global state v⃗ defined by v⃗_{p} = r(max_{p}(I)) for all p. We say that v⃗ is a state of 𝔄 on I. Similarly, a P -state of 𝔄 on I is v⃗_{P}, where v⃗ is a state of 𝔄 on I.

Let ℛ(I) denote the set of all local runs on I. The following is easy to verify.

Proposition 1 Let α : N → Σ and I ⊆ ℰ_{α} an ideal. Then, there is a 1–1 correspondence between ℛ(I) and the set of global runs of 𝔄 on α[I].

Histories A history on an ideal I is a partial function h that assigns joint states to some events in I. Thus dom(h) ⊆ I and when h(e) is defined it denotes a tuple in V_{e}. A history is reachable if there is some local run r on I such that h(e) = r(e) for e in dom(h). A set of histories H is consistent if each pair of histories h and h′ in the set agree on all common events; i.e., for each h, h′ ∈ H, for each e in dom(h) ∩ dom(h′), h(e) = h(e′).

History Products Let I = {I_{1}, I_{2}, …, I_{n}} be a set of ideals with J = ⋃_{j∈[1..n]} I_{j}. Let {h_{1}, h_{2}, …, h_{n}} be a consistent set of histories such that h_{j} is a history over I_{j} for each j ∈ [1..n]. We define the product h = ⨂_{j∈[1..n]} h_{j} as follows:

dom(h) = {e ∈ J | for all j ∈ [1..n], if e ∈ I_{j} then e ∈ dom(h_{j})}
h(e) = h_{k}(e), where k is such that e ∈ dom(h_{k}) (the choice of k
does not matter since {h_{j}}_{j∈[1..n]} is consistent).

In other words, h is a history over J which inherits its values from the set {h_{j}}_{j∈[1..n]}. The value h(e) is defined whenever h_{j}(e) is defined for all j such that e ∈ I_{j}. This means that if e is in I_{j} ∩ I_{k} for some pair {I_{j}, I_{k}} ⊆ I and e ∈ dom(h_{j}) but e ∉ dom(h_{k}), then e ∉ dom(h).

We can extend the notion of product to sets of histories spanning a set of ideals. Let I = {I_{1}, I_{2}, …, I_{n}} be a set of ideals as before, with J = ⋃_{j∈[1..n]} I_{j}. Let ℋ_{I} = {H_{1}, H_{2}, …, H_{n}} where H_{j} is a set of histories over I_{j} for each j ∈ [1..n]. A choice from ℋ_{I} is a set {h_{j}}_{j∈[1..n]} which picks out a history h_{j} ∈ H_{j} for each j ∈ [1..n]. The choice is consistent if the set {h_{j}}_{j∈[1..n]} is. We can then define

⨂ ℋ_{I} = { ⨂_{j∈[1..n]} h_{j} | {h_{j}}_{j∈[1..n]} is a consistent choice from ℋ_{I}}.

So, ⨂ ℋ_{I} contains all histories on J that may be pieced together from mutually consistent histories in the collection ℋ_{I}.

Products of histories play a crucial role in the subset construction for asynchronous automata [KMS]. When determinizing an asynchronous automaton, it is not sufficient for each process to maintain just the subset of states it can be in after reading a part of the input. Suppose X_{p} and X_{q} are the sets of possible states of p and q on ideal I. The set of possible joint {p, q}-states on I is not, in general, the naïve product X_{p} ×X_{q}. To determine which states from X_{p} ×X_{q} are valid {p, q}-states on I, p and q have to record additional information about the runs leading to each state in the current subsets X_{p} and X_{q}. Since the amount of information that a process can store is bounded, it can at best record histories defined over a finite subset of the events it has seen.

In the subset construction of [KMS], after an ideal I, each process p maintains the set H_{p} of all reachable histories over a specific bounded subset of ∂_{p}(I). This subset includes max_{p}(I), so H_{p} has, in particular, information about all the possible states that p can be in on I. Suppose a subset P ⊆ 𝒫 synchronizes after reading a part of the input. In terms of the notation above, we have I = {∂_{p}(I)}_{p∈P}, J = ∂_{P} (I) and ℋ_{I} = {H_{p}}_{p∈P}. The goal is to ensure that ⨂ ℋ_{I} generates all possible consistent “joint” histories of P over an appropriate subset of ∂_{P} (I). This will allow the processes in P to jointly compute all the possible moves they can make on reading the new letter from the input.

The key step is to characterize when the product of a set of reachable histories {h_{j}}_{j∈[1..n]} over I = {I_{1}, I_{2}, …, I_{n}} remains a reachable history over the joint ideal J = ⋃_{j∈[1..n]} I_{j}. For this, we need the notion of a frontier.

Frontiers Let I and J be ideals and p a process. We say that event e of I is an p-sentry for I relative to J if e is also in J and its p-successor is in J but not in I. Thus the process p “leaves” I at e. Let border(I, J) be the set of all such sentries. Note that there is at most one p-sentry for each p, so there are at most N events in border(I, J)—recall that N = |𝒫|. In general, border(I, J) ≠ border(J, I). We are normally interested in the two sets together, which we denote frontier(I, J); i.e., frontier(I, J) = border(I, J) ∪ border(J, I). It is clear that frontier(I, J) = frontier(J, I) and frontier(I, I) = ∅. We then have the following crucial result which is proved in [KMS].

Lemma 2 Let I = {I_{1}, I_{2}, …, I_{n}} be a set of ideals and {h_{j}}_{j∈[1..n]} a consistent set of histories such that for each j ∈ [1..n]:

(i) h_{j} is a reachable history over I_{j}; and

(ii) dom(h_{j}) includes ⋃_{k∈[1..n]} frontier(I_{j}, I_{k}).

Then h = ⨂_{j∈[1..n]} h_{j} is a reachable history over J = ⋃_{j∈[1..n]} I_{j}.

So, whenever the reachable histories {h_{j}}_{j∈[1..n]} span all the frontiers between the ideals in I = {I_{1}, I_{2}, …, I_{n}}, their product is also reachable.

Recall that each process p maintains H_{p}, the set of all reachable histories over a specific subset of ∂_{p}(I). Suppose that this specific subset of ∂_{p}(I) includes frontier_{p}(I), where

frontier_{p}(I) = ⋃_{q∈𝒫} frontier(∂_{p}(I), ∂_{q}(I)).

Then, if I = {∂_{p}(I)}_{p∈P} and ℋ_{I} = {H_{p}}_{p∈P}, the previous lemma guarantees that every history in ⨂ ℋ_{I} is reachable in ∂_{P} (I).

The problem now is for a process p to compute the bounded set of events frontier_{p}(I). This can be done using slightly larger, but still bounded, sets of events called primary and secondary information, which between them subsume the frontiers.

5 Primary and secondary information

Primary information Let I be a finite ideal. Recall that max_{p}(I) denotes the ⊑-maximum p-event in I. The primary information of I, primary(I), is the set of events {max_{p}(I)}_{p∈𝒫}. We can define primary(I) analogously for infinite ideals as well, where we include the events max_{p}(I) for only those processes p such that there are only finitely many p-events in I.

Secondary and tertiary information Let I be a finite ideal. The secondary information in I, secondary(I), is the set of events ⋃_{p∈𝒫} primary(∂_{p}(I)). The tertiary information in I, tertiary(I), is the set of events ⋃_{p,q∈𝒫} primary(∂_{p}(∂_{q}(I))).

The primary information of I represents the latest information available in I about each process in the system. Similarly, the secondary information primary(∂_{p}(I)) is the latest information that process p has in I about the other processes in the system, while the tertiary information primary(∂_{q}(∂_{p}(I))) is the latest information that p has about the primary information of q in I.

It is clear that every event in primary(I) also belongs to secondary(I), since max_{p}(∂_{p}(I)) = max_{p}(I) for all p ∈ P. Similarly, every event in secondary(I) belongs to tertiary(I). (Actually, primary(I), secondary(I) and tertiary(I) are indexed sets of events—an event e ∈ I may be both max_{p}(I) and max_{q}(I) for different processes p and q and must hence be represented twice in primary(I), say as the pairs (e, p) and (e, q). However, we shall normally ignore this aspect and just treat all these indexed collections as sets of events.)

Let I and J be ideals. If I and J satisfy a simple condition, the events in frontier(I, J) can be characterized in terms of the primary and secondary information of I and J, as described in the following lemma. (A proof of the lemma can be found in [KMS].)

Lemma 3 Let I and J be ideals such that I = ∂_{P} (K) and J = ∂_{Q}(K), where K is an ideal and P, Q ⊆ 𝒫 are sets of processes. Let e be a p-sentry for I with respect to J. Then e = max_{p}(I) and, for some process q, e = max_{p}(∂_{q}(J)). Thus, e ∈ primary(I) ∩ secondary(J).

Let I be an ideal. From the previous lemma, it is clear that for a process P to maintain reachable histories over frontier_{p}(I), it is sufficient for p to maintain reachable histories over secondary(∂_{p}(I)). Processes can unambiguously keep track of their primary and secondary information by using time-stamps.

Time-stamps and the subset construction

Let I be a finite ideal. Then, there are at most N^{3} distinct events in tertiary(I). We can thus use a finite set ℒ of labels to time-stamp each event in this set. We can denote the assignment of time-stamps to the events in tertiary(I) as a function λ : tertiary(I) → ℒ. For p ∈ 𝒫, let λ_{p} denote the restriction of λ to ∂_{p}(I). It turns out that the processes in 𝒫 can locally maintain and update the functions λ_{p} so that, overall, the events in tertiary(I) are assigned consistent time-stamps.

Theorem 4 (Time-stamping [MS]) For any distributed alphabet (Σ, θ), we can fix a finite set of labels ℒ and construct a deterministic asynchronous automaton 𝔄_{T} over (Σ, θ) in which, on any finite ideal I, each process p maintains λ_{p} : secondary(∂_{p}(I)) → ℒ, where λ_{p} is the restriction to ∂_{p}(I) of a consistent labelling λ : tertiary(I) → ℒ. Process p maintains λ_{p} as a function from 𝒫× 𝒫 to ℒ. The value λ_{p}(q, r) is the label assigned to the event max_{r}(max_{q}(∂_{p}(I))).

The automaton 𝔄_{T} allows each process to maintain reachable histories over the set secondary(∂_{p}(I))—each history h is maintained as a partial function assigning joint states to labels in ℒ such that whenever λ(e) = ℓ for some event e ∈ secondary(∂_{p}(I)), h(ℓ) is defined and yields an e-state. In conjunction with Lemmas 2 and 3, this yields the following result.

Theorem 5 (Subset construction [KMS]) Let 𝔄 be a non-deterministic asynchronous automaton over (Σ, θ). Then, we can construct a deterministic asynchronous automaton 𝔄_{S} over (Σ, θ) such that for any finite ideal I, the unique global state v⃗ reached by 𝔄_{S} on I has the following properties:

(i) For each process p, v⃗_{p} contains H_{p}, the set of all reachable histories over secondary(∂_{p}(I)).

(ii) For any subset P of 𝒫, we can compute the set of all possible P -states of 𝔄 on I from the information in the P -state v⃗_{P}. In particular, from v⃗ we can recover the set of possible global states of 𝔄 on I.

6 Determinizing Büchi asynchronous automata

We now have enough machinery at hand to apply Safra’s construction in a distributed setting. Recall that we are initially given a non-deterministic Büchi asynchronous automaton B𝔄 = (𝔄, 𝒯_{B}). Our goal is to construct a deterministic Rabin asynchronous automaton R𝔅 = (𝔅, 𝒯_{R}) which accepts the same set of infinite strings that B𝔄 does.

As we remarked earlier, our strategy is to construct a separate deterministic Rabin automaton R𝔅_{τ} = (𝔅_{τ}, 𝒯_{R_{τ}}) for each entry τ in the Büchi table 𝒯_{B} such that R𝔅_{τ} accepts an input α iff there is a run ρ of B𝔄 on α which satisfies τ. We shall then combine these individual automata {R𝔅_{τ}}_{τ∈𝒯_{B}} into a single automaton R𝔅 which accepts the same inputs as B𝔄.

Let τ = (C, T, {(p_{C}, G_{C})}_{C∈C}) be an entry from 𝒯_{B}. We first describe how to construct the corresponding Rabin automaton R𝔅_{τ}. For simplicity, we assume that T = ∅—i.e., a run ρ of B𝔄 on an input α can satisfy τ only if Finite_{α} = ∅. In other words, every process moves infinitely often as 𝔄 reads α. Later, we shall see how to eliminate this “progress” assumption.

The automaton R𝔅_{τ} has to check that there is a run ρ of 𝔄 on α such that along ρ, each signalling process p_{C} visits some recurring state from G_{C} infinitely often. Each process p_{C} can detect whether there is some local run r_{C} of 𝔄 on α which meets G_{C} infinitely often by running Safra’s construction locally. However, we have to check that the individual runs {r_{C}}_{C∈C} are mutually consistent.

Let I_{α} = {I_{C}}_{C∈Conn_{α}} be the set of ideals such that I_{C} = ∂_{C}(ℰ) for each C ∈ Conn_{α}. (Recall that each set C is a subset of 𝒫, so the C-view of ℰ is well-defined.) If there is a run of 𝔄 satisfying τ, it must be the case that C = Conn_{α}, so we can alternatively regard I_{α} as the collection {∂_{C}(ℰ)}_{C∈C}.

Let I_{α}^{joint} denote the set of events which occur in more than one ideal in the collection I_{α}—i.e., I_{α}^{joint} = {e ∈ ℰ | ∃C, C′ ∈ C. C ≠ C′ and e ∈ I_{C} ∩I_{C′}}. Since C = Conn_{α}, it must be the case that I_{α}^{joint} is finite—“above” I_{α}^{joint}, the ideals in I_{α} are pairwise disjoint. Moreover, the union ∪I_{α} is the entire set ℰ. So, if we can ensure that the local runs {r_{C}}_{C∈C} agree on the events in I_{α}^{joint}, they can be “pasted” together to form a global run ρ of 𝔄 satisfying τ.

Actually, it is not necessary that the local runs {r_{C}}_{C∈C} agree on the entire set I_{α}^{joint} in order to synthesize a global run ρ satisfying τ. It is sufficient for these local runs to agree along the frontiers of the ideals in I_{α}.

Lemma 6 Let α : N → Σ be an infinite word. For I_{C} ∈ I_{α}, let frontier(I_{C}, I_{α}) denote the set of events spanning the frontiers of I_{C} with respect to all the ideals in I_{α}—i.e., frontier(I_{C}, I_{α}) = ⋃_{C′∈C} frontier(I_{C}, I_{C′}).

Let ℛ = {r_{C}}_{C∈C} be a set of local runs of 𝔄 on α such that:

(i) For C ∈ C, r_{C} is a local run over I_{C}.

(ii) For each pair C, C′ ∈ C, the local runs r_{C} and r_{C′} agree on frontier(I_{C}, I_{C′}).

Then, there is a local run r of 𝔄 over ℰ which agrees with each run r_{C} ∈ ℛ for all events e ∈ I_{C} “above” frontier(I_{C}, I_{α}). In other words, for each C ∈ C, for each e ∈ I_{C}, if there exists f ∈ frontier(I_{C}, I_{α}) such that f ⊑ e, then r(e) = r_{C}(e).

Proof For C ∈ C, let h_{C} be the history generated by restricting r_{C} to the set {e ∈ I_{C} | ∃f ∈ frontier(I_{C}, I_{α}). f ⊑ e}. It is easy to check that the histories in {h_{C}}_{C∈C} satisfy the assumptions of Lemma 2. So h = ⨂_{C∈C} h_{C} is a reachable history over ∪I_{α} = ℰ. Let r be the local run extending h to all of ℰ. □

So, if the local runs {r_{C}}_{C∈C} detected by the copies of Safra’s construction agree along the frontiers in I_{α}, we can synthesize a local run r over ℰ which agrees with each local run r_{C} outside I_{α}^{joint}. It is clear that the global run ρ of 𝔄 on α which corresponds to r does in fact satisfy τ. Of course, to check the conditions of the previous lemma, we have to verify that, in the limit, the local runs detected by each signalling process agree on the frontier events. In principle, this involves an infinite amount of computation. However, since there is only a finite amount of communication across the ideals in I_{α}, the frontier events of interest get “frozen” at some finite stage.

Lemma 7 Let α : N → Σ be an infinite word. Let J be an ideal such that I_{α}^{joint} ⊆ J ⊆ ℰ. Then, for each pair {C, C′} in Conn_{α},

frontier(∂_{C}(J), ∂_{C′}(J)) = frontier(∂_{C}(ℰ), ∂_{C′}(ℰ)).

Proof Observe that for every J such that I_{α}^{joint} ⊆ J, and for every pair {C, C′} in Conn_{α}, ∂_{C}(J) ∩ ∂_{C′}(J) = ∂_{C}(ℰ) ∩ ∂_{C′}(ℰ). The result then follows.

□

Let α be an infinite word and C, C′ be components in Conn_{α}. From Lemma 3, we know that the events in frontier(∂_{C}(ℰ), ∂_{C′}(ℰ)) are contained in secondary(∂_{C}(ℰ)) and secondary(∂_{C′}(ℰ)).

Let p_{C} and p_{C′} be processes in C and C′ respectively. From the definition of Conn_{α}, it follows that ∂_{C}(ℰ) = ∂_{p_{C}} (ℰ) and ∂_{C′}(ℰ) = ∂_{p_{C′}} (ℰ). So, frontier(∂_{C}(ℰ), ∂_{C′}(ℰ)) is, in fact, contained in the secondary information of both ∂_{p_{C}} (ℰ) and ∂_{p_{C′}} (ℰ).

Let e ∈ secondary(∂_{p_{C}} (ℰ)). From the definition of secondary information, e = max_{r}(∂_{q}(∂_{p_{C}} (ℰ))) for some pair of processes q and r. In other words, there are only finitely many r-events in ∂_{q}(∂_{p_{C}} (ℰ)). There are two possibilities:

• The ideal ∂_{q}(∂_{p_{C}} (ℰ)) is itself finite, in which case q ∈ (𝒫 − C).

• The ideal ∂_{q}(∂_{p_{C}} (ℰ)) is infinite, but the number of r-events in ∂_{q}(∂_{p_{C}} (ℰ)) is finite. This means that q ∈ C but r ∈ (𝒫 − C).

This observation prompts the following definition:

Stable information Let α : N → Σ be an infinite word and let p_{C} ∈ C for some connected component C ∈ Conn_{α}. For any ideal I, the stable information of p_{C} in I, stable-info_{p_{C}} (I) is the subset of secondary(∂_{p_{C}} (I)) given by

{max_{r}(∂_{q}(∂_{p_{C}} (I))) | q ∉ C, r ∈ 𝒫} ∪ {max_{r}(∂_{q}(∂_{p_{C}} (I))) | q ∈ C, r ∉ C}.

The events in stable-info_{p}(I) are frozen once I grows beyond the finite initial portion I_{α}^{joint} in ℰ. In other words, for any ideal J ⊇ I_{α}^{joint}, stable-info_{p_{C}} (J) = stable-info_{p_{C}} (ℰ). By our earlier observations, this means that for any J ⊇ I_{α}^{joint}, stable-info_{p_{C}} (J) subsumes the events lying in the sets ⋃_{C′∈Conn_{α}} frontier(∂_{C}(ℰ), ∂_{C′}(ℰ)).

Let us get back to our distributed version of Safra’s construction corresponding to an entry τ = (C, T, {(p_{C}, G_{C})}_{C∈C}) in 𝒯_{B}. Suppose that each signalling process p_{C} ensures that it has crossed the finite portion I_{α}^{joint} before starting Safra’s construction. Then, along with each successful run r_{C} on ∂_{C}(ℰ) that it detects, it can record the value of r_{C} on stable-info_{p_{C}} (ℰ). If the successful runs {r_{C}}_{C∈C} agree on the stable information across all the signalling processes, we know that the runs satisfy the assumption of Lemma 6, which means that there is some global run of 𝔄 on α which satisfies τ.

The catch is that the signalling processes have no way of knowing when the finite portion I_{α}^{joint} is over. However, since 𝔅_{τ} includes the subset automaton for 𝔄, 𝔅_{τ} also incorporates the time-stamping automaton 𝔄_{T} which maintains consistent labels across tertiary(I) at the end of any ideal I. If the time-stamps assigned by 𝔄_{T} to the events in stable-info_{p_{C}} (I) change, the process p_{C} knows that I_{α}^{joint} is not yet over.

So, we adopt the following strategy. Initially, each signalling process p_{C} starts off Safra’s construction. Whenever it detects that stable-info_{p_{C}} (I) has changed, it “kills” the old copy of Safra’s construction and restarts a new copy. In fact, the process starts a separate copy of Safra’s construction for each distinct history over stable-info_{p_{C}} (I). So, in the limit, p_{C} can signal whether or not there is an accepting local run r_{C} for each history over its stable information.

The structure of R𝔅_{τ}

Let τ = (C, T, {(p_{C}, G_{C})}_{C∈C}). The local state of each signalling process p_{C} in 𝔅_{τ} consists of the following information:

(i) The local state of the subset automaton for 𝔄. This includes the set H_{p_{C}} of all reachable histories over secondary(∂_{p_{C}} (I)) at the end of any input ideal I.

This component incorporates the local state of the time-stamping automaton 𝔄_{T}, which stores the labels of events in secondary(∂_{p_{C}} (I)) as a function λ_{p_{C}} : 𝒫 × 𝒫 → ℒ. The time-stamps assigned to the events in stable-info_{p_{C}} (I) are the values λ_{p}(q, r) where either q ∉ C or (q ∈ C and r ∉ C).

(ii) Let H_{S} be the set of reachable histories over stable-info_{p_{C}} (I). For each h ∈ H_{S}, p_{C} maintains an independent labelled coloured tree as dictated by Safra’s construction.

The non-signalling processes need not run Safra’s construction; it is sufficient for them to maintain the first component of the state, corresponding to the subset automaton.

On reading an input letter a, each process p in θ(a) updates its local states as follows:

(i) First p updates the local state components corresponding to the timestamping automaton and the subset automaton.

(ii) If p is a signalling process and if the time-stamps assigned to stable-info_{p}(I) have not changed, then p updates the trees in each copy of Safra’s construction using the new information provided by the subset automaton.

On the other hand, if the time-stamp corresponding to any event in stable-info_{p}(I) changes, p erases all the existing copies of Safra’s construction and begins a fresh copy for each history in the new set H_{S}.

The single entry τ in 𝒯_{B} generates a table 𝒯_{R_{τ}} in R𝔅_{τ} with multiple entries. Each possible history h over ⋃_{C∈C} stable-info_{p_{C}} (ℰ) generates a distinct entry τ_{h} of the form (C, T, {(p_{C}, pairs_{C})}_{C∈C}) in 𝒯_{R_{τ}}. In τ_{h}, the entries C, T and the set of signalling processes {p_{C}}_{C∈C} are as in the original entry τ ∈ 𝒯_{B}.

Let |V_{p_{C}} | = M_{C} be the number of possible local states for p_{C} in 𝔄. Then, there are 2M_{C} possible pairs (G_{C}^{j}, R_{C}^{j}) in the list pairs_{C}, corresponding to the labels {ℓ_{1}, ℓ_{2}, …, ℓ_{2M_{C}}} used by Safra’s construction to label the nodes in the tree associated with the current subset of possible p_{C} states.

The set G_{C}^{j} consists of all possible states of p_{C} in which the set of histories over stable-info_{p_{C}} (ℰ) includes the projection h_{p_{C}} of h onto stable-info_{p_{C}} (ℰ) and, moreover, in the labelled tree from Safra’s construction corresponding to h_{p_{C}}, the node labelled ℓ_{j} is coloured green.

The set R_{C}^{j} consists of all possible states of p_{C} in which the set of histories over stable-info_{p_{C}} (ℰ) includes the projection h_{p_{C}} of h onto stable-info_{p_{C}} (ℰ) and, moreover, in the labelled tree from Safra’s construction corresponding to h_{p_{C}}, there is no node labelled ℓ_{j}.

It is straightforward though tedious to verify that R𝔅_{τ} accepts an input α : N → Σ iff there is a run of B𝔄 on α satisfying τ.

Removing the progress assumption So far we have assumed that T = ∅ in the Büchi table entry τ. Suppose T ≠ ∅ and there is a run of 𝔄 on α which satisfies τ. Then each process p ∈ T moves only finitely often while 𝔄 reads α. So, we just run the subset construction for p and verify that it terminates in one of the states in G_{p}.

In other words, for each entry τ_{h} of R𝔅_{τ}, we have a single pair (G_{p}^{1}, R_{p}^{1}) in pairs_{{p}}, where R_{p}^{1} = ∅ and G_{p}^{1} consists of all possible states of the subset automaton such that there is a history h′ in H_{p} which agrees with h on stable-info_{p}(ℰ) where the terminal state assigned to p by h′ belongs to G_{p}.

Combining the individual automata {R𝔅_{τ}}_{τ∈𝒯_{B}} We can combine the individual automata {R𝔅_{τ}}_{τ∈𝒯_{B}} using a standard product construction which preserves determinacy. The construction is essentially the same as in the sequential case and we omit the details.

A complementation construction We can complement a Rabin asynchronous automaton by viewing the acceptance table as a Streett condition, as in sequential automata [Tho]. This Streett condition can then be checked efficiently by a non-deterministic Büchi asynchronous automaton using the technique proposed by Vardi (described in [Saf]). So, from R𝔅 we can construct an Büchi automaton B\overline{𝔄} such that B\overline{𝔄} accepts an infinite string α iff R𝔅 does not accept α. Since R𝔅 accepts the same inputs that B𝔄 does, B\overline{𝔄} is a complement automaton for B𝔄. See Appendix D for details of how to construct B\overline{𝔄}.

Complexity analysis In the input automaton B𝔄 = (𝔄, 𝒯_{B}), let N be the number of processes in 𝔄, M the size of the largest set in the collection {V_{p}}_{p∈𝒫} and K the number of entries in 𝒯_{B}.

Then, in the deterministic Rabin automaton R𝔅 which we construct, the number of local states of each process p is bounded by 2^{KM^{O(N^{3})}}, while in the complement automaton B\overline{𝔄}, the number of local states of each process p is bounded by 2^{K^{2}M^{O(N^{4})}}. Details of how these bounds are derived can be found in Appendix E.

In [KMS], it is shown that in the subset automaton for 𝔄, the number of states of each process p is bounded by 2^{M^{O(N^{3})}}. So, the blow-up involved in the construction of R𝔅 and B\overline{𝔄} is essentially the same as that of the subset construction.

Consolidating the results of this section, we have the main result of this paper.

Theorem 8 Let B𝔄 = (𝔄, 𝒯_{B}) be a non-deterministic Büchi asynchronous automaton over (Σ, θ). Then, we can construct a deterministic Rabin asynchronous automaton R𝔅 = (𝔅, 𝒯_{R}) over (Σ, θ) such that R𝔅 accepts the same set of infinite strings that B𝔄 does. From R𝔅, we can construct a complementary non-deterministic Büchi automaton B\overline{𝔄} over (Σ, θ) which accepts an infinite string α iff the original automaton B\overline{𝔄} does not accept α.

The number of local states of each process in R𝔅 and B\overline{𝔄} is essentially exponential in the number of global states of the original automaton B𝔄.

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, Acta Inf., 31 (1994) 379–397.

[EM] W. Ebinger, A. Muscholl: Logical definability on infinite traces, Proc. ICALP ’93, LNCS 700 (1993) 335–346.

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

[HJJ] J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, A. Sandholm: Mona: Monadic Secondorder logic in practice, Report RS-95-21, BRICS, Department of Computer Science, Aarhus University, Aarhus, Denmark (1995).

[Kla] N. Klarlund: Progress measures for complementation of ωautomata with applications to temporal logic, Proc. 32nd IEEE FOCS, (1991) 358–367.

[KMS] N. Klarlund, M. Mukund, M. Sohoni: Determinizing asynchronous automata, Proc. ICALP ’94, LNCS 820 (1994) 130–141.

[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 time-stamps suffice”, Proc. FST&TCS ’93, LNCS 761 (1993) 388–399.

[Mus] A. Muscholl: On the complementation of Büchi asynchronous cellular automata, Proc. ICALP ’94, LNCS 820 (1994) 142–153.

[Nie] P. Niebert: A μ-calculus with local views for systems of sequential agents, Proc. MFCS ’95, to appear.

[Rab] M.O. Rabin: Decidability of second order theories and automata on infinite trees, Trans. AMS, 141(1969) 1–37.

[Saf] S. Safra: On the complexity of ω-automata, Proc. 29th IEEE FOCS, (1988) 319–327.

[Thi] P.S. Thiagarajan: TrPTL: A trace based extension of linear time temporal logic, Proc. 9th IEEE LICS, (1994) 438–447.

[Tho] W. Thomas: Automata on infinite objects, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, North-Holland, Amsterdam (1990) 133–191.

[VW] M. Vardi, P. Wolper: An automata theoretic approach to automatic program verification, P. 1st IEEE LICS, (1986) 332–345.

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

A Comparison with Gastin-Petit automata

The original formulation of Büchi asynchronous automata by Gastin and Petit [GP] differs from the one we use in this paper. In the original definition, information about Conn_{α} and Finite_{α} is not part of the acceptance condition. Instead, in the acceptance table, each entry is a tuple of the form {G_{p}}_{p∈𝒫}. A run ρ is accepting if there is some table entry {G_{p}}_{p∈𝒫} such that inf (ρ_{p}) ⊇ G_{p} for each process p. It is not difficult to verify that our automata are equivalent to those of Gastin and Petit.

Notice that the Gastin-Petit acceptance table uses a “covering” condition on the sets G_{p}, rather than the simple recurring set condition we have in our automata. This covering condition is awkward to work with when trying to determinize these automata.

Actually, to eliminate the “covering” condition it is sufficient to record information about Finite_{α} in the acceptance table [Nie]. The extra information we record about Conn_{α} allows us to separate the processes in 𝔄 into independent groups. After a finite prefix of α has been read, there will be no further synchronizations between processes in different connected components of 𝒢_{α}. So, in the limit, each subset C ∈ Conn_{α} moves as a separate unit, independent of the others.

From Gastin-Petit automata to our automata …

We can use our automata to simulate Büchi automata with Gastin-Petit acceptance tables as follows. On reading an input α, the simulating automaton guesses a partition C of 𝒫 corresponding to Conn_{α} together with a set of processes T corresponding to Finite_{α}. It also guesses a table entry τ = {G_{p}}_{p∈𝒫} from the Gastin-Petit table. It then generates a run ρ of the original automaton on the input α and checks if ρ satisfies τ.

To do this, we fix a signalling process p_{C} ∈ C for each component C ∈ C. The process p_{C} has to verify that every other process p′ ∈ C meets every state in G_{p′} infinitely often along the run being simulated. This can be achieved by organizing the processes in C in a spanning tree rooted at p_{C}, where the edges in the tree come from the graph 𝒢_{α}.

Each process p_{ℓ} corresponding to a leaf in this spanning tree can check that it meets G_{p_{ℓ}} infinitely often using a simple counter. Each time p_{ℓ} cycles through G_{p_{ℓ}} completely, it informs its parent in the tree—if C = Conn_{α}, p_{ℓ} will synchronize infinitely often with its parent and so will pass on this signal infinitely often.

Each internal process p_{i} in the tree maintains two counters: one for itself and one correponding to its children. The first counter checks that p_{i} cycles through G_{p_{i}} infinitely often. The second counter checks that all the children report success infinitely often. Each time both counters complete a cycle, p_{i} informs its parent in the tree.

Eventually, all the information propagating up the tree reaches the root, which is the signalling process p_{C}. So, p_{C} can use a simple recurring Büchi condition to check that all the processes in C meet their “covering” Büchi condition corresponding to the table entry τ.

The blow-up in this simulation corresponds to guessing a partition C, a set T and a table entry τ. The number of choices of C is bounded by 2^{N^{2}}, where N is the number of processes—each choice of C corresponds to dropping some edges from the complete graph on N vertices, which has N^{2} edges. The number of choices for T is bounded by 2^{N}, while the choice of τ depends on K, the number of entries in the original table. Thus, overall the blow-up is O(K2^{N^{2}}).

(Actually, we can do better. The connectivity we begin with does not correspond, in general, to the complete graph on N vertices. The alphabet (Σ, θ) restricts the communication pattern in the system. So, the number of different ways of partitioning the processes in 𝒫 is actually bounded by 2^{|E|}, where E is the number of edges in the “connectivity graph” induced by (Σ, θ). The overall blow-up is then O(K2^{|E|}).)

… and back

The simulation in the other direction is as follows. Let B𝔄 = (𝔄, 𝒯_{B}) be one of our Büchi asynchronous automata. At the initial state, the simulating automaton guesses an entry τ = (C, T, {(p_{C}, G_{C})}_{C∈C}) in 𝒯_{B} and sees if B𝔄 has a run on the input which satisfies τ.

The simulating automaton has to check the following:

• While reading the input, each process in T must move only finitely often, while each process outside T must move infinitely often.

• Each component C ∈ C must actually constitute a connected component in the limit graph of the input.

• For each component C ∈ C, the signalling process p_{C} must visit G_{C} infinitely often along the run.

The first condition can be checked by tagging the state space of each process with a two element counter.

For processes in T, one of the counter values denotes that it is “live” and the other that it is “dead”—in other words, that it will not make any further moves. There are no transitions enabled from the “dead” part of the state space. The simulating automaton non-deterministically sends each terminated process into a dead state when it feels that it has finished its finite quota of moves over a particular input.

For processes not in T, the simulating automaton ensures that with each move, the process switches between the counter values. So, the simulating automaton can record whether or not a process moves infinitely often in the original automaton by checking that it visits both copies of the state space infinitely often. Notice that to check this, the simulating automaton must use a covering Büchi condition—in general, a simple recurring Büchi condition will not suffice.

To check the second condition, the simulating automaton keeps track of when the gossip information of each process changes. Let p belong to a component C ∈ C. Then, while reading the input, p’s primary information about other processes in C must change infinitely often, while p’s primary information about processes outside C becomes frozen at some stage. So, p non-deterministically guesses when the primary information of all processes outside C is frozen. After this, if p ever has to update it primary information for some q outside C, it moves into a reject state.

After making this guess, p uses a counter to cycle through the processes in C, waiting for its primary information about each process to change. When it completes each cycle, it goes into a “good” state.

It is easy to verify that C is a connected component of the limit graph iff p does not go into its reject state and, in addition, p visits its “good” state infinitely often.

Finally, each signalling process p_{C} can easily check on the side that it visits some state from G_{C} infinitely often.

The blow-up in the state space is linear in the size of 𝒯_{B}—each entry of the table generates a copy of the original state space together with at most two counters, one of size two and one whose size is bounded by N, the number of processes in the system. However, the number of entries in the new table could be exponential in the size of 𝒯_{B} since recurring Büchi conditions in the original automaton have to be encoded in terms of covering Büchi conditions in the simulating automaton.

B Safra’s construction

Let BA be a non-deterministic sequential Büchi automaton with n states and a set G of recurring states. Safra constructs a deterministic sequential Rabin automaton RA with a table {(G_{j}, R_{j})}_{j∈[1..2n]} such that RA accepts an input α iff there is some run of BA passing through G infinitely often.

Safra uses the classical subset construction of Rabin and Scott to record the possible states that BA can be in after reading any finite prefix of α. The subset of possible states is maintained as a labelled tree—the elements of the subset are in 1–1 correspondence with the nodes of the tree and each node has a distinct label drawn from a set of names of size 2n. In addition, each node of the tree is coloured either white or green.

After reading a letter from the input, the subset construction updates the set of possible current states of BA. As a result, the shape of the corresponding tree changes. In the process some nodes are discarded from the tree and some new nodes are added. However, Safra’s construction ensures that the labels associated with the old nodes are not reused in the same step for the new nodes. In other words, if a node is dropped at some stage from the tree,

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

Figure 1: An example

its label temporarily disappears from the tree.

These labelled trees are used to keep track of runs in the underlying computation. The colours white and green are used to signal when a run of BA visits the recurring states G. Thus, when updating the trees, the colours of the nodes may also change. When a node is added to the tree, it is assigned the colour white. During its “lifetime” in the tree, it may periodically change colour from white to green and back to white again.

Recall that nodes are labelled using a set of names {ℓ_{1}, ℓ_{2}, …, ℓ_{2n}} of size 2n. Let us look at the entry (G_{j}, R_{j}) in the table for RA. Condition R_{j} says that the label ℓ_{j} disappears from the tree only finitely often. In other words, a node with label ℓ_{j} is added to the tree at some point and this node is never deleted during the rest of the run of RA. Condition G_{j} then guarantees that this node turns green infinitely often.

C Examples

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 ℰ_{α} is then {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}, e_{7}, e_{8}, …} = {0, (1, b), (2, a), (3, c), (4, b), (5, a), (6, c), (7, d), (8, d), …}.

Figure 1 describes (ℰ_{α}, ⊑). 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.

Ideals and views 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}}.

In this example, ∂_{r}(ℰ) = max_{r}(ℰ)↓= e_{6}↓= {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{6}}. On the other hand, ∂_{p}(ℰ) = {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{7}, e_{8} …} = ℰ − {e_{6}}. Notice that max_{p}(ℰ) is undefined.

Neighbourhoods The neighbourhood of e_{5}, nbd(e_{5}), is {e_{2}, e_{4}, e_{5}}.

Let 𝔄 = ({V_{p}}_{p∈𝒫} , {→_{a}}_{a∈Σ}, 𝒱_{0}) be an asynchronous automaton over (Σ, θ). 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}⟩}.

Local runs Let I be the ideal {e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}, e_{7}}. Then, the local runs corresponding to the only two possible global runs of 𝔄 on I 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.

Histories and products For p, let h_{p}^{1} and h_{p}^{2} be two histories over ∂_{p}(I) 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 over ∂_{s}(I) 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. The product ⨂ {{h_{p}^{1}, h_{p}^{2}}, {h_{s}^{1}, h_{s}^{2}}} generates four possible runs over ∂_{{p,s}}(I). However, only two of these runs are reachable—those generated by h_{p}^{1} ⊗ h_{s}^{1} and h_{p}^{2} ⊗ h_{s}^{2}. The “bad” entry h_{p}^{2} ⊗ h_{s}^{1} implies that ⟨4_{p}, 3_{q}, 1_{r}, 1_{s}⟩ is a valid global state of 𝔄 after I, which is not the case.

[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}]

Figure 2: Local runs

D Streett asynchronous automata and complementation

Let R𝔄 = (𝔄, 𝒯_{R}) be a Rabin asynchronous automaton. Then, it is easy to verify that R𝔄 does not accept an input α iff for every run ρ of 𝔄 on α and for every entry τ = (C, T, {(p_{C}, pairs_{C})}_{C∈C}) in 𝒯R, the following holds:

If C = Conn_{α} and T = Finite_{α} then ∃C ∈ C. ∀i ∈ [1..k_{C}]. (inf_{p_{C}} (ρ) ∩ G_{p_{C}} ≠ ∅) ⇒ (inf_{p_{C}} (ρ) ∩ R_{p_{C}} ≠ ∅).

This corresponds to a “complemented pairs” condition, first investigated by Streett in the setting of automata over infinite strings [Tho].

So, we can formally define a Streett asynchronous automaton as a pair S𝔄 = (𝔄, 𝒯_{S}) where the table 𝒯_{S} has the same structure as a Rabin table— i.e., each entry τ in 𝒯_{S} is of the form (C, T, {(p_{C}, pairs_{C})}_{C∈C}).

A run ρ of 𝔄 on α satisfies τ provided it meets the condition described above. The automaton 𝔄 accepts α if there is a run ρ on α which satisfies every table entry in 𝒯_{S}.

(Actually, due to the extra quantification over the partitions in C, this definition of a Streett asynchronous automaton is perhaps not the natural one. A more intuitive condition for a run ρ over α to satisfy a table entry τ = (C, T, {(p_{C}, pairs_{C})}_{C∈C}) is to stipulate that the following holds:

If C = Conn_{α} and T = Finite_{α} then ∀C ∈ C. ∀i ∈ [1..k_{C}]. (inf_{p_{C}} (ρ) ∩ G_{p_{C}} ≠ ∅) ⇒ (inf_{p_{C}} (ρ) ∩ R_{p_{C}} ≠ ∅).

This definition is not complementary to that of Rabin acceptance in our setting. Since our primary goal is to complement the given Rabin automaton, we shall stick to our “unnatural” definition of a Streett automaton.)

To complement Büchi asynchronous automata using our determinization construction, it suffices to be able to simulate a deterministic Streett asynchronous automaton by a Büchi asynchronous automaton. Starting with a non-deterministic Büchi asynchronous automaton B𝔄 = (𝔄, 𝒯_{B}), determinization produces an equivalent Rabin asynchronous automaton R𝔅 = (𝔅, 𝒯_{R}). Since R𝔅 is deterministic, if we interpret 𝒯_{R} as a Streett table 𝒯_{S}, we get a deterministic Streett automaton S𝔅 = (𝔅, 𝒯_{S}) which is complementary to B𝔄. We can then simulate S𝔅 using a non-deterministic Büchi asynchronous automaton to obtain the complementary automaton B\overline{𝔄} which we set out to construct.

To simulate a deterministic Streett asynchronous automaton S𝔄 by a non-deterministic Büchi asynchronous automata B𝔅, we proceed as follows:

(i) The simulating automaton should accept an input α if there is no entry τ = (C, T, {(p_{C}, pairs_{C})}_{C∈C}) for which C = Conn_{α} and T = Finite_{α}. This can be achieved using an automaton which has just one state for each process along with one table entry for each pair (C, T) which does not occur in the table for S𝔄. In all these new table entries, the Büchi condition for each process is the trivial one.

(ii) If the first case does not hold, let X_{α} = {τ_{1}, τ_{2}, …, τ_{m}} be the set of all entries in 𝒯_{S} such that each entry τ_{i} ∈ X_{α} is of the form (C, T, {(p_{C}, pairs_{C})}_{C∈C}) where C = Conn_{α} and T = Finite_{α}.

In [Saf], Safra describes an elegant construction due to Vardi for simulating a (sequential) Streett automaton by a (sequential) Büchi automaton. For each entry τ_{i} ∈ X_{α}, we construct a Büchi asynchronous automaton B𝔅_{i} in which each signalling process p_{C} runs Vardi’s construction to check if the (unique) run of the original automaton on α satisfies all the complemented pairs {(G_{C}^{j}, R_{C}^{j})}_{j∈[1..k_{C}]}.

The acceptance table for B𝔅_{i} has one entry τ_{C} for each C ∈ C. All entries in the new table have the same partition C and set of terminated processes T as in τ_{i}. The difference between the entries lies in the acceptance condition—the recurring set for p_{C} in the entry τ_{C} checks that p_{C} satisfies its complemented pairs condition in the original automaton.

The recurring condition in τ_{C} for signalling processes p_{C′} corresponding to components C′ ≠ C is the trivial one.

It is straightforward to see that B𝔅_{i} accepts an input α provided the (unique) run ρ_{α} of S𝔄 on α satisfies τ_{i}. Notice that ρ_{α} trivially satisfies all table entries not in X_{α}. We can check that ρ_{α} satisfies all the entries in X_{α} by intersecting the automata {B𝔅_{i}}_{i∈[1..m]}. (We omit the details of how to intersect two Büchi asynchronous automata.)

Overall, we can partition 𝒯_{S} according to the values of C and T in the entries. For each pair (C, T), we can then construct a Büchi asynchronous automaton as described in step (ii) above. To get a single Büchi automaton simulating S𝔄, we take the union of all the automata constructed in this fashion together with the automaton of step (i) which catches all inputs which do not match any of the table entries.

E Complexity analysis

Determinization In the input automaton B𝔄 = (𝔄, 𝒯_{B}), let N be the number of processes in 𝔄, M the size of the largest set in the collection {V_{p}}_{p∈𝒫} and K the number of entries in 𝒯_{B}.

We first estimate the number of bits required to describe the state of a signalling process p_{C} in R𝔅_{τ} corresponding to a single entry τ ∈ 𝒯_{B}. This state consists of the state of the subset automaton for 𝔄 together with one copy of the labelled tree used by Safra’s construction for each history in H_{S}, the set of histories over stable-info_{p_{C}} (I).

The state of the subset automaton for 𝔄 can be written down using M^{O(N^{3})} bits. Each labelled tree maintained by Safra’s construction requires O(M log M) bits [Saf]. In [KMS], it is shown that there are at most M^{O(N^{3})} elements in H_{p_{C}}, the set of all reachable histories over secondary(∂_{p_{C}} (I)). Since this is also a bound on |H_{S}|, p_{C} maintains at most M^{O(N^{3})} copies of Safra’s construction and, overall, the state of p_{C} can be written down using M^{O(N^{3})} · O(M log M) = M^{O(N^{3})} bits. Thus, the number of local states of p_{C} in R𝔅_{τ} is 2^{M^{O(N^{3})}}, which is essentially the same as in the subset construction of [KMS].

When combining the individual automata in {R𝔅_{τ}}_{τ∈𝒯_{B}} , we take the Kfold product of the state space of each individual process p. So, overall, the number of local states of a process is 2^{KM^{O(N^{3})}}.

The number of entries in the Rabin table 𝒯_{R} of the final deterministic automaton R𝔅 = (𝔅, 𝒯_{R}) is KM^{O(N^{4})}: each individual automaton R𝔅_{τ} = (𝔅_{τ}, 𝒯_{R_{τ}}) has as many entries in 𝒯_{R_{τ}} as there are possible histories over the events ⋃_{C∈C} stable-info_{p_{C}} (I). The number of such histories is bounded by M^{O(N^{4})}. Taking the product of the automata {R𝔅_{τ}}_{τ∈𝒯_{B}} results in the tables {𝒯_{R_{τ}} }_{τ∈𝒯_{B}} being concatenated together. Since K copies are concatenated, the final table has at most KM^{O(N^{4})} entries.

The product construction does not affect the lengths of the lists pairs_{C}. So, for each entry τ_{R} = (C, T, {(p_{C}, pairs_{C})}_{C∈C}) in 𝒯_{R}, the number of pairs in the list pairs_{C} for each C ∈ C is bounded by 2M.

Complementation The complexity of complementation is that of determinzation together with the cost of simulating a Streett automaton by a Büchi automaton. Let us analyze the second cost independently.

In the input Streett automaton S𝔄 = (𝔄, 𝒯_{S}), let N′ be the number of processes in 𝔄, M′ the size of the largest set in the collection {V_{p}}_{p∈𝒫}, K′ the number of entries in 𝒯_{S} and L′ the length of the longest list of pairs {G_{C}^{j}, R_{C}^{j}}_{j∈[1..k_{C}]} across all signalling processes and all table entries.

Vardi’s procedure for simulating an n-state Streett automaton with h pairs in the acceptance condition generates a Büchi automaton with n2^{h} states. So, in step (ii) of the simulation procedure for Streett automata, each signalling process in the automaton B𝔅_{i} we construct will have at most M′2^{L′} local states. The intersection of the automata {B𝔅_{i}}_{τ_{i}∈X_{α}} will involve at most K′ automata at a time, since the number of table entries overall is bounded by K′. Intersecting K′ Büchi asynchronous automata essentially generates the K′ fold product of each process’s local state space together with a modulo K′ counter. Thus, each process in the resulting automaton will effectively have (M′2^{L′})^{K′} = M^{′K′}2^{K′L′} local states.

When we take the union of all the automata constructed according to step (ii), we will make upto K′ disjoint copies of each process’s local state space. We then merge this with the trivial automaton constructed in step (i), which has only one local state per process. So, overall the Büchi asynchronous automaton simulating S𝔄 will have not more than K′M^{′K′}2^{K′L′} local states for each process.

If we plug in values for K′, M′ and L′ after determinization, we see that K′ = KM^{O(N^{4})}, M′ = 2^{KM^{O(N^{3})}} and L′ = 2M, where K, M and N are the parameters corresponding to the original non-deterministic Büchi asynchronous automaton. So, number of local states of each process in the complementary Büchi asynchronous automaton B\overline{𝔄} is bounded by KM^{O(N^{4})} · (2^{KM^{O(N^{3})}})^{KM^{O(N^{4})}} · 2^{KM^{O(N^{4})}·2M}, which is 2^{K^{2}M^{O(N^{4})}}.

Recent Publications in the BRICS Report Series

RS-95-58 Nils Klarlund, Madhavan Mukund, and Milind Sohoni. Determinizing Asynchronous Automata on In�nite Inputs. November 1995. 32 pp.

RS-95-57 Jaap van Oosten. Topological Aspects of Traces. November 1995. 16 pp.

RS-95-56 Luca Aceto, Wan J. Fokkink, Rob J. van Glabbeek, and Anna Ing� olfsd� ottir. Axiomatizing Pre�x Iteration with Silent Steps. November 1995. 25 pp.

RS-95-55 Mogens Nielsen and Kim Sunesen. Trace Equivalence - Partially Decidable! November 1995.

RS-95-54 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Using Monadic Second-Order Logic with Finite Domains for Speci�cation and Veri�cation. November 1995.

RS-95-53 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Automated Logical Veri�cation based on Trace Abstractions. November 1995.

RS-95-52 Anton��n Ku� cera. Deciding Regularity in Process Algebras. October 1995. 42 pp.

RS-95-51 Rowan Davies. A Temporal-Logic Approach to Binding-Time Analysis. October 1995. 11 pp.

RS-95-50 Dany Breslauer. On Competitive On-Line Paging with Lookahead. September 1995. 12 pp.

RS-95-49 Mayer Goldberg. Solving Equations in the λ-Calculus using Syntactic Encapsulation. September 1995. 13 pp.

RS-95-48 Devdatt P. Dubhashi. Simple Proofs of Occupancy Tail Bounds. September 1995. 7 pp. To appear in Random Structures and Algorithms.

RS-95-47 Dany Breslauer. The Suf�x Tree of a Tree and Minimizing Sequential Transducers. September 1995. 15 pp.