On the complementation of asynchronous cellular Büchi automata ^{∗}

Anca Muscholl

Universität Stuttgart, Institut für Informatik Breitwiesenstr. 20-22, 70565 Stuttgart, Germany

Abstract

We present direct subset automata constructions for asynchronous (asynchronous cellular, resp.) automata. This provides a solution to the problem of direct determinization for automata with distributed control for languages of finite traces. We use the subset automaton construction and apply Klarlund’s progress measure technique in order to complement non-deterministic asynchronous cellular Büchi automata for infinite traces. Both constructions yield a super-exponential blow-up in the size of local states sets.

1 Introduction

Infinite Mazurkiewicz traces provide a sound framework for studying non-termina-ting concurrent systems, such as e.g. distributed operating systems or transaction systems. Basically, a concurrent system is viewed as a labelled partial order of a special form. The labelling corresponds to a (finite) set Σ of atomic actions. The partial ordering is based on a fixed symmetric, reflexive dependence relation D ⊆ Σ×Σ, denoting pairs of actions which cannot be executed in parallel. Especially interesting are systems where the behaviour can be described by finite state devices. The family of recognizable languages of infinite traces, Rec(ℝ(Σ, D)), has been introduced by means of recognizing homomorphisms [9]. Various characterizations have been obtained for this class, including automata-theoretic and logical aspects [10, 6, 8], which generalize the well-understood framework of ωlanguages. We are interested in automata with distributed control, more precisely in asynchronous (asynchronous cellular, resp.) automata. They play a basic role in the theory of Mazurkiewicz traces, as finite automata do for sequential systems. For example, Zielonka’s important theorem states the equivalence between recognizability for languages of finite traces and acceptance by deterministic asynchronous cellular automata. For languages of infinite traces a natural counterpart of the classical Büchi acceptance condition [10] yields the equivalence between Rec(ℝ(Σ, D)) and the class of languages of infinite traces which are accepted by non-deterministic Büchi asynchronous cellular automata. As in the special case of ω-languages, recognizability of languages of infinite traces can also be characterized by deterministic automata, by using the analogue of the more powerful Muller acceptance condition [6]. This generalizes McNaughton’s theorem to languages of infinite traces. All these results hold also for the asynchronous automaton model, due to a straightforward transformation from asynchronous cellular to asynchronous automata. The closure of Rec(ℝ(Σ, D)) under complementation is easily seen from the definition by recognizing homomorphisms (or the acceptance by deterministic Muller automata). We present in this paper a direct proof based on automata by exhibiting a complementation procedure for non-deterministic asynchronous cellular Büchi automata. We use the notion of progress measures, which has been introduced by Klarlund [11] for complementing Büchi (and Streett) ω-automata. We will apply progress measures locally to computation subgraphs of asynchronous automata. A basic component of several constructions for ω-automata [20, 11] is the usual subset automaton of Rabin and Scott. In the case of asynchronous automata, no subset construction has been so far available, in spite of several attempts [18, 5]. We present in Sect. 3 subset constructions for asynchronous (asynchronous cellular, resp.) automata relying on Cori/Métivier’s notion of asynchronous mapping [2]. Based on the bounded time-stamping of Zielonka’s construction we exhibit natural mappings which turn out to be asynchronous and thus can be directly translated into asynchronous (asynchronous cellular, resp.) automata. The deterministic automata obtained provide the full information of asynchronous subset automata. The highly technical part is the proof of correctness, i.e. showing that the above mappings are asynchronous, which requires a detailed analysis of prefix relations in a given trace. We consider here two models of trace automata with distributed control (asynchronous and asynchronous cellular, resp.), due to size considerations which may be significant and determine their practical use. Asynchronous automata seem to be more advantageous, since they are more compact, in general; the cellular model is easier to understand, due to canonical relations to the prefix structure of a trace. The determinization ideas are closely related and in both cases a superexponential blow-up of size results. However we are interested in the precise size of the subset automata obtained. Related ideas with respect to determinization have been developed independently in [12], where a subset construction for asynchronous automata essentially matching the lower bound is presented. We note that the superexponential lower bound for the size blow-up obtained in [12] holds by the same argument for the cellular model, too. We consider infinite traces only in Sect. 4, where we use the subset automaton introduced previously and apply the progress measure of Klarlund [11] to asynchronous cellular Büchi automata. We obtain a size blow-up for the global state space of 2^{N^{O(1)}}. Note that we can obtain a deterministic automaton for the complementation problem using deterministic asynchronous Muller automata, applying the algebraic construction given in [6]. This yields however a blow-up for the set of global states at least doubly exponential, since we have to compute the syntactic monoid and to apply usual determinization, as well as Zielonka’s construction. A preliminary version of this paper appeared in [16]. In this paper we additionally consider the asynchronous model with regard to determinization constructions. Moreover, we present here a more involved subset construction which improves the size of the subset automata.

∗Research supported by the ESPRIT Basic Research Action No. 6317 (ASMICS 2).

2 Preliminaries

Throughout this paper we denote by (Σ, D) a finite dependence alphabet, i.e. a finite alphabet Σ together with a reflexive, symmetric dependence relation D ⊆ Σ×Σ. The complementary relation I = (Σ×Σ)\D, called independence relation, induces an equivalence relation ≡_{I} on Σ^{∗}, generated by the pairs (uabv, ubav), with u, v ∈ Σ^{∗}, (a, b) ∈ I. The relation ≡_{I} turns out to be a congruence. The quotient monoid 𝕄(Σ, D) = Σ^{∗}/ ≡_{I} was called trace monoid by Mazurkiewicz [13] and it was first used in combinatorics for rearrangement problems [1]. The canonical surjective homomorphism associated to ≡_{I} will be denoted by φ: Σ^{∗} → 𝕄(Σ, D). For a ∈ Σ, A ⊆ Σ, let D(a) = {b ∈ Σ | (a, b) ∈ D} and D(A) = ⋃_{a∈A} D(a). By definition, a trace t is a congruence class of words and it may be represented by words. A natural, unique representation is given by considering labelled partial orders. We identify a trace t with a dependence graph, i.e. with a (isomorphism class of a) labelled directed, acyclic graph G = [V, E, λ], where λ: V → Σ is the labelling of the vertex set and edges exist between (different) vertices with dependent labellings, i.e. for every u, v ∈ V we have (λ(u), λ(v)) ∈ D if and only if u = v or (u, v) ∈ E ∪ E^{−1}. Given the trace t = [a_{1} ⋯ a_{n}], we define the associated dependence graph by taking n vertices V = {1, …, n} labelled as λ(i) = a_{i}, with edges (i, j) ∈ E for 1 ≤ i < j ≤ n whenever (a_{i}, a_{j}) ∈ D. In this paper we consider finite and infinite dependence graphs with countable vertex sets, such that λ^{−1}(a) is well-ordered for every a ∈ Σ. The set of dependence graphs satisfying these properties is denoted by 𝔾(Σ, D). It forms a monoid with the multiplication [V_{1}, E_{1}, λ_{1}][V_{2}, E_{2}, λ_{2}] = [V_{1} ˙⋃ V_{2}, E, λ_{1} ˙⋃ λ_{2}], where E = E_{1} ˙⋃ E_{2} ˙⋃{(v_{1}, v_{2}) ∈ V_{1} × V_{2} | (λ_{1}(v_{1}), λ_{2}(v_{2})) ∈ D}. The identity is the empty graph 1 = [∅, ∅, ∅]. The requirement that any subset of vertices with the same labelling is well-ordered allows us to represent vertices as pairs (a, i), with a ∈ Σ and i ≥ 0 a countable ordinal, where (a, i) represents the (i + 1)-th node labelled by the letter a. This is called the standard representation. We use here the usual notion of infinite traces, where every vertex in the dependence graph has a finite past. This corresponds to the ideal completion of 𝕄(Σ, D) under the prefix ordering, which has been already considered by Mazurkiewicz [14]. Infinite traces with this property are called real traces and the set of real traces is denoted ℝ(Σ, D). Equivalently, real traces correspond to finite and infinite dependence graphs having a representation by words; i.e. with φ: Σ^{∞} → 𝔾(Σ, D) being the extension of the canonical mapping to the set of finite and infinite words Σ^{∞} = Σ^{∗} ∪ Σ^{ω}, we have ℝ(Σ, D) = φ(Σ^{∞}). Note that ℝ(Σ, D) is not a submonoid of 𝔾(Σ, D) (e.g. for (a, b) ∈ D we have a^{ω}, b ∈ ℝ(Σ, D), but a^{ω}b ∉ ℝ(Σ, D)). The notion of recognizability provides an interesting language class in various contexts of finite and infinite objects: words, traces, trees, graphs. For real traces a language L is recognizable if φ^{−1}(L) ⊆ Σ^{∞} is recognizable in the usual sense for languages over Σ^{∞}. The class of recognizable real trace languages is denoted by Rec(ℝ(Σ, D)). A natural finite state device for trace languages is the asynchronous model introduced by Zielonka [21]. By asynchronous automata we mean two types of automata of equal expressive power, both of which have distributed control and memory. The difference consists mainly in the kind of restriction imposed on the concurrent access to common data. Asynchronous automata belong to the Exclusive-Read-Exclusive-Write type, while asynchronous cellular automata correspond to the Concurrent-Read-Owner-Write access restriction. An asynchronous cellular automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F) has for each a ∈ Σ a set of local states Q_{a} and a local transition relation δ_{a} ⊆ (∏_{b∈D(a)} Q_{b})×Q_{a}. The set of global states is ∏_{a∈Σ} Q_{a}, and q_{0} ∈ ∏_{a∈Σ} Q_{a} resp. F ⊆ ∏_{a∈Σ} Q_{a} denotes the initial state, resp. the set of final states of A. The global transition relation δ ⊆ ∏_{a∈Σ} Q_{a} × Σ × ∏_{a∈Σ} Q_{a} is defined for q = (q_{a})_{a∈Σ}, q′ = (q′_{a})_{a∈Σ} by

\begin{aligned}q′ ∈ δ(q, a) & :⟺ & q′_{a} ∈ δ_{a}((q_{b})_{b∈D(a)}) & and \\ & & q′_{c} = q_{c}, for c ≠ a . \end{aligned}

