Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Proceedings, P.S. Thiagarajan (Ed.), Lecture Notes in Computer Science 1026, Springer-Verlag (1995) 456–470.

Determinizing Büchi Asynchronous Automata

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

1 BRICS^{†}, 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@ssf.ernet.in 3 Dept of Computer Sc and Engg, Indian Institute of Technology

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

Abstract. Büchi asynchronous automata are a natural distributed machine model for recognizing ω-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 second-order logics.

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.

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 Σ is equipped with a pre-specified independence relation I, describing the concurrency in the system [Maz]. 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 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.

† Basic Research in Computer Science, Centre of the Danish National Research Foundation.

1 Calling 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.

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 and determinization.

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 [KMS1] 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 efficiently simulate the complement of the determinized automaton using 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, automatatheoretic 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 [KMS1, MS] for manipulating asynchronous automata. In Section 6 we show how to apply these techniques to determinize Büchi asynchronous automata. Due to space limitations we have been forced to omit many examples and proofs. For a more detailed exposition, the reader is referred to [KMS2].

1 Preliminaries

The following definitions are essentially those of [KMS1] 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, …}.) A global run of 𝔄 on α : N → Σ is a function ρ : N_{0} → V_{𝒫}

such that ρ(0) ∈ 𝒱_{0} and, for i ∈ N, ρ(i−1) ⟹^{α(i)} ρ(i).

Analogously, we represent a finite word u ∈ Σ^{∗} of length m as a function u : [1..m] → Σ, where [i..j] abbreviates the set {i, i+1, …, j}. A global run of 𝔄 on u : [1..m] → Σ is a function ρ : [0..m] → V_{𝒫} such that ρ(0) ∈ 𝒱_{0} and, for

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

Let ρ be a global run. For P ⊆ 𝒫, ρ_{P} denotes the projection of ρ onto the P -components. So, ρ_{P} is a sequence of P -states. As usual, inf (ρ_{P}) denotes the set of P -states which occur infinitely often in ρ_{P}; 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 word α, we have to examine the communication between processes in the limit, as α is read. 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]. 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.

Since non-deterministic Büchi asynchronous automata are strictly more powerful than their deterministic counterparts [GP], 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 which is an extension of the classical subset construction for finite automata [Saf]. We do not have space to describe this construction here. However, it is possible to understand the salient features of our construction without getting into the precise details of how Safra’s construction works.

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𝔅_{τ} for the table entry τ = (C, T, {(p_{C} , G_{C})}_{C∈C}) we have to check that for each signalling process p_{C}, inf (ρ_{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 [KMS1] 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 connected components in 𝒢_{α} 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]. 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, 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 it 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.

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 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 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 ppredecessor 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 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, 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 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 [KMS1]. 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 [KMS1], on 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. 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 [KMS1].

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 ⋃_{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).

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.

Lemma 3 [KMS1]. 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—let this assignment of timestamps be denoted by 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 [KMS1]. 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 from the information in the P -state v⃗_{P} the set of all possible P -states of 𝔄 on I. In particular, from v⃗ we can recover all 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 ρ_{C} of 𝔄 on α which meets G_{C} infinitely often by running Safra’s construction locally. However, we have to check that the individual runs {ρ_{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 welldefined.) 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 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 copy of 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.

On reading a letter a, each process p in θ(a) updates its local states as follows (where we have left out some important details due to a lack of space):

(i) First p updates the local state components corresponding to the time-stamping 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 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}.

The sequential version of Safra’s construction uses labels {ℓ_{1}, ℓ_{2}, …, ℓ_{2M}}, where M is the number of states of the original automaton. The acceptance condition of the determinized automaton consists of pairs {(G^{j}, R^{j})}_{j∈[1..2m]}, where each pair (G^{j}, R^{j}) expresses some constraints on the label ℓ_{j}.

In the distributed construction, each signalling process uses labels in the same manner as in the sequential case and generates the same number of acceptance pairs. Let M_{C} = |V_{p_{C}} | be the number of possible local states for each signalling process p_{C} in 𝔄. Then pairs_{C} = {(G_{C}^{j}, R_{C}^{j})}_{j∈[1..2M_{C}]}, where, for j ∈ [1..2M_{C}], the sets G_{C}^{j} and R_{C}^{j} consist of all possible states of p_{C} in which label ℓ_{j} meets the criteria required by Safra’s construction and, in addition, the set of histories stored in the state includes the projection h_{p_{C}} of h onto stable-info_{p_{C}} (ℰ).

It can then be verified 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}. 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 Following the technique proposed by Vardi (described in [Saf]), we can use a non-deterministic Büchi asynchronous to efficiently simulate the complement of a deterministic Rabin asynchronous automaton. 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𝔄. 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})}} (see [KMS2] for details).

In [KMS1], 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 that of the subset construction.

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

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

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

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

[KMS2] N. Klarlund, M. Mukund, M. Sohoni: Determinizing asynchronous automata on infinite traces, Report TCS-95-6, School of Mathematics, SPIC Science Foundation, Madras (1995).

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

[MS] M. Mukund, M. Sohoni: Keeping track of the latest gossip: Bounded 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 ’94, LNCS 820 (1994) 142–153.

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