Thus, an a-transition changes only the local a-state and the change depends only on the local states of letters b with (b, a) ∈ D. Note that for any q, q′ ∈ ∏_{a∈Σ} Q_{a}, u, v ∈ Σ^{∗} with u ≡_{I} v and q′ ∈ δ(q, u) also q′ ∈ δ(q, v) holds. Hence, we may define the trace language accepted by A by L(A) = {t ∈ 𝕄(Σ, D) | δ(q_{0}, t) ∩ F ≠ ∅}. The asynchronous automaton model, as originally considered by Zielonka [21], associates to each letter a ∈ Σ a set dom(a) ⊆ {1, …, m} of processors representing the read- and write-domain, such that (a, b) ∈ I ⇔ dom(a) ∩ dom(b) = ∅. An asynchronous automaton A is a tuple ((Q_{i})_{i=1}^{m}, (δ_{a})_{a∈Σ}, q_{0}, F), with a local transition relation δ_{a} ⊆ ∏_{i∈dom(a)} Q_{i} × ∏_{i∈dom(a)} Q_{i} for each letter a ∈ Σ. The set of global states is ∏_{i=1}^{m} Q_{i}, and q_{0} ∈ ∏_{i=1}^{m} Q_{i}, resp. F ⊆ ∏_{i=1}^{m} Q_{i} denotes the initial state, resp. the set of final states of A. A global transition step q′ ∈ δ(q, a), q = (q_{i})_{1≤i≤m}, q′ = (q′_{i})_{1≤i≤m}, is defined by

q′ ∈ δ(q, a) :⟺ (q′_{i})_{i∈dom(a)} ∈ δ_{a}((q_{i})_{i∈dom(a)}) and
q′_{j} = q_{j}, for j ∉ dom(a) .

The language accepted by A is L(A) = {t ∈ 𝕄(Σ, D) | δ(q_{0}, t) ∩ F ≠ ∅}. An automaton is called complete, if all transition relations are totally defined. By standard methods, asynchronous and asynchronous cellular automata are shown to be equivalent. Starting e.g. with an asynchronous cellular automaton with local states sets Q_{a}, a ∈ Σ, an equivalent asynchronous automaton is obtained by embedding A through Q_{i} := ∏_{i∈dom(a)} Q_{a}. Note that the number of (reachable) global states does not change. Conversely, given an asynchronous automaton with local states Q_{i}, 1 ≤ i ≤ m, a simple time-stamping for each set A_{i} = {a ∈ Σ | i ∈ dom(a)} can be used for determining the last occurrence of letters from A_{i} (note A_{i} × A_{i} ⊆ D): the sum modulo |A_{i}| of the time-stamps associated to a ∈ A_{i} yields the last occurrence from A_{i} (see also [19]). Let the size of an asynchronous (cellular) automaton denote the total number of local states. Then an asynchronous automaton of size n with m processors is transformed into an equivalent cellular one of size O(|Σ|n)^{m}; the converse transformation yields an asynchronous automaton with m processors and size O(m · n^{|Σ|}). Zielonka’s theorem [21] characterizes the class of recognizable languages of finite traces by deterministic asynchronous automata, providing a suitable recognition device for traces. Asynchronous automata showed to be an appropriate finite state model for languages of real traces, too. A distributed (i.e., local) analogue of the usual Büchi (resp. Muller) acceptance condition has been proposed in [10]. The idea is to augment e.g. an asynchronous cellular automaton by a table T ⊆ ∏_{a∈Σ} P(Q_{a}), i.e. we are given a tuple A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, T ). Consider an infinite transition path π = (q^{0}, a_{0}, q^{1}, a_{1}, …) in A, with q^{n} ∈ ∏_{a∈Σ} Q_{a}, a_{n} ∈ Σ and q^{n+1} ∈ δ(q^{n}, a_{n}) for n ≥ 0. For each a ∈ Σ we are interested in the set of local a-states which occur infinitely often in π, i.e. in the set inf_{a}(π) = {q_{a} ∈ Q_{a} | (q^{n})_{a} = q_{a} for infinitely many n}. The path π is accepted by A with the Büchi acceptance condition if for some T = (T_{a})_{a∈Σ} ∈ T we have inf_{a}(π) ⊇ T_{a} for every a ∈ Σ. (Viewing A as a Muller automaton, π is accepted if for some T = (T_{a})_{a∈Σ} ∈ T , inf_{a}(π) = T_{a} for every a ∈ Σ). An infinite trace t ∈ ℝ(Σ, D) is accepted if there exists a path π as above labelled by some representing word of t, i.e. t = φ(a_{0}a_{1} …), which is accepted. (The local acceptance condition ensures that this notion of acceptance is well-defined, i.e. it does not depend on the representing word, [10]). Finite traces are accepted in the usual way, by reaching a final state from F. Similar definitions apply to the asynchronous model, where the acceptance depends on the sets inf_{i}(π) = {q_{i} ∈ Q_{i} | (q^{n})_{i} = q_{i} for infinitely many n}.

We denote by R_{A}(t) the set of runs of an asynchronous cellular automaton A on t ∈ ℝ(Σ, D), starting with the initial state q_{0} of A. We view a run r ∈ R_{A}(t) as a labelling r: V (t) → ∪_{a∈Σ}Q_{a} of the dependence graph of t, [V (t), E(t), λ(t)], by local states, such that r is consistent with the alphabetical labelling λ(t) and with the transition relations (δ_{a})_{a∈Σ}. Concretely, consider (a, n_{a}) ∈ V (t) and let for b ∈ D(a): q_{b} = r(b, n_{b}), where ((b, n_{b}), (a, n_{a})) ∈ E(t) with n_{b} maximal, respectively q_{b} = (q_{0})_{b}, if no such (b, n_{b}) exists. Then we have r(a, n_{a}) ∈ δ_{a}((q_{b})_{b∈D(a)}). For u ∈ 𝕄(Σ, D), r ∈ R_{A}(u), let δ(r, u) denote the global state reached in the run r on u.

We close this section with some general notations. For t ∈ ℝ(Σ, D), a ∈ Σ we denote by |t|_{a} the number of occurrences of a in t; by alph(t) = {a ∈ Σ | |t|_{a} > 0} the alphabet of t; finally, by alphinf(t) = {a ∈ Σ | |t|_{a} = ∞} the alphabet at infinity of t. For A ⊆ Σ let Inf(A) = {t ∈ ℝ(Σ, D) | alphinf(t) = A}. For t ∈ 𝕄(Σ, D) let max(t) = {a ∈ Σ | ∃w ∈ Σ^{∗} : t = φ(wa)} be the labellings of the maximal elements of t. A subalphabet A ⊆ Σ is called connected if (A, D|_{A×A}) is a connected subgraph of (Σ, D). A trace t is connected if alph(t) is connected. The prefix order on ℝ(Σ, D) is defined by u ≤ t if t = uv for some v ∈ ℝ(Σ, D). For t = uv let u^{−1}t = v. As usual, u ⊓ v is the greatest lower bound of u, v. Whenever it exists, the least upper bound of u, v is denoted by u ⊔ v. For m ∈ ℕ let [m] be the set \{1, …, m\}. The complement of a set X is denoted \overline{X}, while P(X) denotes the powerset of X.

3 Determinization for asynchronous automata

We present in this section subset constructions for asynchronous (asynchronous cellular, resp.) automata relying on the notion of asynchronous mapping introduced by Cori/Métivier [2]. While the underlying idea of the first construction is more intuitive, the second one achieves a better bound for the size of the subset automata obtained. Asynchronous mappings reflect the functional aspect of asynchronous automata. As defined below, a mapping μ: 𝕄(Σ, D) → S is asynchronous if it can be computed stepwise in a distributed way, thus being easily transformed into an equivalent deterministic asynchronous (cellular) automaton. (For more details and general notions on traces and asynchronous automata see Ch. 7,8 in [7].) Before recalling the definition, let us introduce a basic notation for trace prefixes. For t ∈ 𝕄(Σ, D), a ∈ Σ and A ⊆ Σ let

∂_{a}(t) = ⊓{ u ≤ t | |t|_{a} = |u|_{a} } and ∂_{A}(t) = ⨆_{a∈A} ∂_{a}(t)
(In particular ∂_{∅}(t) = 1 and ∂_{Σ}(t) = ∂_{max(t)} = t.)

Thus, ∂_{a}(t) resp. ∂_{A}(t) = ⨆{u ≤ t | max(u) ⊆ A} is the minimal prefix of t containing all a, resp. all letters a ∈ A from t. Especially we have ∂_{a}(ta) = ∂_{D(a)}(t)a. In the following we will use the notation ∂_{a,A}(t) instead of ∂_{a}(∂_{A}(t)) (or simply ∂_{a,b}(t), if A = {b}).

Definition 3.1 ([2]) A mapping μ: 𝕄(Σ, D) → S is called asynchronous if for every t ∈ 𝕄(Σ, D), a ∈ Σ and A, B ⊆ Σ the following conditions are satisfied.

• The value μ(∂_{D(a)}(t)) and the letter a uniquely determine μ(∂_{a}(ta)).

• The values μ(∂_{A}(t)), μ(∂_{B}(t)) and A, B uniquely determine μ(∂_{A∪B}(t)).

For example, alph(·) is an asynchronous mapping. On the other hand, max(·) is not asynchronous (let e.g. (Σ, D) = a −b −c and consider t_{1} = ac, t_{2} = acb, resp. t′_{1} = bac, t′_{2} = b: max(t_{1} ⊔ t_{2}) ≠ max(t′_{1} ⊔ t′_{2})). Suppose we are given an asynchronous mapping μ: 𝕄(Σ, D) → S and a subset R ⊆ S. Then let A_{μ} = ((Q_{a})_{a∈Σ}, δ, q_{0}, F) be defined by Q_{a} = {μ(∂_{a}(t)) | t ∈ 𝕄(Σ, D)}, a ∈ Σ, q_{0} = (μ(1))_{a∈Σ}, F = {(μ(∂_{a}(t)))_{a∈Σ} | μ(t) ∈ R}, and for q, q′ ∈ ∏_{a∈Σ} Q_{a}:

q′ = δ(q, a) ⟺ q_{b} = μ(∂_{b}(t)), q′_{b} = μ(∂_{b}(ta)), b ∈ Σ, for some t ∈ 𝕄(Σ, D).

Since ∂_{a}(ta) = ∂_{D(a)}(t)a and ∂_{b}(ta) = ∂_{b}(t) for b ≠ a, it is immediate that δ is the transition function of an asynchronous cellular automaton. Moreover, with δ(q_{0}, t) = (μ(∂_{a}(t)))_{a∈Σ}, it is clear that L(A_{μ}) = μ^{−1}(R) [3, 4].

Remark 3.2 1. Asynchronous mappings can be easily translated to asynchronous automata, too. Let dom(a) ⊆ [m] denote the domain of a ∈ Σ, and let A_{i} = {a ∈ Σ | i ∈ dom(a)}, i ∈ [m]. Consider the automaton A = ((Q_{i})_{i∈[m]}, (δ_{a})_{a∈Σ}, q_{0}, F) with Q_{i} = {μ(∂_{A_{i}}(t)) | t ∈ 𝕄(Σ, D)}, q_{0} = (μ(1))_{i∈[m]}, F = {(μ(∂_{A_{i}}(t)))_{i∈[m]} | μ(t) ∈ R}. The transition q′ = δ(q, a) is defined if q_{i} = μ(∂_{A_{i}}(t)) and q′_{i} = μ(∂_{A_{i}}(ta)), i ∈ [m], holds for some t ∈ 𝕄(Σ, D). It is left to the reader to verify that δ is the transition function of an asynchronous automaton accepting μ^{−1}(R).

2. Consider a non-deterministic asynchronous (asynchronous cellular, resp.) automaton A. It will suffice to obtain an asynchronous mapping μ: 𝕄(Σ, D) → S based on A, with S finite and such that μ^{−1}μ(L(A)) = L(A). The asynchronous (cellular) subset automaton will be then directly constructed as just described.

As previously mentioned, we will use throughout our determinization constructions Zielonka’s labelling function ν: 𝕄(Σ, D) → {0, …, |Σ|}^{Σ×Σ}, which is defined inductively for a, b ∈ Σ, t ∈ 𝕄(Σ, D) by:

• ν(1)(a, b) = 0.

• If t ≠ ∂_{a,b}(t) then ν(t)(a, b) = ν(∂_{a,b}(t))(a, a).

• If t = ∂_{a}(t) and t ≠ 1 then

ν(t)(a, a) = min{n > 0 | n ≠ ν(t)(a, c) for every c ≠ a}.

Note that ν(∂_{A}(t))(c, a) = ν(t)(c, a) for every a ∈ A. The labelling function ν is a time-stamping function, allowing to determine the actuality of information received in a distributed way. In particular, it provides information about ordering of prefixes of the form ∂_{a}(t). Consider e.g. the dependence alphabet (Σ = {a, b, c, d}, D) with D = (Σ×Σ)\{(a, c), (c, a), (b, d), (d, b)}, and the trace t = [ada^{n}cb], n ≥ 1. Then using ν we are able to determine whether b or c have the most recent information about a. In the following we point out some basic properties of ν:

Fact 3.3 ([3, 4]) Let t ∈ 𝕄(Σ, D), a, b, c ∈ Σ, A, B ⊆ Σ. Then:

1. ν(t)(c, a) = ν(t)(c, b) ⟺ ∂_{c,a}(t) = ∂_{c,b}(t) .

2. Suppose that we are given the value ν(t) or both values ν(∂_{A}(t)), ν(∂_{B}(t)). Then we can determine the set C_{a,b} := {c ∈ Σ | ∂_{c,a}(t) = ∂_{c,b}(t)}, for every a, b ∈ A ∪ B. Moreover, we can determine for every c ∈ Σ which of the following holds:

∂_{c,A}(t) = ∂_{c,B}(t) , resp. ∂_{c,A}(t) < ∂_{c,B}(t) , resp. ∂_{c,B}(t) < ∂_{c,A}(t) .

3. ν is an asynchronous mapping.

3.1 A simple determinization construction

The crucial idea for the determinization constructions presented in the sequel is to augment the time-stamping mapping ν by a mapping ρ depending on the given non-deterministic asynchronous (asynchronous cellular, resp.) automaton A. We start considering the cellular model and denote in the following by Q the set of local states, Q = ˙⋃_{a∈Σ} Q_{a} of an asynchronous cellular automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F). Let now ρ: 𝕄(Σ, D) → P(Q^{Σ×Σ}) be given for t ∈ 𝕄(Σ, D) as

ρ(t) = {f ∈ Q^{Σ×Σ} | ∃r ∈ R_{A}(t) s.t. for every a, b ∈ Σ : f(b, a) = δ(r, ∂_{a}(t))_{b}} .

Thus, every element f: Σ × Σ → Q of ρ(t) is associated to a run r on t, such that for every a, b ∈ Σ, f(b, a) represents the local b-state reached in the run r on the prefix ∂_{a}(t) of t.

Proposition 3.4 Given a non-deterministic asynchronous cellular automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F). Then the associated mapping (ν, ρ) is asynchronous. Moreover, we have

L(A) = {t ∈ 𝕄(Σ, D) | ∃q = (q_{a})_{a∈Σ} ∈ F, ∃f ∈ ρ(t) s.t. f(a, a) = q_{a}, ∀a ∈ Σ}.

For the proof, let us start with a technical lemma.

Lemma 3.5 Let A, B ⊆ Σ, t = ∂_{A∪B}(t) and t_{1} = ∂_{A}(t), t_{2} = ∂_{B}(t). Let a, b ∈ Σ such that ∂_{a}(t_{1}) < ∂_{a}(t_{2}) and ∂_{b,a}(t) ≤ t_{1} ⊓ t_{2}. Then there exists some d ∈ Σ such that ∂_{b,a}(t) = ∂_{b,d}(t_{1}). Moreover, a letter d with this property can be computed effectively, given the values ν(t_{1}) and ν(t_{2}).

Proof: By assumption, we have ∂_{b,a}(t) = ∂_{b,a}(t_{2}) ≤ t_{1} ⊓ t_{2}. Using ν the common prefix s := t_{1} ⊓ t_{2} can be determined, since we have max(s) ⊆ C, with C = {c ∈ Σ | ∂_{c}(t_{1}) = ∂_{c}(t_{2})} = {c ∈ Σ | ν(t_{1})(c, c) = ν(t_{2})(c, c)} [3]. By the very definition of C we have ∂_{c}(s) = ∂_{c}(t_{i}), for every c ∈ C, i = 1, 2. Let further u, v ∈ 𝕄(Σ, D) be such that t_{1} = su, t_{2} = sv, hence alph(u) × alph(v) ⊆ I. Assume first ∂_{b,a}(t) ≠ 1 and consider the set C′ = {d ∈ Σ | ∂_{d,a}(t_{2}) = ∂_{d}(s)}. We denote s′ = s ⊓ ∂_{a}(t_{2}), with s = s′x, ∂_{a}(t_{2}) = s′y for suitable x, y ∈ 𝕄(Σ, D), where alph(x) × alph(y) ⊆ I (see also Fig. 1). Again, we have s′ = ∂_{C′}(s′) = ∂_{C′}(s) = ∂_{C′,a}(t_{2}). From ∂_{b,a}(t_{2}) ≤ ∂_{b}(s) we obtain directly ∂_{b,a}(t_{2}) = ∂_{b}(s′). (In particular, s′ ≠ 1, thus C′ ≠ ∅.) Together with s′ = ∂_{C′}(s) we have ∂_{b,a}(t_{2}) = ∂_{b,d}(s) for a suitable d ∈ max(s′) ⊆ C′. We show now ∂_{d}(s) = ∂_{d}(t_{1}). Since d belongs to a path from b to a, where the vertex labelled a lies in y, there is some e ∈ alph(y) with (d, e) ∈ D (see Fig. 1). Due to y ≤ v, the assumption d ∈ alph(u) would contradict alph(u)×alph(v) ⊆ I. (Note that y ≠ 1, otherwise we would have ∂_{a}(t_{2}) ≤ s.) By the definition of C′ we have C′ ∩ alph(x) = ∅. From t_{1} = s′xu we conclude ∂_{d}(t_{1}) = ∂_{d}(s′) = ∂_{d}(s). Note also that ∂_{b,a}(t_{2}) = ∂_{b,C′′}(s), where C′′ := C′ ∩ D(alph(v)). For ∂_{b,a}(t_{2}) ≠ 1 (i.e., ν(t_{2})(b, a) ≠ 0) we compute effectively a letter d with ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}) as follows: using ν(t_{1}), ν(t_{2}) we first determine the sets C and alph(v) [3]; using again ν(t_{2}) we compute C′. Finally we choose d ∈ C′′ such that ∂_{b,d}(t_{1}) = ∂_{b,C′′}(t_{1}) and obtain

∂_{b,d}(t_{1}) = ∂_{b,C′′}(t_{1}) =^{C′′⊆D(alph(v))} ∂_{b,C′′}(s) = ∂_{b,a}(t_{2}) .

Finally, if ∂_{b,a}(t_{2}) = 1, then d = a satisfies the requirement ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}). □

Remark 3.6 Consider now a clique covering of (Σ, D) = (⋃_{i∈[m]} A_{i}, ⋃_{i∈[m]} A_{i} × A_{i}). A closer look at the proof of Lem. 3.5 yields the existence of a clique A_{k} such that ∂_{b,a}(t) = ∂_{b,A_{k}}(t_{1}). For this, let us assume ∂_{b,a}(t) ≠ 1 and consider a clique A_{k} containing both d, e, with the notations from the last proof. We observe that ∂_{A_{k}}(t_{1}) = ∂_{A_{k}}(s′) = ∂_{d}(s′), since A_{k} ⊆ D(e) ⊆ D(alph(y)) and d ∈ A_{k} ∩ max(s′). For ∂_{b,a}(t) = 1 we choose A_{k} with a ∈ A_{k} and note a ∉ alph(u). Hence, it can be easily verified that for any i, j ∈ [m] with ∂_{A_{i}}(t_{1}) < ∂_{A_{i}}(t_{2}) and ∂_{A_{j},A_{i}}(t) ≤ t_{1} ⊓ t_{2} some k ∈ [m] effectively exists such that ∂_{A_{j},A_{i}}(t) = ∂_{A_{j},A_{k}}(t_{1}).

[figure] [figure] [figure] [figure]  t_{1} = ∂_{A}(t) t^{2} = ∂^{B}(t) a b  e d ∈ C′ x y s′ Figure 1: ∂^{b,d}(t^{1}) = ∂^{b,a}(t^{2}) = ∂^{b,a}(t).

Proof of 3.4: By Fact 3.3 we know that ν is asynchronous. Let t ∈ 𝕄(Σ, D), a ∈ Σ, A, B ⊆ Σ. Given ν(∂_{D(a)}(t)), ρ(∂_{D(a)}(t)) and a, we define R ⊆ Q^{Σ×Σ} by letting g ∈ R if for some f ∈ ρ(∂_{D(a)}(t)):

• g(c, b) = f(c, b), for b ≠ a and c ∈ Σ;

• g(c, a) = q_{c} ∈ Q_{c}, where q_{c} = f(c, c) for c ≠ a, and q_{a} ∈ δ_{a}((f(b, b))_{b∈D(a)}).

It is straightforward to see R = ρ(∂_{a}(ta)), since runs on ∂_{a}(ta) represent exactly extensions of runs on ∂_{D(a)}(t) by an a-transition. The details are left to the reader. Consider now A, B ⊆ Σ and t = ∂_{A∪B}(t), with t_{1} = ∂_{A}(t), t_{2} = ∂_{B}(t), s = t_{1} ⊓ t_{2}. Hence, t_{1} = su and t_{2} = sv with alph(u) × alph(v) ⊆ I. We denote C = {c ∈ Σ | ∂_{c}(t_{1}) = ∂_{c}(t_{2})} = {c ∈ Σ | ν(t_{1})(c, c) = ν(t_{2})(c, c)}. Let ν(t_{i}), ρ(t_{i}) be given and define R ⊆ Q^{Σ×Σ} by f ∈ R if for some f_{i} ∈ ρ(t_{i}) (i = 1, 2) satisfying f_{1}(c′, c) = f_{2}(c′, c) for every c ∈ C, c′ ∈ Σ, we have for all a, b ∈ Σ:

f(b, a) = \{ \begin{matrix}f_{1}(b, a) & if ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1}) \\ f_{2}(b, a) & if ∂_{b}(s) < ∂_{b,a}(t_{2}) \\ f_{1}(b, d) & otherwise, with d ∈ Σ s.t. ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}) . \end{matrix}

By Lemma 3.5 f is well-defined in the last case, too. The definition of f is based on the idea of combining pairs of runs on t_{1}, t_{2} if they yield the same global state on the common prefix s = t_{1} ⊓ t_{2}. More precisely, let r_{i} ∈ R_{A}(t_{i}) be given such that δ(r_{1}, ∂_{c}(t_{1})) = δ(r_{2}, ∂_{c}(t_{2})), for every c ∈ C. In particular, we also have δ(r_{1}, s) = δ(r_{2}, s), since s = ∂_{C}(s). Denoting by [V_{i}, E_{i}, λ_{i}] the dependence graph of t_{i} it follows easily that the mapping r: V_{1} ∪ V_{2} → Q with

r(v) = \{ \begin{matrix}r_{1}(v) & if v ∈ V_{1} \\ r_{2}(v) & if v ∈ V_{2} \ V_{1} \end{matrix}

is a well-defined run on t. Hence, for the inclusion R ⊆ ρ(t) it suffices to show that the mappings f ∈ Q^{Σ×Σ} defined above correspond exactly to runs r: V_{1} ∪V_{2} → Q as just described. The converse inclusion ρ(t) ⊆ R is immediate. For a, b ∈ Σ we distinguish whether ∂_{b,a}(t) = ∂_{b,a}(t_{1}) or ∂_{b,a}(t) = ∂_{b,a}(t_{2}) holds, where in the second case the position of the maximal vertex of ∂_{b,a}(t) (if any) w.r.t. v or s is taken into account:

∂_{b,a}(t) = \{ \begin{matrix}∂_{b,a}(t_{1}) & if ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1}) \\ ∂_{b,a}(t_{2}) & if ∂_{b}(s) < ∂_{b,a}(t_{2}) \\ ∂_{b,d}(t_{1}) & otherwise, for d ∈ Σ s.t. ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}) . \end{matrix}

To conclude the proof, note that the values ν(t_{1}), ν(t_{2}) allow to distinguish the three cases considered in the definition of f, due to s = ∂_{C}(t_{2}), together with Lem. 3.5. □

Notation: We will use in the next section the abbreviation q →^{(a)} q′, for t ∈ 𝕄(Σ, D) and states q, q′ ∈ ∏_{a∈Σ} Q_{a} in an asynchronous cellular automaton A. This means that t ∈ 𝕄(Σ, D) and a run r ∈ R_{A}(∂_{a}(ta)) exist, such that q = δ(r, ∂_{a}(t)) and q′ = δ(r, ∂_{a}(ta)). Note that the subset automaton based on Prop. 3.4 (see also Prop. 3.9) provides this information, given the values ν(∂_{b}(t)), ρ(∂_{b}(t)), for all b ∈ D(a).

Remark 3.7 The idea of the construction in Prop. 3.4 can be easily adapted to asynchronous automata. Let A = ((Q_{i})_{i=1}^{m}, (δ_{a})_{a∈Σ}, q_{0}, F) be a non-deterministic asynchronous automaton, and let Q = ˙⋃_{i∈[m]} Q_{i}. Let ρ: 𝕄(Σ, D) → P(Q^{[m]×[m]}) be defined for t ∈ 𝕄(Σ, D) by:

ρ(t) := {f ∈ Q^{[m]×[m]} | ∃r ∈ R_{A}(t) : δ(r, ∂_{A_{i}}(t))_{j} = f(j, i)}.

Then the mapping μ = (ν, ρ) is asynchronous. Consider e.g. the case where μ(t_{1}), μ(t_{2}) are given, with t_{1} = ∂_{A}(t) = su, t_{2} = ∂_{B}(t) = sv, alph(u) × alph(v) ⊆ I. Assume that both u and v are non-empty and let C = {c ∈ Σ | ∂_{c}(t_{1}) = ∂_{c}(t_{2})}. We show how runs r_{i} ∈ R_{A}(t_{i}), i = 1, 2, can be chosen with δ(r_{1}, s) = δ(r_{2}, s). For k ∈ [m] let c ∈ max(s) be such that ∂_{A_{k}}(s) = ∂_{A_{k},c}(s). Due to u ≠ 1, v ≠ 1 we have c ∈ D(alph(u))∩D(alph(v)), hence there exist i, j ∈ [m] with A_{i}∩alph(u) ≠ ∅, A_{j} ∩ alph(v) ≠ ∅ and c ∈ A_{i} ∩ A_{j}. Clearly, A_{i} ∩ alph(v) = A_{j} ∩ alph(u) = ∅. This yields ∂_{c}(s) = ∂_{A_{i}}(t_{2}) = ∂_{A_{j}}(t_{1}), hence ∂_{A_{k}}(s) = ∂_{A_{k},A_{i}}(t_{2}) = ∂_{A_{k},A_{j}}(t_{1}). Moreover, C, c and i, j can be effectively determined from ν(t_{1}), ν(t_{2}). For the definition of the combined run on t = t_{1} ⊔ t_{2} we require f_{1}(k, i) = f_{2}(k, j) for all k and we use Rem. 3.6. The details and the definition of a subset R ⊆ {0, …, |Σ|}^{Σ×Σ} × P(Q^{[m]×[m]}) with L(A) = μ^{−1}(R) are left to the reader.

The asynchronous mappings considered in Prop. 3.4 and Rem. 3.7 lead together with Rem. 3.2(2) to determinization constructions for both asynchronous automata models as stated in the following theorem. Recall that the size of an asynchronous (cellular) automaton corresponds to the total number of local states.

Theorem 3.8 1. Let A be a non-deterministic asynchronous cellular automaton of size n. Then a deterministic asynchronous cellular subset automaton Ã of size 2^{O(n^{|Σ|^{2}})} effectively exists with L(A) = L(Ã).

2. Let A be a non-deterministic asynchronous automaton of size n with m processors. Then a deterministic asynchronous subset automaton Ã of size 2^{O(n^{m^{2}})} effectively exists with L(A) = L(Ã), having the same read-and-write-domains as A.

3.2 An improved determinization construction

We consider in this section further mappings for both asynchronous models, which lead to determinization constructions with improved bounds w.r.t. size. More precisely, we obtain a size blow-up of 2^{n^{O(|Σ|)}} for the asynchronous cellular model, resp. 2^{n^{O(m)}} for the asynchronous one, where m is the number of processors. However, the correctness proof is more involved and the definition of these mappings is less intuitive. We denote in the following by Q_{Σ} the set of global states of an asynchronous cellular automaton A, Q_{Σ} = ∏_{a∈Σ} Q_{a}.

Proposition 3.9 Given a complete non-deterministic asynchronous cellular automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F). Let ρ: 𝕄(Σ, D) → P(Q_{Σ} × Q_{Σ} × P(Σ) × Σ) be defined for t ∈ 𝕄(Σ, D) by:

ρ(t) := {(q, q′, A, a) | ∃r ∈ R_{A}(t) : δ(r, ∂_{A}(t)) = q and δ(r, ∂_{A∪{a}}(t)) = q′}.

Then the mapping μ = (ν, ρ) is asynchronous. Moreover, we have

L(A) = {t ∈ 𝕄(Σ, D) | ∃q ∈ F : (q, q, Σ, a) ∈ ρ(t), ∀a ∈ Σ}.

Proof: Let first t = ∂_{D(a)}(t) and t′ = ta, for a ∈ Σ. Note that for X ⊆ Σ, ∂_{X}(t′) = ∂_{X}(t) if a ∉ X, resp. ∂_{X}(t′) = t′ if a ∈ X. For B ⊆ Σ, b ∈ Σ, and given μ(t) and a we define a set R as the least subset of Q_{Σ} × Q_{Σ} × P(Σ) × Σ satisfying the following:

1. If a ≠ b and a ∉ B, then let (q, q′, B, b) ∈ R if (q, q′, B, b) ∈ ρ(t).

2. If b = a ∉ B, then let (q, q′, B, b) ∈ R if some q′′ ∈ Q_{Σ} exists such that (q′′, q′′, Σ, a) ∈ ρ(t), q′ ∈ δ(q′′, a) and q′′ ∈ δ(q, ∂_{B}(t)^{−1}t). Note that the last condition can be checked by augmenting B stepwise by letters from D(a).

3. If a ∈ B, then let (q, q, B, a) ∈ R if q ∈ δ(q′, a), for some (q′, q′, Σ, a) ∈ ρ(t).

By the previous remark, it is easy to see that R ⊆ ρ(t′) holds. The converse inclusion ρ(t′) ⊆ R is immediate. For the second property of asynchronous mappings let A, B ⊆ Σ and consider t = ∂_{A∪B}(t) with t_{1} = ∂_{A}(t) = su, t_{2} = ∂_{B}(t) = sv, where alph(u) × alph(v) ⊆ I. We denote by C the alphabet C = {c ∈ Σ | ∂_{c}(t_{1}) = ∂_{c}(t_{2})}, and recall that C can be computed from the values ν(t_{1}), ν(t_{2}) of the labelling function ν. Recall further that s = ∂_{C}(s) = ∂_{C}(t_{i}), i = 1, 2. Let E ⊆ Σ, a ∈ Σ and assume without loss of generality ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1}). Let y = ∂_{E}(v) and note that we have ∂_{E}(t) = ∂_{E}(t_{1}v) = ∂_{E∪F} (t_{1})y, where F = D(alph(y)). The idea of this construction is to determine runs on ∂_{E}(t) by applying to more information than necessary in order to build the run (see also Fig. 2): we combine a run r_{1} ∈ R_{A}(∂_{E∪F} (t_{1})) with a run r_{2} ∈ R_{A}(∂_{C∪E}(t_{2})) to a run r on ∂_{E}(t) corresponding to r_{1} on ∂_{E∪F} (t_{1}), respectively to r_{2} on y. For the consistency note first that ∂_{f}(t_{1}) = ∂_{f}(s) for every f ∈ F, since F ⊆ D(alph(v)) and alph(u) × alph(v) ⊆ I. Moreover, in order to combine consistent runs we need the state reached by a run on ∂_{E}(t_{2}) = ∂_{E∪F} (s)y on the prefix ∂_{E∪F} (s) (actually, only the F -components are needed). This information cannot be provided by supplying the global state on ∂_{E}(t_{2}), only. Therefore, we consider the run r_{2} on the larger prefix ∂_{C∪E}(t_{2}) = sy, and we additionally assume the existence of a third run r_{3} on s, such that r_{2} is an extension of r_{3} and r_{1} agrees with r_{3} in the F -components.

[figure] [figure] [figure] [figure] [figure] [figure] [figure] [figure] [figure]  t_{1}t^{2} a ∂_{E}(t_{2})∂_{E}(t_{1}) yf ∈ F s

Figure 2: Forming runs on ∂_{E}(t).

Formally, consider a run r_{3} ∈ R_{A}(s) and let q_{1} = δ(r_{1}, ∂_{E∪F} (t_{1})), q_{2} = δ(r_{2}, ∂_{C∪E}(t_{2})), and q_{3} = δ(r_{3}, s). Suppose that q_{2} ∈ δ(q_{3}, y) and (q_{1})_{f} = (q_{3})_{f}, for every f ∈ F. We claim that the following mapping r: V (∂_{E}(t)) → ⋃_{a∈Σ} Q_{a}, which labels the vertex set V (∂_{E}(t)) of ∂_{E}(t) by local states, is a well-defined run on ∂_{E}(t):

r(w) := \{ \begin{matrix}r_{1}(w) & if w ∈ V (∂_{E∪F} (t_{1})) \\ r_{2}(w) & if w ∈ V (y), \end{matrix}

with V (∂_{E∪F} (t_{1})) resp. V (y) denoting the vertex set of ∂_{E∪F} (t_{1}) resp. y. To see the claim, note that given a run r′ on ∂_{C∪E}(t_{2}) = sy and a run r′′ on s with δ(r′, s)_{f} = δ(r′′, s)_{f} for all f ∈ F, we can combine r′, r′′ to a third run r′′′ on ∂_{C∪E}(t_{2}), corresponding to r′′ on s, resp. to r′ on y. This property is mainly due to F = D(alph(y)), together with the definition of read-domains of an asynchronous cellular automaton. Recall also ∂_{f,E∪F} (t_{1}) = ∂_{f}(t_{1}) = ∂_{f}(s), for f ∈ F. The global state q = δ(r, ∂_{E}(t)) associated to the run r defined above satisfies:

q_{e} = \{ \begin{matrix}(q_{2})_{e} & if ∂_{e,C}(t_{2}) < ∂_{e,E}(t_{2}) \\ (q_{1})_{e} & otherwise. \end{matrix}

Recall the assumption ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1}) and let r_{4} denote a run on ∂_{E∪F ∪{a}}(t_{1}) satisfying δ(r_{4}, ∂_{E∪F} (t_{1})) = q_{1} = δ(r_{1}, ∂_{E∪F} (t_{1})). Denote by q_{4} the state q_{4} = δ(r_{4}, ∂_{E∪F ∪{a}}(t_{1})). Similar to the run r, the mapping r′: V (∂_{E∪{a}}(t)) → ⋃_{a∈Σ} Q_{a} defined by

r′(w) := \{ \begin{matrix}r_{4}(w) & if w ∈ V (∂_{E∪F ∪\{a\}}(t_{1})) \\ r_{2}(w) & if w ∈ V (y) \end{matrix}

is a well-defined run on ∂_{E∪{a}}(t). Note that the run r′ yields the state q on the prefix ∂_{E}(t). For q′ = δ(r′, ∂_{E∪F ∪{a}}(t)) we have analogously to q:

q′_{e} = \{ \begin{matrix}(q_{2})_{e} & if ∂_{e,C}(t_{2}) < ∂_{e,E}(t_{2}) \\ (q_{4})_{e} & otherwise. \end{matrix}

Therefore, for ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1}) we let (q, q′, E, a) ∈ R if the following conditions are satisfied for some states q_{i} ∈ ∏_{a∈Σ} Q_{a}, 1 ≤ i ≤ 4:

1. (q_{1})_{f} = (q_{3})_{f}, for every f ∈ F = D(alph(∂_{E}(v))).

2. Let E = {e_{1}, …, e_{k}}, k ≥ 0, and C_{i} = C ∪ {e_{1}, …, e_{i}}, 0 ≤ i ≤ k (with C = C_{0}). Then we require the existence of a sequence q_{3} = p_{0}, p_{1}, …, p_{k} = q_{2} of global states satisfying (p_{i}, p_{i+1}, C_{i}, e_{i+1}) ∈ ρ(t_{2}), for all 0 ≤ i < k.

3. (q_{1}, q_{4}, E ∪ F, a) ∈ ρ(t_{1}).

4. • q_{e} = q′_{e} = (q_{2})_{e}, if ∂_{e,C}(t_{2}) < ∂_{e,E}(t_{2}).

• q_{e} = (q_{1})_{e} resp. q′_{e} = (q_{4})_{e}, if ∂_{e,E}(t_{2}) ≤ ∂_{e,C}(t_{2}).

By the remarks above we see R ⊆ ρ(t), whereas the converse inclusion is again immediate, using the fact that the transition relations of A are totally defined. Note also that the sets C, F and the conditions concerning the prefixes ∂_{a}(t_{2}), ∂_{a}(t_{1}), ∂_{e,E}(t_{2}), ∂_{e,C}(t_{2}) can be checked using the values ν(t_{1}), ν(t_{2}). □

Remark 3.10 The idea of the improved construction for asynchronous cellular automata based on Prop. 3.9 can be adapted also to asynchronous automata. Let A = ((Q_{i})_{i=1}^{m}, (δ_{a})_{a∈Σ}, q_{0}, F) denote an asynchronous automaton with readand-write domains dom(a) ⊆ [m], a ∈ Σ, and denote by Q_{[m]} the set of global states ∏_{i∈[m]} Q_{i}. We denote in the following by A_{i}, i ∈ [m], the dependence clique {a ∈ Σ | i ∈ dom(a)}, and let ∂_{i}(t), resp. ∂_{E}(t) (i ∈ [m], E ⊆ [m]) denote the prefix ∂_{A_{i}}(t), resp. ∂_{A_{E}}(t), where A_{E} = ∪_{i∈E}A_{i}. Consider the mapping ρ: 𝕄(Σ, D) → P(Q_{[m]} × Q_{[m]} × P([m]) × [m]) given by

ρ(t) := {(q, q′, E, i) | ∃r ∈ R_{A}(t) : δ(r, ∂_{E}(t)) = q and δ(r, ∂_{E∪{i}}(t)) = q′}.

Since the first property of asynchronous mappings can be easily verified for the above mapping, let us consider the second one. Suppose t = ∂_{A∪B}(t), with A, B ⊆ Σ, and let t_{1} = ∂_{A}(t) = su, t_{2} = ∂_{B}(t) = sv, where alph(u)×alph(v) ⊆ I. For E ⊆ [m], i ∈ [m] assume u ≠ 1 and ∂_{i}(t_{2}) ≤ ∂_{i}(t_{1}). We denote as in the proof of Prop. 3.9 y = ∂_{E}(v), and let F = ⋃_{b∈alph(y)} dom(b). Note that D(alph(y)) = ⋃_{i∈F} A_{i}, hence ∂_{E}(t) = ∂_{E}(t_{1}v) = ∂_{E∪F} (t_{1})y. Moreover, we have again ∂_{i}(t_{1}) = ∂_{i}(s), for every i ∈ F. It remains to define the set C accordingly. Let C′ = {c ∈ Σ | ∂_{c}(t_{1}) = ∂_{c}(t_{2})} ⊇ max(s) and define C = {j ∈ [m] | A_{j} ∩ C′ ≠ ∅, A_{j} ∩ alph(u) ≠ ∅}. Since u ≠ 1, we have for every c ∈ max(s): c ∈ D(alph(u)), hence max(s) ⊆ ⋃_{i∈C} A_{i}. Moreover, ∂_{C}(t_{2}) = ∂_{C}(s) = s, and for every i ∈ F: ∂_{i,C}(t_{2}) = ∂_{i}(s) = ∂_{i}(t_{1}) = ∂_{i,E∪F} (t_{1}). It is not difficult to show that μ = (ν, ρ) is asynchronous and that L(A) = μ^{−1}μ(L(A)). The details of the proof are left to the reader.

Prop. 3.9 and the above remark yield the improved constructions for asynchronous (asynchronous cellular, resp.) subset automata:

Theorem 3.11 1. Let A be a non-deterministic asynchronous cellular automaton of size n. Then a deterministic asynchronous cellular subset automaton Ã of size 2^{n^{O(|Σ|)}} effectively exists with L(A) = L(Ã).

2. Let A be a non-deterministic asynchronous automaton of size n with m processors. Then a deterministic asynchronous automaton Ã of size 2^{n^{O(m)}} effectively exists with L(A) = L(Ã), having the same read-and-write-domains as A.

We conclude this section with remarks concerning related subset constructions. As previously mentioned, Klarlund, Mukund and Sohoni presented independently a solution to the determinization problem for asynchronous automata [12]. Their construction yields a blow-up in size of 2^{n^{O(m^{3})}}, where n denotes the size of the input automaton (as the maximal size of local states sets) and m is the number of processors. This paper also contains a nice example for the lower bound of 2^{n^{m}/m}.

A less direct subset construction can be achieved by using an alternative determinization procedure given in [3]. Here, we view e.g. a non-deterministic asynchronous cellular automaton A as a sequential automaton with transition relation δ ⊆ Q × Σ^{∗} × Q, where |Q| ≤ n^{|Σ|} denotes the set of global states. After determinizing A (and possibly minimizing it) we obtain a deterministic automaton with at most 2^{n^{|Σ|}} states, having the I-diamond property (i.e., for every states q, q′ and letters (a, b) ∈ I: q′ = q·ab ⇔ q′ = q·ba). This sequential automaton can be used as input for the alternative construction of deterministic asynchronous automata mentioned above (see [3]). One obtains an equivalent asynchronous cellular automaton with at most 2^{O(n)^{|Σ|}} local states. For practical use, this offline approach may be less efficient than the direct constructions of Thm. 3.8 and [12], since simulating the subset automaton is done by table lookup instead of updating local information. Moreover, direct subset constructions are more flexible w.r.t. modifications of the input automaton or to partial determinization. Note also that direct constructions take only reachable local states into account.

4 Complementing Büchi asynchronous cellular automata

The complementation procedure for asynchronous cellular Büchi automata presented in this section applies the progress measure technique proposed by Klarlund [11], and uses the subset automaton construction given in Sect. 3. Progress measures have been devised in a more general setting for verifying sequential programs, and provide optimal complementation procedures for e.g. Büchi and Streett ω-automata. Our starting point is a slightly different Büchi acceptance condition, which restricts the accepted inputs to some set Inf(A), A ⊆ Σ, and specifies for each letter at most one local state to be repeated infinitely often. Formally, we consider a tuple A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, T ) with T ⊆ Q × P(Σ) × P(Σ), where Q = ∏_{a∈Σ} Q_{a}. A table element is a triple (p, A, {a_{1}, …, a_{k}}) satisfying the following condition: we require a_{i} ∈ A_{i} for every 1 ≤ i ≤ k, with A = ˙⋃_{i=1}^{k} A_{i} being the decomposition of A in connected components (i.e. every A_{i} induces a connected subgraph of (Σ, D) and A_{i} × A_{j} ⊆ I for i ≠ j). Throughout this section we use the standard representation for dependence graphs, introduced in Sect. 2. A run r ∈ R_{A}(t) on t is accepted by the table element (p, A, {a_{1}, …, a_{k}}) if

• A = alphinf(t) and

• For every a ∈ Ā ∪ {a_{1}, …, a_{k}} we have p_{a} ∈ inf_{a}(r), where inf_{a}(r) := {q_{a} ∈ Q_{a} | ∀n < |t|_{a} ∃n ≤ m < |t|_{a} : r(a, m) = q_{a}}.

Hence, this local acceptance condition specifies halting states for letters a ∉ alphinf(t) and recurrent states for the designated letters a_{i}. Note that an asynchronous cellular Büchi automaton with acceptance table T ⊆ ∏_{a∈Σ} P(Q_{a}) as defined in Sect. 2 can be easily transformed into an equivalent one with acceptance table as above: for t with alphinf(t) = A the letters a_{i} ∈ A_{i} can be used for checking that all local states from ⋃_{a∈A_{i}} T_{a} occur infinitely often, where T = (T_{a})_{a∈Σ} ∈ T . The converse transformation is straightforward, since we only have to check additionally that the input trace belongs to some (recognizable) set Inf(A), A ⊆ Σ. For t ∈ ℝ(Σ, D), a ∈ Σ, 0 ≤ n < |t|_{a}, let t[a, n] = ⊓{u ≤ t | |u|_{a} = n + 1} be the least prefix of t containing the first n+1 occurrences of a (note max(t[a, n]) = {a}, if |t|_{a} > 0). Furthermore, let us define U_{a}(t) ⊆ Q × ℕ by

U_{a}(t) = {(q, n) | 0 ≤ n < |t|_{a}, q ∈ δ(q_{0}, t[a, n])}.

U_{a}(t) is the vertex set of a directed graph containing the information about the global states reached by prefixes t[a, n], n ≥ 0. The edges are given by

(q, n) →^{a,t} (q′, n+1) for q ∈ U_{a}(t) and q′ ∈ δ(q, t[a, n]^{−1}t[a, n+1]), when n+1 < |t|_{a}.

Throughout this section we use the notion of transition graph with the meaning of a subgraph of (U_{a}(t), →^{a,t}). Moreover we use the abbreviation U_{i}(t) for U_{a_{i}}(t), 1 ≤ i ≤ k. The basic idea for Klarlund’s progress measure method is to express a global property of an infinite (transition) graph by the existence of a suitable mapping, which associates with each vertex a finite amount of information. This information quantifies progress towards satisfying the required condition. For complementing e.g. Büchi automata, the condition expresses that certain states are visited finitely often, i.e. they are not recurrent. In our distributed setting, we have to assume the existence of several progress measures, one for each connected component of alphinf(t) (i.e., for each designated letter). The next proposition gives the basis for the complementation procedure. Recall Q = ∏_{a∈Σ} Q_{a} and let N := |Q|. Let F_{i} := {q = (q_{a})_{a∈Σ} ∈ Q | q_{a_{i}} = p_{a_{i}}}, where p ∈ Q will be the first component in the unique element of the table of the given automaton.

Proposition 4.1 Let A = ˙⋃_{i=1}^{k} A_{i} be the decomposition in connected components of A ⊆ Σ, a_{i} ∈ A_{i}, for all i, and p ∈ Q. Let A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, {T }) be an asynchronous cellular Büchi automaton, with T = (p, A, {a_{1}, …, a_{k}}). Then t ∈ Inf(A) \ L(A) holds if and only if there exists a family of transition graphs (V_{i}(t), E_{i}(t)), together with associated mappings Φ_{i}: U_{i}(t) → {0, …, 2N + 1}, 1 ≤ i ≤ k, such that the following conditions hold for each i:

1. (V_{i}(t), E_{i}(t)) is the subgraph of the transition graph (U_{i}(t), →^{a_{i},t}) induced by V_{i}(t) = U_{i}(t) \ Φ_{i}^{−1}(2N + 1).

2. Φ_{i}: U_{i}(t) → {0, 1, …, 2N + 1} satisfies for every (q, n), (q′, n + 1) ∈ U_{i}(t)

with (q, n) →^{a_{i},t} (q′, n + 1):

• Φ_{i}(q, n) ≥ Φ_{i}(q′, n + 1)

• Φ_{i}(q, n) = Φ_{i}(q′, n + 1) ⟹ q′ ∉ F_{i} or Φ_{i}(q, n) ∈ {0, 2, …, 2N} ∪ {2N + 1}.

3. Let ((q_{n}, n))_{n≥n_{0}} ⊆ V_{i}(t) be an infinite sequence with (q_{n}, n) →^{a_{i},t} (q_{n+1}, n+1),

n ≥ n_{0}. Then

lim_{n→∞} Φ_{i}(q_{n}, n) ∈ {1, 3, …, 2N − 1} .

4. There exists a finite prefix t_{0} ≤ t, t_{0} ∈ 𝕄(Σ, D), with |t_{0}|_{a} = |t|_{a} for every a ∈ Ā, such that every run r ∈ R_{A}(t_{0}) satisfies

• either δ(r, t_{0})_{a} ≠ p_{a} for some a ∈ Ā,

• or (q_{i}, n_{i}) ∈ V_{i}(t) for some 1 ≤ i ≤ k, where q_{i} = δ(r, ∂_{a_{i}}(t_{0})) and n_{i} = |t_{0}|_{a_{i}} − 1.

Remark 4.2 Following Klarlund’s construction for Büchi ω-automata [11], each mapping Φ_{i} is a quasi-progress measure for the subgraph (V_{i}(t), E_{i}(t)). Note that since Φ_{i} is decreasing w.r.t the transition relation →^{a_{i},t}, every transition graph (V_{i}(t), E_{i}(t)) is downward closed, i.e. for (q, n) ∈ V_{i}(t) and (q′, n+1) with (q, n) →^{a_{i},t} (q′, n + 1) we have (q′, n + 1) ∈ V_{i}(t), too.

Condition 4 corresponds to a safety requirement. It guarantees that computations which reach the final halting state for each letter a ∉ A and which are not captured by some quasi-progress measure Φ_{i} can not be synchronized to a run on t. The existence of Φ_{i} ensures that the local state p_{a_{i}} is not recurrent (for a subset of runs on t). This means that we eliminate every possibility for runs r ∈ R_{A}(t) on t to be accepting.

Proof of 4.1: Let t ∈ Inf(A). Assume that a family of transition graphs (V_{i}(t), E_{i}(t)) exists, together with associated mappings Φ_{i}, 1 ≤ i ≤ k, satisfying the conditions of the proposition. Let r ∈ R_{A}(t) be a run on t. It suffices to consider the case where for some connected component 1 ≤ i ≤ k and some n ∈ ℕ we have (δ(r, t[a_{i}, n]), n) ∈ V_{i}(t) (hence, also (δ(r, t[a_{i}, m]), m) ∈ V_{i}(t) holds, for every m ≥ n). Due to Φ_{i} being decreasing (Cond. (2)) and taking values in a finite set, we may assume with q_{m} := δ(r, t[a_{i}, m]) that we have Φ_{i}(q_{m}, m) = Φ_{i}(q_{n}, n) for every m ≥ n. With Cond. (3) we obtain Φ_{i}(q_{n}, n) ∉ {0, 2, …, 2N}∪{2N +1}, hence by Cond. (2), q_{m} ∉ F_{i} for all m ≥ n. Therefore, the run r ∈ R_{A}(t) is rejecting. Hence, t ∉ L(A).

For the converse direction, let t ∈ Inf(A) \ L(A) and let 1 ≤ i ≤ k be fixed. We follow [11] and define the mappings Φ_{i} in two steps. First, progress measures Φ̃_{i} with values in the set of countable ordinals ω_{1} are defined by transfinite induction. In the present setting, we simultaneously define the computation graphs (V_{i}(t), E_{i}(t)). For a set V ⊆ U_{i}(t) we denote in the following by N_{V} (q, n) the set of proper successors of (q, n) ∈ U_{i}(t) from U_{i}(t) \ V, i.e.,

N_{V} (q, n) := {(q′, m) | m > n, ∃q = q_{n}, q_{n+1}, …, q_{m} = q′, (q′, m) ∈ U_{i}(t) \ V

with (q_{k}, k) →^{a_{i},t} (q_{k+1}, k + 1), for every n ≤ k < m} .

The transition graph (V_{i}(t), E_{i}(t)) and the progress measure Φ̃_{i}: U_{i}(t) → ω_{1} are now defined inductively: let V_{0} = V_{i}(t) = ∅. Assume that for β < ω_{1}, the sequence (V_{α})_{α<β} of pairwise disjoint subsets of U_{i}(t) is already defined, with V_{i}(t) = ∪_{α<β}V_{α}. If either U_{i}(t) = V_{i}(t), or N_{V_{i}(t)}(q, n)∩(F_{i}×ℕ) ≠ ∅ holds for all (q, n) ∈ U_{i}(t)\V_{i}(t), then let V_{β} := U_{i}(t) \ V_{i}(t) and V_{γ} := ∅ for every β < γ < ω_{1} and we are done. Otherwise choose (q, n) ∈ U_{i}(t) \ V_{i}(t) satisfying N_{V_{i}(t)}(q, n) ∩ (F_{i} × ℕ) = ∅ and define

V_{β} := \{ \begin{matrix}\{(q, n)\} & if N_{V_{i}(t)}(q, n) = ∅ \\ N_{V_{i}(t)}(q, n) & otherwise, \end{matrix}

updating V_{i}(t) := V_{i}(t) ∪ V_{β}. The decomposition of U_{i}(t) in pairwise disjoint sets naturally induces a mapping Φ̃_{i}: U_{i}(t) → ω_{1}. Let Φ̃_{i}(q, n) = β if (q, n) ∈ V_{β}. It is easy to see that Φ̃_{i} is decreasing w.r.t. the transition relation →^{a_{i},t}, due to the definition by means of successors in the transition graph. Moreover, suppose Φ̃_{i}(q, n) = Φ̃_{i}(q′, n + 1) holds for (q, n) ∈ V_{i}(t), with (q, n) →^{a_{i},t} (q′, n + 1). Then we have

q′ ∉ F_{i} .  (1)

By construction we obtain a countable ordinal β_{0} with V_{β_{0}} = U_{i}(t) \ V_{i}(t), such that β_{0} = ⊔{α < ω_{1} | V_{α} ≠ ∅}. Note that we have either V_{β_{0}} = ∅, or for every (s_{n}, n) ∈ V_{β_{0}} there is an infinite transition path (s_{n}, n) →^{a_{i},t} (s_{n+1}, n + 1) →^{a_{i},t} ⋯ in the subgraph induced by V_{β_{0}}, repeating infinitely often some state from F_{i}, i.e.,

|{m ≥ n | (s_{m})_{a_{i}} = p_{a_{i}}}| = ∞ .  (2)

The second step of Klarlund’s construction [11] uses the bounded width N of the given transition graph for modifying the progress measure to a quasi-progress measure mapping with finite range. Given α < ω_{1}, let the predicate const(α) be true, if there is an infinite path (q_{n}, n) →^{a_{i},t} (q_{n+1}, n + 1) →^{a_{i},t} ⋯ in the transition graph U_{i}(t), such that Φ̃_{i}(q_{m}, m) = α for every m ≥ n. Since these infinite paths are disjoint one obtains a set of at most N countable ordinals 0 < α_{1} < ⋯ < α_{M} < ω_{1} (M ≤ N) satisfying const(α_{i}), 1 ≤ i ≤ M. Let α_{0} = 0, α_{M+1} = ω_{1} and define Φ_{i}: U_{i}(t) → {0, 1, …, 2N + 1} for (q, n) ∈ V_{i}(t) as

Φ_{i}(q, n) := \{ \begin{matrix}2k − 1 & if Φ̃_{i}(q, n) = α_{k}, 1 ≤ k ≤ M \\ 2k & if α_{k} < Φ̃_{i}(q, n) < α_{k+1}, 0 ≤ k ≤ M . \end{matrix}

For (q, n) ∈ U_{i}(t) \ V_{i}(t) let Φ_{i}(q, n) = 2N + 1. The mapping Φ_{i} satisfies the condition of real progress (Cond. (3)): assume by contradiction that an infinite transition path (q_{n}, n) →^{a_{i},t} (q_{n+1}, n + 1) →^{a_{i},t} ⋯ exists in U_{i}(t), such that Φ_{i}(q_{m}, m) = 2k holds for some k and every m ≥ n. With Φ̃_{i} being decreasing and by the definition of Φ_{i}, some α_{k} < α < α_{k+1} would exist with lim_{m→∞} Φ̃_{i}(q_{m}, m) = α. Thus, const(α) follows, contradicting the definition of {α_{1}, …, α_{M}}. The mapping Φ_{i} is obviously decreasing, since Φ̃_{i} already was. Moreover, suppose we have (q, n) →^{a_{i},t} (q′, n + 1) with Φ_{i}(q, n) = Φ_{i}(q′, n + 1) ≠ 2N + 1 and q′ ∈ F_{i}. By Eq. (1) we obtain Φ̃_{i}(q, n) > Φ̃_{i}(q′, n + 1). Hence, Φ_{i}(q, n) ∉ {0, 2, …, 2N} leads to a contradiction.

Finally, we show that runs which are not covered by the quasi-progress measures (Φ_{i})_{1≤i≤k} cannot be synchronized (Cond. 4). Let us assume by contradiction that for every tuple (n_{i})_{1≤i≤k} ∈ ℕ^{k} there exist global states (q_{i})_{1≤i≤k} ∈ Q^{k} and a run

r ∈ R_{A}(t_{0}) on the (finite) prefix t_{0} = ⨆_{1≤i≤k} t[a_{i}, n_{i}] ⊔ ⨆_{a∈Ā} t[a, |t|_{a} − 1] of t with

• (q_{i}, n_{i}) ∈ U_{i}(t) \ V_{i}(t) for every 1 ≤ i ≤ k,

• δ(r, t[a_{i}, n_{i}]) = q_{i} for every 1 ≤ i ≤ k, and

• δ(r, t_{0})_{a} = p_{a} for every a ∈ Ā.

For large enough values of n_{i}, 1 ≤ i ≤ k, we have max(t_{0})∩A = {a_{1}, …, a_{k}}, due to t ∈ Inf(A) and the way we choosed the designated letters a_{i}. Let t = t_{0}t_{1} ⋯ t_{k} with alph(t_{i}) = A_{i} for every i. Due to (q_{i}, n_{i}) ∈ U_{i}(t) \ V_{i}(t) we obtain by Eq. (2) an infinite path π_{i} in the subgraph of (U_{i}(t), →^{a_{i},t}) induced by U_{i}(t)\V_{i}(t), such that π_{i} starts in (q_{i}, n_{i}) and visits infinitely often the set F_{i} × ℕ. Since alph(t_{0}^{−1}t) = A every path π_{i} defines (a set of) runs on the connected suffix t_{i} of t, starting with the state q_{i} . Moreover, every run r_{i} associated to π_{i} repeats infinitely often the local state p_{a_{i}}. For each i we choose a run r_{i} on t_{i} associated to π_{i} as above. With V_{i}, 0 ≤ i ≤ k, denoting the vertex set of t_{i} in the dependence graph of t, we define r′ ∈ R_{A}(t) by r′|_{V_{0}} := r and r′|_{V_{i}} := r_{i}, 1 ≤ i ≤ k. Obviously, we obtained an accepting run on t, since p_{a} ∈ inf_{a}(r′) for every a ∈ Ā ∪ {a_{1}, …, a_{k}}. Hence, a contradiction follows. □

We are now ready to define an asynchronous cellular Büchi automaton B such that L(B) = \overline{L(A)} ∩ Inf(A), where A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, \{T \}) is an asynchronous cellular Büchi automaton with a single element T = (p, A, {a_{1}, …, a_{k}}) in T . Following [11], the automaton B guesses the values of the quasi-progress measures. In this setting B guesses at the same time the transition graphs (V_{i}(t), E_{i}(t)) covered by Φ_{i}. The automaton recognizing the complement language relies on the subset automaton of the given asynchronous cellular automaton ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}), defined in Sect. 3 for an asynchronous mapping μ = (ν, ρ) (we omit final states).

Let A_{μ} = ((Q̃_{a})_{a∈Σ}, (δ̃_{a})_{a∈Σ}, q̃_{0}) denote the subset automaton obtained from μ. In the following we denote by [2N + 1]^{Q} the set of partial mappings from Q to {0, 1, …, 2N + 1} (recall Q = ∏_{a∈Σ} Q_{a}). Furthermore, dom(f) denotes the domain of f ∈ [2N + 1]^{Q}. We recall the notation q →^{(a)} q′ from Sect. 3, which means that for some t ∈ 𝕄(Σ, D) a run r ∈ R_{A}(∂_{a}(ta)) exists, with q = δ(r, ∂_{a}(t)) and q′ = δ(r, ∂_{a}(ta)). Let B = ((S_{a})_{a∈Σ}, (Δ_{a})_{a∈Σ}, J , T ) be defined as follows (with J denoting the set of initial states):

1.

S_{a} = \{ \begin{matrix}Q̃_{a} & if a ∉ \{a_{1}, …, a_{k}\} \\ Q̃_{a} × [2N + 1]^{Q} × P(Q) & otherwise \end{matrix}

Moreover, for every a ∈ {a_{1}, …, a_{k}} and (q̃_{a}, α_{a}, A_{a}) ∈ S_{a} let

dom(α_{a}) = {δ(r, u) | ∃u ∈ 𝕄(Σ, D), u = ∂_{a}(u), δ̃(q̃_{o}, u)_{a} = q̃_{a} and r ∈ R_{A}(u)}.

For the subset construction of Prop. 3.4, the above condition is equivalent to the following one: if q̃_{a} = (ν(u), ρ(u)), then we let (f(b, a))_{b∈Σ} ∈ dom(α_{a}), for some f ∈ ρ(u). If we use instead the subset construction given in Prop. 3.9 then we simply let q ∈ dom(α_{a}), whenever (q, q, {a}, a) ∈ ρ(u).

2. For a ∉ {a_{1}, …, a_{k}} let s′_{a} ∈ Δ_{a}((s_{b})_{b∈D(a)}) if s′_{a} = δ̃_{a}((q̃_{b})_{b∈D(a)}), where s_{b} = q̃_{b} or s_{b} = (q̃_{b}, α_{b}, A_{b}) for some α_{b} ∈ [2N + 1]^{Q}, A_{b} ⊆ Q, for all b ∈ D(a).

For a = a_{i} (1 ≤ i ≤ k), let s_{a} = (q̃_{a}, α_{a}, A_{a}) and s′_{a} = (q̃′_{a}, α′_{a}, A′_{a}). Then s′_{a} ∈ Δ_{a}((s_{b})_{b∈D(a)}) if

• q̃′_{a} = δ̃_{a}((q̃_{b})_{b∈D(a)}), for q̃_{b} = s_{b}, b ∈ D(a) \ {a} (note that D(a) ∩ {a_{1}, …, a_{k}} = {a});

• For every q ∈ dom(α_{a}), q′ ∈ dom(α′_{a}) such that q →^{(a)} q′ we require that

both conditions below hold: i. α_{a}(q) ≥ α′_{a}(q′) ii. α_{a}(q) = α′_{a}(q′) implies q′_{a} ≠ p_{a} or α_{a}(q) ∈ {0, 2, …, 2N} or α_{a}(q) =

2N + 1.

• A′_{a} = \{ \begin{matrix}dom(α′_{a}) & if A_{a} = ∅ \\ \{q′ ∈ dom(α′_{a}) | ∃q ∈ dom(α_{a}) ∩ A_{a} with \\ q →^{(a)} q′ and α_{a}(q) = α′_{a}(q′) ∈ \{0, 2, …, 2N\}\} & otherwise \end{matrix}

3. The table T is given by (z, A, {a_{1}, …, a_{k}}) ∈ T if and only if for some u ∈ 𝕄(Σ, D) with q̃_{a} = (ν(∂_{a}(u)), ρ(∂_{a}(u))), a ∈ Σ, and mappings α_{a} ∈ [2N + 1]^{Q}, a ∈ {a_{1}, …, a_{k}} both conditions below are satisfied:

1. z_{a} = (q̃_{a}, α_{a}, ∅), for a ∈ {a_{1}, …, a_{k}}, respectively z_{a} = q̃_{a} for a ∉

{a_{1}, …, a_{k}}.

2. Let M = Ā ∪ {a_{1}, …, a_{k}}. Then we require for every r ∈ R_{A}(∂_{M}(u)):

• either δ(r, ∂_{M}(u))_{a} ≠ p_{a}, for some a ∈ Ā,

• or α_{a}(δ(r, ∂_{a}(u))) ≠ 2N + 1, for some a ∈ {a_{1}, …, a_{k}}.

The conditions above can be easily checked using our subset automata constructions (Prop. 3.4, 3.9).

4. Let s_{0} ∈ J be an initial state if (s_{0})_{a} = (q̃_{0})_{a}, resp. (s_{0})_{a} = ((q̃_{0})_{a}, α_{a}, ∅), for some α_{a} ∈ [2N + 1]^{Q}.

Proposition 4.3 Let A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, {T }) be an asynchronous cellular Büchi automaton with a single table element T = (p, A, {a_{1}, …, a_{k}}). Let B be defined as above. Then L(B) = \overline{L(A)} ∩ Inf(A).

Proof: Let us first assume t ∈ Inf(A) \ L(A). We apply Prop. 4.1 and obtain transition graphs (V_{i}(t), E_{i}(t))_{1≤i≤k}, together with quasi-progress measures (Φ_{i})_{1≤i≤k} satisfying the properties in 4.1. The definition of an accepting B-run r on t follows immediately:

1. For a ∉ {a_{1}, …, a_{k}}, 0 ≤ n < |t|_{a}, let r(a, n) = δ̃(q̃_{0}, t[a, n])_{a}.

2. For a = a_{i}, 1 ≤ i ≤ k and n ≥ 0 let r(a, n) = (q̃_{a}, α_{a}, A_{a}), where

• q̃_{a} = δ̃(q̃_{0}, t[a, n])_{a};

• Let q̃_{a} = (ν(u), ρ(u)) for some u = ∂_{a}(u). Then dom(α_{a}) = {q ∈ Q | ∃r ∈ R_{A}(u) : δ(r, u) = q}. For the construction given in Prop. 3.4 (resp. Prop. 3.9) this means q ∈ dom(α_{a}) if and only if q = (f(b, a))_{b∈Σ} for some f ∈ ρ(u) (resp. (q, q, {a}, a) ∈ ρ(u)).

• For all q ∈ dom(α_{a}) let α_{a}(q) = Φ_{i}(q, n).

The local state component A_{a} being computed deterministically, we note that the limit condition (Cond. (3)) in Prop. 4.1 implies for some u ∈ 𝕄(Σ, D) and partial mappings α_{a}, a ∈ {a_{1}, …, a_{k}}, that the local states (p̃_{a}, α_{a}, ∅) with p̃_{a} = (ν(∂_{a}(u)), ρ(∂_{a}(u))) are repeated infinitely often. Otherwise, by the same argument as in [11] we would obtain using König’s Lemma an infinite path in (U_{i}(t), →^{a_{i},t}) with a constant Φ_{i}-value from {0, 2, …, 2N}. For a ∈ Ā assume w.l.o.g. that the state (ν(∂_{a}(u)), ρ(∂_{a}(u))) labels the last avertex in t, i.e. (a, |t|_{a} − 1). Finally, the synchronization condition (Cond. 4) in 4.1 ensures that there is no run r ∈ R_{A}(∂_{M}(u)) satisfying both δ(r, ∂_{M}(u))_{a} = p_{a}, for all a ∈ Ā, and α_{a}(δ(r, ∂_{a}(u))) ≠ 2N + 1 for all a ∈ {a_{1}, …, a_{k}} (recall that α_{a_{i}}(q) = 2N + 1, for all q ∉ V_{i}(t)). For the converse let t ∈ L(B) be accepted by a B-run r by (z, A, {a_{1}, …, a_{k}}) ∈ T , hence alphinf(t) = A. Once again, there is a canonical definition for (V_{i}(t), E_{i}(t)) and Φ_{i}, 1 ≤ i ≤ k. For a = a_{i}, n ≥ 0, let (q̃_{a}, α_{a}, A_{a}) = Δ(r, t[a, n])_{a}. Furthermore, for q ∈ dom(α_{a}) define (q, n) ∈ V_{i}(t) if and only if α_{a}(q) ≠ 2N + 1 and let Φ_{i}(q, n) = α_{a}(q). Since for any a ∈ {a_{1}, …, a_{k}}, z_{a} = (q̃_{a}, α_{a}, ∅) for some q̃_{a} ∈ Q̃_{a}, α_{a} ∈ [2N + 1]^{Q}, we directly obtain that the real progress condition (Cond. (3)) from Prop. 4.1 holds. Finally, let u ∈ 𝕄(Σ, D), u < t be such that Δ(r, u)_{a} = z_{a} for a ∈ Ā ∪ {a_{1}, …, a_{k}} and max(u) ∩ A = {a_{1}, …, a_{k}}. Then with n_{i} = |u|_{a_{i}} − 1, 1 ≤ i ≤ k, we satisfy Cond. 4 in Prop. 4.1, too. □

For the size of the automaton recognizing the complement language note that the size of every local state set S_{a} of B is dominated by the size obtained for asynchronous cellular subset automata. Hence, by the construction based on Prop. 3.9 we obtain the bound 2^{N^{O(1)}}, where the exponent of N is independent of the alphabet size. The lower bound for the complementation of Büchi ω-automata is 2^{N log N} [15].

Theorem 4.4 Given a non-deterministic asynchronous cellular Büchi automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, T ) with table T ⊆ (∏_{a∈Σ} Q_{a}) × P(Σ) × P(Σ), and N = | ∏_{a∈Σ} Q_{a}| global states. Then an asynchronous cellular Büchi automaton B = ((S_{a})_{a∈Σ}, (Δ_{a})_{a∈Σ}, s_{0}, T′), with table T′ ⊆ (∏_{a∈Σ} S_{a}) × P(Σ) × P(Σ) effectively exists, such that L(B) = \overline{L(A)}. The automaton B has 2^{N^{O(1)}} global states.

The construction of Prop. 4.3 can be adapted smoothly to asynchronous Büchi automata, similar to our subset constructions. Based on the subset constructions for asynchronous automata, the size blow-up obtained for the complementation procedure is again dominated by the subset automaton. Note that we can also start with an asynchronous Büchi automaton A (with modified acceptance condition) and use the asynchronous mapping ρ based on the asynchronous automaton A (given in Rem. 3.10) in the definition of B. This yields an asynchronous cellular automaton B accepting the complement language and having local states sets of size 2^{n^{O(m)}} = 2^{N^{O(1)}}, with N denoting the number of global states. Finally, by the standard embedding we transform B into an equivalent asynchronous automaton B′ still having 2^{N^{O(1)}} global states. Asynchronous (cellular) automata viewed as sequential automata satisfy the Idiamond property, as we already mentioned in Sect. 2. This means that for every pair of states q, q′ and independent letters (a, b) ∈ I: q′ ∈ δ(q, ab) holds if and only if q′ ∈ δ(q, ba). This property expresses a reduced view of concurrency, the interleaving viewpoint. We note that non-deterministic Büchi ω-automata satisfying the I-diamond property which accept closed languages from Σ^{∞} characterize precisely Rec(ℝ(Σ, D)) (a language L is closed if φ^{−1}(φ(L)) = L, with φ denoting the canonical mapping). If we were only interested in Büchi automata A with I-diamond property, then we could apply for complementing A a simple construction proposed by Pécuchet [17]. All we need is a homomorphism h: Σ^{∗} → S to a finite monoid recognizing L(A) and satisfying h(ab) = h(ba), for all (a, b) ∈ I. Then the size of the automaton for the complement language obtained in [17] is O(|S|^{2}). Note that the syntactic morphism of a closed language L ⊆ Σ^{∞} satisfies this property. Moreover, the size of the syntactic monoid of L is bounded by 2^{O(N^{2})}, with N denoting the size of A.

Acknowledgment: I wish to thank Volker Diekert and Paul Gastin for interesting discussions and Wolfgang Thomas for pointing out the work of J.-P. Pécuchet. I also thank the referees from ICALP’93 and especially from Theoretical Computer Science for the comments which led to an improved presentation of this paper.

References

[1] P. Cartier and D. Foata. Problèmes combinatoires de commutation et réarrangements. Number 85 in Lecture Notes in Mathematics. Springer, Berlin-Heidelberg-New York, 1969.

[2] R. Cori and Y. Métivier. Approximation of a trace, asynchronous automata and the ordering of events in a distributed system. In Proceedings of the 15th International Colloquium on Automata, Languages and Programming (ICALP’88), number 317 in LNCS, pages 147–161. Springer, 1988.

[3] R. Cori, Y. Métivier, and W. Zielonka. Asynchronous mappings and asynchronous cellular automata. Information and Computation, 106:159–202, 1993.

[4] V. Diekert. Combinatorics on Traces. Number 454 in Lecture Notes in Computer Science. Springer, Berlin-Heidelberg-New York, 1990.

[5] V. Diekert and W. Ebinger, editors. Infinite Traces. Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Tübingen, Germany, 1992, Bericht 4/92. Universität Stuttgart, Fakultät Informatik, 1992.

[6] V. Diekert and A. Muscholl. Deterministic asynchronous automata for infinite traces. Acta Informatica, 31:379–397, 1994. A preliminary version was presented at STACS’93, Lecture Notes in Computer Science 665 (1993).

[7] V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

[8] W. Ebinger and A. Muscholl. Logical definability on infinite traces. Theoretical Computer Science, 154:67–84, 1996. A preliminary version was presented at ICALP’93, Lecture Notes in Computer Science 700 (1993).

[9] P. Gastin. Recognizable and rational trace languages of finite and infinite traces. In C. Choffrut et al., editors, Proceedings of the 8th Annual Symposium on Theoretical Aspects of Computer Science (STACS’91), Hamburg 1991, number 480 in Lecture Notes in Computer Science, pages 89–104, Berlin-Heidelberg-New York, 1991. Springer.

[10] P. Gastin and A. Petit. Asynchronous automata for infinite traces. In W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP’92), Vienna (Austria) 1992, number 623 in Lecture Notes in Computer Science, pages 583–594, Berlin-Heidelberg-New York, 1992. Springer.

[11] N. Klarlund. Progress measures for complementation of ω-automata with applications to temporal logic. In Proc. of the 32nd Symposium on Foundations of Computer Science, Oct. 1-4, 1991, San Juan, Puerto Rico, pages 358–367, 1991.

[12] N. Klarlund, M. Mukund, and M. Sohoni. Determinizing asynchronous automata. In S. Abiteboul and E. Shamir, editors, Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP’94), Jerusalem (Israel) 1994, number 820 in Lecture Notes in Computer Science, pages 130–141, 1994.

[13] A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.

[14] A. Mazurkiewicz. Trace theory. In W. Brauer et al., editors, Petri Nets, Applications and Relationship to other Models of Concurrency, number 255 in Lecture Notes in Computer Science, pages 279–324, Berlin-Heidelberg-New York, 1987. Springer.

[15] M. Michel. Complementation is more difficult with automata on infinite words. Manuscript., 1988.

[16] A. Muscholl. On the complementation of Büchi asynchronous cellular automata. In S. Abiteboul and E. Shamir, editors, Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP’94), Jerusalem (Israel) 1994, number 820 in Lecture Notes in Computer Science, pages 142–153. Springer, 1994.

[17] J.-P. Pécuchet. On the complementation of Büchi automata. Theor. Comp. Science, (47):95–98, 1986.

[18] G. Pighizzini. Personal communication, 1993.

[19] G. Pighizzini. Recognizable trace languages and asynchronous automata. PhD thesis, Università di Milano, February 1993.

[20] S. Safra. On the complexity of ω-automata. In Proc. of the 29th Symposium on Foundations of Computer Science, pages 319–327, 1988.

[21] W. Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications, 21:99–135, 1987.