Über die

Erkennbarkeit unendlicher Spuren

Von der Fakultät Informatik der Universität Stuttgart zur Erlangung

der Würde eines Doktors der Naturwissenschaften genehmigte Abhandlung

Vorgelegt von

Anca Muscholl

aus Bukarest

Hauptberichter: Prof. Dr. V. Diekert Mitberichter: Prof. Dr. V. Claus Mitberichter: Prof. Dr. J-E. Pin

Tag der mündlichen Prüfung: 7. Februar 1994

Stuttgart, 1994

Danksagung

Ich danke meinen Kollegen der beiden Theorie-Abteilungen für ihr konstantes Interesse an meinen Themen, insbesondere danke ich Werner Ebinger für eine sehr gute Zusammenarbeit.

Für die tatkräftige redaktionelle Unterstützung geht ein besonderer Dank an Dan Teodosiu und Markus Stolpmann.

Dank der intensiven Unterstützung von Prof. V. Diekert konnte die vorliegende Arbeit in so kurzer Zeit fertiggestellt werden. Seinem regen Interesse und seiner Fähigkeit zum Zuhören verdanke ich sehr viel.

Mein größter Dank gilt Matthias für seine riesige Unterstützung.

Zusammenfassung

Unendliche Spuren stellen einen geeigneten Rahmen für die Untersuchung nichtterminierender nebenläufiger Systeme dar. Eine besonders wichtige Eigenschaft dabei ist die endliche Kontrollierbarkeit (Erkennbarkeit) des Verhaltens der Systeme. Unter den vielfältigen Charakterisierungen von Erkennbarkeit im Kontext unendlicher Spuren fehlte lange Zeit ein geeignetes Akzeptormodell, d.h. ein auf Automaten mit verteilter Kontrolle basierendes deterministisches Modell. Wir beantworten diese wichtige Frage in der vorliegenden Arbeit, indem wir die Klasse erkennbarer Sprachen unendlicher Spuren durch deterministische asynchrone Muller Automaten charakterisieren. Damit verallgemeinern wir das Theorem von McNaughton über unendliche Wörter auf unendliche Spuren. Wir definieren deterministische Sprachen unendlicher Spuren, und zeigen die Äquivalenz zwischen Erkennbarkeit und dem Booleschen Abschluß dieser Sprachklasse. Die Komplementierung nichtdeterministischer Büchi Automaten ist bereits im Fall der unendlichen Wörter ein wichtiges Problem mit interessanten Lösungen. Wir erweitern die Methode des Fortschrittsmaßes von N. Klarlund auf asynchron-zelluläre Automaten. Voraussetzung war, daß wir eines der offenen Problemen im Bereich endlicher Spuren lösen, indem wir eine Potenzautomaten-Konstruktion für asynchron-zelluläre Automaten angeben. Diese wird anschließend für die Komplementierung verwendet, um die Konstruktion möglichst effizient durchzuführen.

Inhaltsverzeichnis

Einleitung

1 Spursprachen und Erkennbarkeit 9 1.1 Erkennbarkeit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.2 Asynchrone Automaten . . . . . . . . . . . . . . . . . . . . . . . . 13 1.3 Erkennbare Sprachen reeller Spuren . . . . . . . . . . . . . . . . . 16

2 Das Theorem von McNaughton für IR(Σ, D) 23 2.1 Algebraische Eigenschaften in Rec(IR) . . . . . . . . . . . . . . . . 23 2.2 Äquivalenz von Rec(IR) und dem Booleschen Abschluß der Familie

deterministischer Sprachen . . . . . . . . . . . . . . . . . . . . . . 30 2.3 Deterministische asynchrone Muller Automaten . . . . . . . . . . 32

3 Deterministische reelle Spursprachen 37 3.1 Abschlußeigenschaften deterministischer Sprachen . . . . . . . . . 37 3.2 Deterministische Automaten für DRec(IR) . . . . . . . . . . . . . 38 3.3 DRec(IR) und I-Diamant Büchi Automaten . . . . . . . . . . . . 40

4 Sternfreie und aperiodische reelle Spursprachen 43

5 Komplementierung asynchroner Büchi Automaten 49 5.1 Determinisierung asynchron-zellulärer Automaten . . . . . . . . . 49 5.2 Komplementierung asynchron-zellulärer Büchi Automaten …. 53

6 I-Diamant Automaten 61 6.1 Deterministische I-Diamant Muller Automaten . . . . . . . . . . 62 6.2 Nichtdeterministische I-Diamant Büchi Automaten . . . . . . . . 67

Abschließende Bemerkungen und Ausblick

Literaturverzeichnis

Index 2

Einleitung

Das Verhalten nebenläufiger Systeme, zusammen mit der Problematik des Entwurfs, der Analyse und der Verifikation verteilter Algorithmen, stellt eine Grundherausforderung an die formalen Methoden der Informatik dar. Eine fundierte Behandlung nebenläufiger Systeme kann jedoch erst in einem formalen Rahmen erfolgen. Dort herrscht genügend Abstraktion, um Eigenschaften mit mathematischen Instrumenten präzise formulieren und überprüfen zu können. Eines der frühesten formalen Modelle für parallele Systeme wurde Anfang der 60’er Jahre von C. A. Petri vorgestellt. Petri-Netze drücken Parallelität in Form von kooperierenden, verteilten Aktionen aus. Sie stellen auch den Ausgangspunkt der Theorie der Spuren dar, die in Zusammenhang mit dem Verhalten sicherer Petri-Netze durch A. Mazurkiewicz [Maz77] eingeführt wurde. Die Spurtheorie hat sich seither als geeigneter Rahmen für die Untersuchung paralleler Systeme erwiesen. Das Konzept der Spuren formalisiert auf einfache Art den Kern eines nebenläufigen Systems in Form einer Menge atomarer Aktionen, zusammen mit Abhängigkeitsbeziehungen zwischen Aktionspaaren. Diese Festlegung der statischen Struktur eines nebenläufigen Systems führt zu einem erstmals in der Kombinatorik durch Cartier und Foata untersuchten mathematischen Objekt, dem freien, partiell-kommutativen Monoid [CF69]. Die Spezifikation eines gegebenen Systems besteht aus einer Menge von atomaren Aktionen Σ, zusammen mit einer irreflexiven, symmetrischen Unabhängigkeitsoder Kommutationsrelation I ⊆ Σ × Σ. Die kausale Unabhängigkeit wird in diesem Modell als wechselseitige Relation dargestellt, und es kann keine Aktion parallel zu sich selbst ausgeführt werden. Intuitiv betrachtet können unabhängige Aktionen gleichzeitig stattfinden, während abhängige Aktionen zeitlich geordnet werden müssen. Sind zwei Aktionen a, b unabhängig, (a, b) ∈ I, so werden zwei sequentielle Beobachtungen u ab v und u ba v (u, v ∈ Σ^{∗}) miteinander identifiziert. Betrachtet man die Äquivalenzrelation, die durch Gleichungen dieser Art induziert wird, so stellt sich heraus, daß sie eine Kongruenzrelation ist. Sie führt somit zu einer Monoidstruktur, zum Monoid der endlichen Spuren. Aus dieser formalsprachlichen Perspektive heraus sind Spuren Äquivalenzklassen von Wörtern, die mittels Kommutation ineinander überführt werden können. Diese Sicht entspricht der Darstellung von Nebenläufigkeit durch Interleaving.

Von einem weiteren Standpunkt aus entspricht ein paralleler Prozeß einer beschrifteten partiellen Ordnung, deren Knoten mit Aktionen aus Σ markiert sind und deren Kanten die kausalen Zusammenhänge zwischen Aktionen in Form einer Ordnungsbeziehung ausdrücken. Aus dieser Sicht werden Spuren als Abhängigkeitsgraphen angesehen, d.h. als azyklische, beschriftete Graphen mit Kanten zwischen Knoten mit abhängigen Markierungen. Die Theorie endlicher Spuren hat in den letzten Jahren eine ergebnisreiche Entwicklung durchlaufen, sowohl als Erweiterung der Theorie der formalen Sprachen, als auch im Zusammenhang mit anderen Modellen nebenläufiger Systeme, wie z.B. Petri-Netze (für einen Überblick sei auf die Monographie [Die90] verwiesen).

Der Übergang zu unendlichen Spuren erscheint als natürlicher Schritt, um Eigenschaften reaktiver Systeme wie Lebendigkeit oder Fairneß untersuchen zu können [Kwi89]. Verteilte Systeme, die unter dem Aspekt dieser beiden Eigenschaften betrachtet werden, werden gewöhnlich entweder axiomatisch beschrieben, zumeist im Rahmen einer temporalen Logik, oder aber konstruktiv, als Verhalten eines endlichen Transitionssystems [LL90]. Begrifflich wurden unendliche Spuren als Modell für nichtterminierende, nebenläufige Systeme in verschiedenen Zusammenhängen eingeführt: u.a. für Serialisierungsprobleme in verteilten Datenbanksystemen [FR85] und in der Theorie der Petri-Netze [BD87]. Eine erste formale Definition wird erneut Mazurkiewicz [Maz85] zugesprochen, der eine unendliche (reelle) Spur als gerichtete, präfixabgeschlossene Menge endlicher Spuren eingeführt hat. Im Sinne dieser Definition wird eine reelle Spur als Grenzwert ihrer endlichen Präfixe angesehen, d.h. das unendliche Verhalten wird durch endliche Anfangsteile approximiert. Definiert man unendliche Spuren als unendliche Abhängigkeitsgraphen, so entsprechen die reellen Spuren den Graphen, deren sämtliche Knoten eine endliche Vergangenheit haben. Es handelt sich also um Graphen, die zu einer (unendlichen) Sequenz serialisiert werden können (vgl. das folgende Beispiel, in dem die Spur (abc)^{ω} als Hasse-Diagramm dargestellt ist).

[figure: a; c; b; a; b; c; a; b; c; …]

Die bereits erwähnte konstruktive Darstellung mittels Transitionssystemen führt auf ein fundamentales Konzept, auf die endliche Kontrollierbarkeit (Erkennbarkeit). Erkennbare Mengen zeichnen sich außerdem durch eine Vielfalt von Charakterisierungen aus, die verschiedene Bereiche wie Logik oder Topologie miteinander verbinden. So wurde beispielsweise die Untersuchung erkennbarer Mengen unendlicher Sequenzen innerhalb der Logik initiiert, und zwar durch Büchi’s Ergebnis der Äquivalenz zwischen Erkennbarkeit und Definierbarkeit in monadischer Logik 2. Stufe [Büc60]. Eine ausführliche Behandlung erkennbarer Mengen unendlicher Sequenzen erscheint in [PP93, Tho90a].

Erkennbarkeit im Rahmen reeller Spursprachen wurde 1989 erstmals untersucht [Gas91, BMP90]. Die Definition von P. Gastin [Gas91] entspricht dem klassischen Ansatz der saturierenden Morphismen. Die Charakterisierungen dieser Sprachfamilie mittels der syntaktischen Kongruenz von A. Arnold [Arn85], bzw. mittels c-rationaler Ausdrücke [GPZ91] zeigten, daß die Definition erkennbarer reeller Spursprachen adäquat ist. Hingegen fehlte ein geeignetes Erkennungsmodell im Sinne von endlichen Automaten. Wünschenswert für eine automatentheoretische Charakterisierung ist das Modell der asynchronen Automaten, das von W. Zielonka für die Erkennung endlicher Spuren eingeführt wurde [Zie87]. Asynchrone Automaten sind endliche Automaten mit verteilter Kontrolle und Speicher, d.h. sie stellen Netze autonomer und kooperierender endlicher Automaten dar. Die verteilte endliche Kontrolle erlaubt es, Nebenläufigkeit als parallele Ausführung unabhängiger Aktionen auszudrücken. Damit sind sie ausdrucksstärker als gewöhnliche endliche Automaten, die Parallelität lediglich durch Interleaving darstellen. Darüberhinaus sind sie mächtig genug, um die Klasse der erkennbaren Sprachen endlicher Spuren zu charakterisieren, wie durch das wichtige Ergebnis von Zielonka gezeigt wird [Zie87, Zie89]. Der Automat der folgenden Abbildung gehört zu einer speziellen Art von asynchronen Automaten, nämlich zu den asynchron-zellulären Automaten. Deren Funktionsweise kann durch das Concurrent-Read-Owner-Write Konzept der P-RAM Maschine umschrieben werden. Der Automat erkennt die Spur (abc)^{ω}. Als erstes automatentheoretisches Resultat wurde von P. Gastin und A. Petit gezeigt, daß mit einer geeigneten lokalen Büchi Akzeptanzbedingung die Familie erkennbarer reeller Spursprachen durch nichtdeterministische Automaten charakterisiert werden kann. Dieses Ergebnis verallgemeinerte die Charakterisierung für unendliche Wörter auf reelle Spuren. Für eine Charakterisierung der Erkennbarkeit für Sprachen unendlicher Wörter mittels deterministischer Automaten ist ein mächtigeres Automatenmodell notwendig, z.B. der Muller Automat. Die Äquivalenz beider Automatenmodelle im Wortfall wurde sowohl mit algebraischen Methoden [Sch73], als auch mit direkten (allerdings aufwendigen) Automaten-Konstruktionen (beispielsweise die Konstruktion von S. Safra [Saf88]) gezeigt. Damit war die Frage nach der Äquivalenz nichtdeterministischer Büchi und deterministischer Muller Automaten im asynchron (-zellulären) Modell naheliegend und besonders interessant. Wir beantworten diese wichtige Frage, indem wir die Klasse erkennbarer reeller Spursprachen durch deterministische asynchronzelluläre Muller Automaten charakterisieren und verallgemeinern hierdurch das Theorem von McNaughton [McN66] über unendliche Wörter auf reelle Spuren.

Abschließend geben wir eine inhaltliche Übersicht der vorliegenden Arbeit. Wir beginnen in Kapitel 1 mit einer kurzen Einführung der Grundbegriffe der Spuren, gefolgt von einer Zusammenfassung der wichtigsten Eigenschaften asynchroner Automaten. Der Schwerpunkt liegt dabei auf dem Spezialfall des asynchron-zellulären Automaten, aus dessen einfacher Struktur elementare Eigen-

[figure: A; C; B; Asynchron-zellulärer Automat:; Prozessor a; Prozessor b; Prozessor c; do forever; (read) x := A; (read) y := C; if (x̄ ∧ ȳ) ∨ (x ∧ y); then A := x̄ (write); do forever; (read) x := B; (read) y := C; if (x̄ ∧ ȳ) ∨ (x ∧ y); then B := x̄ (write); do forever; (read) x := C; y := A; z := B; if (x ∧ ȳ ∧ z̄) ∨ (x̄ ∧ y ∧ z); then C := x̄ (write)]

Abbildung 0.1: Die Programme stellen atomare Aktionen dar. Die gemeinsamen Variablen A, B, C werden mit 1 initialisiert.

schaften hervorgehen. Die Konstruktion von Zielonka wird in ihren Grundzügen vorgestellt, wobei wir in Kapitel 5 auf die technischen Einzelheiten näher eingehen. Abschließend führen wir Erkennbarkeit im Kontext reeller Spursprachen ein. Kapitel 2 ist dem Beweis des Theorems von McNaughton [McN66] für reelle Spursprachen gewidmet. Dabei folgen wir einem algebraischen Ansatz, der Schützenberger’s Beweis entspricht, so wie er in [PP93] vereinfacht vorgestellt wird. Wir definieren deterministische reelle Spursprachen und zeigen, daß die Klasse der erkennbaren reellen Spursprachen mit dem Booleschen Abschluß der Klasse deterministischer Sprachen übereinstimmt. In einem zweiten (im Gegensatz zu unendlichen Wörtern) nichttrivialen Teil, werden deterministische asynchron-zelluläre Muller Automaten für die Erkennung deterministischer reeller Spursprachen angegeben. Die deterministischen reellen Spursprachen stellen auch das Thema von Kapitel 3 dar. Zunächst geben wir eine kurze Begründung der speziellen Definition aus der Sicht des Abschlusses unter Booleschen Operationen. Anschließend charakterisieren wir diese Sprachklasse mittels deterministischer I-Diamant Büchi Automaten mit verallgemeinerter Akzeptanzbedingung. I-Diamant Automaten sind Wortautomaten, die Unabhängigkeit in Form von Interleaving darstellen.

Wir zeigen, daß deterministische asynchron-zelluläre Büchi Automaten für eine Charakterisierung deterministischer Sprachen nicht ausreichen. In Kapitel 4 gehen wir auf eine Unterklasse erkennbarer reeller Spursprachen ein, und zwar auf die sternfreien Sprachen. Wir verallgemeinern eine bekannte Charakterisierung der Sternfreiheit indem wir zeigen, daß sie mit der Aperiodizität des syntaktischen Monoids übereinstimmt. Die Komplementierung nichtdeterministischer Büchi Automaten ist bereits im Fall der unendlichen Wörter ein wichtiges Problem mit interessanten Lösungen. In Kapitel 5 erweitern wir die Komplementierungskonstruktion von Klarlund [Kla91] auf asynchron-zelluläre Automaten. Voraussetzung war, daß wir eines der offenen Probleme im Bereich endlicher Spuren lösten, indem wir eine Potenzautomaten-Konstruktion für asynchron-zelluläre Automaten angaben. Diese wird anschließend für die Komplementierung verwendet, um die Konstruktion möglichst effizient durchzuführen. Kapitel 6 ist schließlich einigen algorithmischen Überlegungen bezüglich dem Abgeschlossenheitsproblem für I-Diamant Automaten gewidmet. Es werden Kriterien für die Abgeschlossenheit der Sprachen angegeben, die von Büchi bzw. Muller Automaten dieser Art akzeptiert werden. Wir zeigen, daß die Kriterien für gewisse Komplexitätsklassen vollständig sind. Zusammenfassend zeigt unsere Arbeit, daß alle wichtigen Ergebnisse der Theorie unendlicher Wörter eine natürliche Erweiterung für reelle Spursprachen haben.

8

Kapitel 1

Spursprachen und Erkennbarkeit

Wir leiten diesen Abschnitt mit einer kurzen Einführung der grundlegenden Begriffe ein, zusammen mit einigen Notationen. Ein Abhängigkeitsalphabet ist ein Paar (Σ, D), wobei Σ ein endliches Alphabet und D ⊆ Σ×Σ eine reflexive, symmetrische Beziehung bezeichnet, die Abhängigkeitsrelation. Die komplementäre Relation I = (Σ × Σ) \ D wird als Unabhängigkeitsrelation bezeichnet. Sei ≡_{I} ⊆ Σ^{∗} × Σ^{∗} die Äquivalenzrelation, die durch die Menge {(uabv, ubav) | (a, b) ∈ I, u, v ∈ Σ^{∗}} induziert wird. Die Relation ≡_{I} ist eine Kongruenz und das dazugehörige Quotientenmonoid IM(Σ, D) = Σ^{∗}/_{≡_{I}} wird als freies, partiell kommutatives Monoid bzw. Monoid endlicher Spuren bezeichnet. Eine endliche Spur ist damit eine Äquivalenzklasse von Wörtern. Aus einer weiteren Sicht heraus kann eine Spur mit einem Abhängigkeitsgraphen identifiziert werden, d.h. mit einem (bis auf Isomorphie) beschrifteten, azyklischen, gerichteten Graphen [V, E, λ], mit V, E bzw. λ : V → Σ als Knoten-, Kantenmenge bzw. Beschriftung der Knotenmenge so, daß für alle u, v ∈ V gilt:

(λ(u), λ(v)) ∈ D ⟺ (u, v) ∈ id_{V} ∪ E ∪ E^{−1}.

Zu einer Spur t = [a_{1} ⋯ a_{n}] ∈ IM(Σ, D) mit a_{i} ∈ Σ für 1 ≤ i ≤ n wird der dazugehörige Abhängigkeitsgraph G(t) gebildet, indem zunächst eine n-elementige Knotenmenge V = {v_{1}, …, v_{n}} so beschriftet wird, daß λ(v_{i}) = a_{i} gilt. Die Kantenmenge ist dabei durch E = {(v_{i}, v_{j}) | i < j und (λ(v_{i}), λ(v_{j})) ∈ D} festgelegt. Der Begriff des Abhängigkeitsgraphen kann natürlich auf unendliche Graphen erweitert werden. Im folgenden bezeichnet G(Σ, D) die Menge der endlichen und unendlichen Abhängigkeitsgraphen mit abzählbarer Knotenmenge V so, daß für alle a ∈ Σ gilt: λ^{−1}(a) ⊆ V ist eine wohlgeordnete Kette. Mit dieser Festlegung können Knoten als Paare (a, i) mit a ∈ Σ und i eine abzählbare Ordinalzahl dargestellt werden, wobei (a, i) den (i+1)-ten mit a beschrifteten Knoten bezeichnet. Auf G(Σ, D) sei die Konkatenation gegeben durch [V_{1}, E_{1}, λ_{1}][V_{2}, E_{2}, λ_{2}] = [V, E, λ], mit [V, E, λ] disjunkte Vereinigung der beiden Abhängigkeitsgraphen, zusammen mit zusätzlichen Kanten (v_{1}, v_{2}) ∈ V_{1} × V_{2} zwischen Knoten mit abhängiger Markierung, (λ_{1}(v_{1}), λ_{2}(v_{2})) ∈ D. Die Identität sei der leere Graph 1 = [∅, ∅, ∅]. Wir können nun das ω-Produkt analog definieren. Sei (g_{n})_{n≥0} ⊆ G(Σ, D) eine Sequenz von Abhängigkeitsgraphen. Dann ist das Produkt g = g_{0}g_{1} … ∈ G(Σ, D) als disjunkte Vereinigung der g_{n} erklärt, zusammen mit zusätzlichen Kanten von g_{n} nach g_{m} mit n < m, zwischen Knoten mit abhängiger Markierung. Wir bezeichnen für L ⊆ G(Σ, D) mit L^{ω} die ω-Iteration von L, d.h. die Menge L^{ω} = { g_{0}g_{1} … | g_{n} ∈ L, ∀n ≥ 0 }.

Weiterhin bezeichnen wir mit Σ^{ω} die Menge der unendlichen Wörter über Σ. Es sei Σ^{∞} = Σ^{∗} ∪ Σ^{ω} die Menge der endlichen und unendlichen Wörter.

Der kanonische Epimorphismus φ : Σ^{∗} → IM(Σ, D) kann auf Σ^{∞} erweitert werden, wobei es sich bei φ : Σ^{∞} → G(Σ, D) nicht mehr um einen Homomorphismus handelt. Die Bildmenge φ(Σ^{∞}) ⊆ G(Σ, D) ist die Menge reeller Spuren und wird mit IR(Σ, D) bezeichnet. Beachte, daß IR(Σ, D) kein Untermonoid von G(Σ, D) darstellt (es gilt beispielsweise a^{ω} ∈ IR(Σ, D) und b ∈ IR(Σ, D), aber für (a, b) ∈ D ist das Produkt a^{ω}b keine reelle Spur mehr). Außerdem ist φ weder mit der Konkatenation, noch mit der ω-Iteration vertauschbar: für L, K ∈ Σ^{∞} gilt φ(LK) = φ(L)φ(K) bzw. φ(L^{ω}) = (φ(L))^{ω} genau dann, wenn L ⊆ Σ^{∗}.

Abschließend seien einige häufig verwendete Bezeichnungen erklärt. Für a ∈ Σ sei D(a) = {b ∈ Σ | (a, b) ∈ D} bzw. I(a) = Σ \ D(a). Analog seien für A ⊆ Σ die Mengen D(A) = ∪_{a∈A}D(a) bzw. I(A) = Σ \ D(A) erklärt. Für eine Menge K sei P(K) die Potenzmenge von K, bzw. |K| die Kardinalität von K. Mit K^{co} bezeichnen wir das Komplement von K.

Für t ∈ IR(Σ, D) sei 0 ≤ |t|_{a} ≤ ω die Anzahl der Vorkommen von a in t. Dann bezeichnet alph(t) das Alphabet von t, d.h. die Menge {a ∈ Σ | |t|_{a} > 0}; mit alphinf(t) wird das unendlich oft auftretende Alphabet von t bezeichnet, d.h. die Menge {a ∈ Σ | |t|_{a} = ω}. Wir verwenden später die Bezeichnung alphinf(w) auch für (un)endliche Wörter w ∈ Σ^{∞}. Weiterhin sei für eine endliche Spur t ∈ IM(Σ, D) die Menge der Beschriftungen der maximalen Elemente mit max(t) bezeichnet.

Die Präfix-Ordnung ≤ auf IR(Σ, D) wird wie folgt erklärt: Es sei u ≤ t genau dann, wenn t = us für ein s ∈ IR(Σ, D) gilt. Für zwei Spuren t_{1}, t_{2} bezeichnen wir dann mit t_{1}⊓t_{2} das Infimum von t_{1}, t_{2}. Das Supremum einer Menge Y ⊆ IR(Σ, D), wird (falls es existiert) mit ⊔Y bezeichnet.

In den Beweisen werden wir durchgehend Durchschnitte t_{1} ∩ t_{2} im Sinne von Faktoren einer Spur verwenden. Sei beispielsweise t = u_{1}u_{2}u_{3} eine Zerlegung von u ∈ IR(Σ, D) in Faktoren u_{i}, mit u_{i} ∈ IR(Σ, D), i = 1, 2, 3. Dann können die Faktoren u_{i} mit Untergraphen von t identifiziert werden. Allgemeiner sei t = u_{1} ⋯ u_{m} = v_{1} ⋯ v_{n}, dann definieren die Graphendurchschnitte w_{ij} = u_{i} ∩ v_{j} mit 1 ≤ i ≤ m und 1 ≤ j ≤ n Faktoren von t. Es gilt u_{i} = w_{i1} ⋯ w_{in} bzw. v_{j} = w_{1j} ⋯ w_{mj}, für alle i, j. Man beachte, daß aus der Darstellung von t folgt: alph(w_{ij}) × alph(w_{kl}) ⊆ I, für alle i < k und j > l (bzw. i > k und j < l). Ein wichtiger Spezialfall hiervon ist mit m = n = 2 das Lemma von Levi.

1.1 Erkennbarkeit

Ziel dieses Abschnitts ist es, eine knappe Übersicht über Erkennbarkeit im Kontext allgemeiner Monoide anzugeben (für Einzelheiten siehe [Ber79]).

Definition 1.1.1 Sei M ein Monoid. Eine Teilmenge L ⊆ M heißt erkennbar, wenn ein endliches Monoid N und ein Monoid-Homomorphismus h : M → N derart existieren, daß L = h^{−1}h(L) gilt. Wir sagen in diesem Fall, daß L von h erkannt wird.

Bemerkung 1.1.2 Die obige Definition ist offensichtlich äquivalent zur Existenz einer Kongruenzrelation R auf M mit endlichem Index, die L saturiert, d.h. so, daß L als Vereinigung von Äquivalenzklassen von R darstellbar ist.

Die Klasse Rec(M) der erkennbaren Teilmengen von M bildet eine Boolesche Algebra und ist abgeschlossen unter inversen Homomorphismen. Eine äquivalente Definition der Erkennbarkeit basiert auf den Begriff des M-Automaten, der Gegenstand der folgenden Definition ist:

Definition 1.1.3 Sei (M, ·, 1) ein Monoid. Ein M-Automat A ist ein 4-Tupel (Q, δ, q_{0}, F), wobei:

• Q ist die Zustandsmenge,

• δ : Q × M → Q ist die Übergangsfunktion so, daß mit δ(q, m) =: qm für alle q ∈ Q, m, n ∈ M gilt:

q1 = q  und  q(mn) = (qm)n,

• q_{0} ∈ Q ist der Anfangszustand, und

• F ⊆ Q ist die Menge der Endzustände.

Der M-Automat A heißt endlich, wenn die Zustandsmenge Q endlich ist. Er akzeptiert die Menge L(A) = {m ∈ M | q_{0}m ∈ F }.

Die nachfolgenden Beziehungen zwischen Akzeptanz durch (endliche) Automaten und Erkennbarkeit durch Homomorphismen auf (endlichen) Monoide sind leicht zu verifizieren. Eine Menge L ⊆ M, die von einem vollständigen M-Automaten A = (Q, δ, q_{0}, F) akzeptiert wird, wird vom folgenden Homomorphismus erkannt (wobei Q^{Q} das Transformationsmonoid von Q bezeichnet):

h : M → Q^{Q}
m ⟼ (q ↦ qm, ∀q ∈ Q)
Es gilt:  L = h^{−1}(Φ), mit Φ = {f ∈ Q^{Q} | f(q_{0}) ∈ F }

Umgekehrt können wir zu einem Monoid (N, ·, 1) und einem Homomorphismus h : M → N, der L ⊆ M erkennt, einen M-Automaten A = (N, δ, 1, h(L)) angeben, der L akzeptiert. Die Übergangsfunktion δ : N × M → N wird dabei erklärt durch δ(n, m) := nh(m). Der Automat A ist endlich, falls N ein endliches Monoid ist. Um auf den Begriff der saturierenden Kongruenzen zurückzukommen (vgl. Bemerkung 1.1.2), führen wir schließlich die syntaktische Kongruenz ≡_{L} einer Sprache L ⊆ M ein. Dies ist die gröbste Kongruenz, die L saturiert, und wird für m, m′ ∈ M wie folgt definiert:

m ≡_{L} m′ ⟺ (nmp ∈ L ⇔ nm′p ∈ L, ∀n, p ∈ M)

Das zu dieser Kongruenz gehörende Quotientenmonoid M/_{≡_{L}} =: Synt(L) wird als syntaktisches Monoid von L bezeichnet und der kanonische Homomorphismus h : M → Synt(L) als syntaktischer Morphismus. Der nächste Satz faßt die angegebenen Charakterisierungen erkennbarer Mengen zusammen:

Satz 1.1.4 Sei M ein Monoid. Folgende Aussagen sind zueinander äquivalent:

1. L ⊆ M ist erkennbar.

2. Es existiert ein endlicher Automat A, der L akzeptiert.

3. Das syntaktische Monoid von L, Synt(L), ist endlich.

Wir schließen diesen Abschnitt mit einigen Bemerkungen zum Begriff des minimalen Automaten. Zu einer gegebenen Menge L ⊆ M definieren wir eine Relation R_{L} ⊆ M × M durch:

m R_{L} m′  ⟺  (mn ∈ L ⇔ m′n ∈ L, ∀n ∈ M)

Es ist leicht zu sehen, daß R_{L} eine rechtsinvariante Äquivalenzrelation ist, daher ist die Übergangsfunktion des nachfolgenden Automaten A_{L} wohldefiniert. Dabei bezeichnet [m] die Äquivalenzklasse eines Elements m ∈ M:

A_{L} = ( Q = M/_{R_{L}}, δ, q_{0} = [1], F = {[m] | m ∈ L})
mit δ([m], m′) = [mm′]

Es gilt L(A) = L und, falls L ∈ Rec(M) erkennbar ist, so ist der Automat A_{L} endlich und stellt den minimalen Automaten von L dar.

Bemerkung 1.1.5 Im Spezialfall des freien, partiell kommutativen Monoids M = IM(Σ, D) besitzt der minimale Automat A_{L} = (Q, ·, q_{0}, F) einer erkennbaren Sprache L ∈ Rec(IM) die sogenannte I-Diamant Eigenschaft:

∀ q ∈ Q, ∀ (a, b) ∈ I : q · ab = q · ba

Der klassische Begriff des M-Automaten führt daher auf natürlichem Wege zur I-Diamant Eigenschaft, die die Unabhängigkeit von Aktionspaaren mittels Interleaving ausdrückt. Dabei werden alle Ausführungsfolgen einer Sequenz von Aktionen als äquivalente Berechnungspfade im Automaten ermöglicht (äquivalent im Sinne der Akzeptanz). Der Nachteil des I-Diamant Automaten besteht allerdings in der zentralisierten Kontrollstruktur, die Nebenläufigkeit nicht direkt ausdrücken kann. Ihr wesentlicher Vorteil besteht hingegen in ihrer geringen Größe, verglichen mit dem verteilten Automatenmodell, das wir jetzt vorstellen.

1.2 Asynchrone Automaten

Das Konzept der asynchronen Automaten ist von W. Zielonka als verteiltes Automatenmodell für endliche Spuren eingeführt worden [Zie87, Zie89, CMZ90]. Vom Prinzip her ist ein asynchroner Automat ein Netz von endlichen Automaten, die als autonome, kooperierende Prozesse arbeiten. Ihre verteilte endliche Kontrolle ermöglicht eine nebenläufige Ausführung unabhängiger Aktionen. Im Zusammenhang mit anderen parallelen Berechnungsmodellen sei angemerkt, daß asynchrone Automaten äquivalent sind zu 1–sicheren, beschrifteten Petri-Netzen. Die Bedeutung der asynchronen Automaten liegt im herausragenden Ergebnis von Zielonka über die Äquivalenz von Erkennbarkeit in IM(Σ, D) und Akzeptanz durch deterministische Automaten dieser Art. Gegenstand unserer Betrachtung hier werden die asynchronen und die asynchron-zellulären Automaten sein. Später werden wir uns hauptsächlich auf die asynchron-zellulären Automaten konzentrieren, deren interne Struktur sich als elementarer erweist und ”bessere“ Eigenschaften besitzt. Ein weiterer wichtiger Aspekt ist die Tatsache, daß Zielonka’s Konstruktion genau diesen Automatentyp liefert. Darüber hinaus liegen einfache Umwandlungen von einem Modell ins andere vor. Sei (Σ, D) ein Abhängigkeitsalphabet und IM(Σ, D) das zugehörige freie, partiell kommutative Monoid. Ein asynchroner Automat über (Σ, D) ist ein 4-Tupel A = (Q, δ, q_{0}, F) mit:

• Q = ∏_{i=1}^{m} Q_{i} ist die Zustandsmenge, wobei Q_{i} für 1 ≤ i ≤ m lokale Zustandsmengen darstellen,

• Zu jedem a ∈ Σ ist eine Indexmenge (Domäne) Dom(a) ⊆ {1, …, m} assoziiert so, daß Dom(a) ∩ Dom(b) = ∅ genau dann gilt, wenn (a, b) ∈ I.

• δ ⊆ Q × Σ × Q ist die (partiell definierte) globale Übergangsrelation, die aus den lokalen Übergangsrelationen δ_{a}, a ∈ Σ, besteht mit:

δ_{a} ⊆ ∏_{i∈Dom(a)} Q_{i} × ∏_{i∈Dom(a)} Q_{i},

• q_{0} ∈ Q (bzw. F ⊆ Q) ist der Anfangszustand (bzw. die Menge der Endzustände).

Ein globaler a-Übergang (q′_{i})_{1≤i≤m} ∈ δ((q_{i})_{1≤i≤m}, a) ist definiert, wenn der lokale Übergang (q′_{i})_{i∈Dom(a)} ∈ δ_{a}((q_{i})_{i∈Dom(a)}) definiert ist, und bewirkt eine Änderung lediglich auf den lokalen Zuständen, die zur Domäne von a gehören, d.h.:

(q′_{i})_{1≤i≤m} ∈ δ((q_{i})_{1≤i≤m}, a) ⟺
\{ \begin{matrix}(q′_{i})_{i∈Dom(a)} ∈ δ_{a}((q_{i})_{i∈Dom(a)}, a) und \\ q_{j}′ = q_{j}, falls j ∉ Dom(a) . \end{matrix}

Der Automat ist endlich, wenn seine Zustandsmenge Q endlich ist; er ist deterministisch, wenn alle δ_{a} (partiell definierte) Funktionen sind. Er akzeptiert mit u ∈ Σ^{∗} alle Wörter, die zu u äquivalent sind bzgl. (Σ, D). Daher kann die Spursprache, die von A erkannt wird, durch L(A) = {t ∈ IM(Σ, D) | δ(q_{0}, u) ∈ F für ein u ∈ φ^{−1}(t)} definiert werden.

Ein asynchron-zellulärer Automat über dem Abhängigheitsalphabet (Σ, D) ist ein 4-Tupel A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F), wobei für alle a ∈ Σ gilt:

• Q_{a} stellt eine endliche Menge von lokalen Zuständen dar,

• q_{0} ∈ ∏_{a∈Σ} Q_{a} ist der globale Anfangszustand,

• F ⊆ ∏_{a∈Σ} Q_{a} ist eine Menge globaler Endzustände und

• δ_{a} ⊆ (∏_{b∈D(a)} Q_{b}) × Q_{a} stellt die lokale (partiell definierte) Übergangsrelation dar.

Der Automat heißt deterministisch, wenn δ_{a} eine (partiell definierte) Funktion ist, für alle a ∈ Σ. Im folgenden verwenden wir die Abkürzungen Q_{A} für ∏_{b∈A} Q_{b} und q_{A} für ∏_{b∈A} q_{b}, wobei A ⊆ Σ. Insbesondere wird q_{D(a)} die Bedeutung ∏_{b∈D(a)} q_{b} haben, d.h. q_{D(a)} ist die Projektion eines globalen Zustands q ∈ Q_{Σ} auf die lokalen Komponenten b ∈ D(a). Die globale Übergangsrelation δ ⊆ Q_{Σ} × Σ × Q_{Σ} des asynchron-zellulären Automaten A ist definiert durch:

q′ ∈ δ(q, a) ⇔ q′_{a} ∈ δ_{a}(q_{D(a)})  und
q′_{c} = q_{c} für alle c ≠ a

Damit kann die von A akzeptierte Spursprache L(A) analog definiert werden durch L(A) = {t ∈ IM(Σ, D) | δ(q_{0}, u) ∈ F für ein u ∈ φ^{−1}(t)}. Mit anderen Worten ist die Existenz eines globalen Folgezustands q′ ∈ Q_{Σ} von q nur durch diejenigen lokalen Komponenten des Zustands q bedingt, die in Abhängigkeit von a stehen. Weiterhin bewirkt der a-Übergang lediglich eine Änderung der a-Komponente des globalen Zustandes, wobei der neue Wert durch die b-Komponenten von q mit b ∈ D(a) festgelegt wird. Durch seine verteilte endliche Kontrolle besitzt ein asynchron-zellulärer Automat die Fähigkeit, unabhängige Aktionen (Übergänge) parallel ablaufen zu lassen. Weiterhin ergibt die Betrachtung der Übergänge im Automaten als Lese-Schreibe-Operationenpaar eine Analogie zum Concurrent-Read-Owner-Write–Prinzip für P-RAM Maschinen: Simultanes Lesen ist erlaubt, während Schreiboperationen nur im eigenen Bereich zugelassen sind. Wir verwenden vorwiegend asynchron-zelluläre Automaten aufgrund einiger markanter Eigenschaften, die von Automaten der Zielonka-Konstruktion erfüllt werden. Wegen dem häufigen Gebrauch dieser Eigenschaften sollen an dieser Stelle die Grundzüge der Konstruktion von Zielonka zusammengefaßt werden (die Beweise können z.B. [Die90, CMZ90] entnommen werden). Für a ∈ Σ und Teilalphabete A ⊆ Σ seien die ∂_{a}- bzw. ∂_{A}-Präfixe einer endlichen Spur als kleinste Präfixe definiert, die alle Auftreten des Buchstabens a bzw. aller Buchstaben aus A enthalten. Formal bedeutet dies:

∂_{a}(t) = ⊓{ u ≤ t | |t|_{a} = |u|_{a} } und  ∂_{A}(t) = ⨆_{a∈A} ∂_{a}(t)
(insbesondere gilt ∂_{∅}(t) = 1 und ∂_{Σ}(t) = t).

Es gilt beispielsweise ∂_{a}(ta) = ∂_{D(a)}(t)a für alle t ∈ IM(Σ, D), a ∈ Σ. Die Konstruktion von Zielonka beruht auf der Berechnung einer ”verteilten“ Abbildung, der asynchronen Abbildung (asynchronous mapping, siehe e.g. [Die90]). Es handelt sich um eine Abbildung μ : IM(Σ, D) → Q zu einer Menge Q, die für alle t ∈ IM(Σ, D), a ∈ Σ und A, B ⊆ Σ folgende zwei Eigenschaften erfüllt:

• Der Wert μ(∂_{A∪B}(t)) ist durch die Werte μ(∂_{A}(t)) und μ(∂_{B}(t)) eindeutig festgelegt.

• Der Wert μ(∂_{a}(ta)) (= μ(∂_{D(a)}(ta))) ist durch den Buchstaben a und den Wert μ(∂_{D(a)}(t)) eindeutig festgelegt.

Zwischen asynchronen Abbildungen und asynchron-zellulären Automaten besteht ein grundlegender Zusammenhang, ähnlich dem zwischen Monoid-Homomorphis-men und endlichen Automaten, wie dies im folgenden gezeigt wird.

Bemerkung 1.2.1 Es seien eine asynchrone Abbildung μ : IM(Σ, D) → Q und eine Menge R ⊆ Q gegeben. Dann wird die Sprache μ^{−1}(R) vom folgenden asynchron-zellulären Automaten A_{μ} = (Q^{Σ}, δ, q_{0}, F) erkannt:

\begin{matrix}δ : Q^{Σ} × IM(Σ, D) → Q^{Σ}, \\ δ((μ(∂_{b}(t)))_{b∈Σ}, a) = (μ(∂_{b}(ta)))_{b∈Σ} \end{matrix}

Man beachte, daß ein a-Übergang nur die a-Komponente des globalen Zustands (μ(∂_{b}(t)))_{b∈Σ} ändert, wobei für b ≠ a gilt: ∂_{b}(ta) = ∂_{b}(t). Desweiteren hängt der neue lokale Zustand μ(∂_{a}(ta)) nur von a und dem Wert μ_{D(a)}(t) ab, da letzteres eindeutig durch die Werte (lokalen Zustände) μ(∂_{b}(t)) mit b ∈ D(a) festgelegt wird. Damit ist gezeigt, daß δ wohldefiniert ist und der Übergangsfunktion eines asynchron-zellulären Automaten entspricht. Der Anfangszustand sei q_{0} = (μ(1))_{a∈Σ} und die Menge der Endzustände sei gegeben durch F = { (μ(∂_{a}(t)))_{a∈Σ} | μ(t) ∈ R }. Man beachte außerdem, daß für alle t ∈ IM(Σ, D) gilt: δ(q_{0}, t) = (μ(∂_{a}(t)))_{a∈Σ}. Nehmen wir nun an, daß eine erkennbare Spursprache K ⊆ IM(Σ, D) gegeben ist, die vom Homomorphismus η : IM(Σ, D) → S zum endlichen Monoid S erkannt wird. Die Konstruktion von Zielonka besteht darin, eine endliche Menge Q und eine asynchrone Abbildung μ : IM(Σ, D) → Q so zu bestimmen, daß der Homomorphismus η durch μ faktorisiert wird, d.h. es existiert eine Abbildung π : Q → S derart, daß η = π ∘ μ (siehe Abbildung 1.1). Mit R = π^{−1}(η(K)) akzeptiert der oben beschriebene asynchron-zelluläre Automat A_{μ} genau die Sprache K.

[figure: K ⊆ IM(Σ, D); S; Q ⊇ π^{−1}(η(K)); μ; π; η; η = π ∘ μ]

Abbildung 1.1: η = π ∘ μ

Eine grundlegende Eigenschaft des Automaten, der aus einer asynchronen Abbildung entsteht, betrifft die lokalen Zustände der maximalen Elemente einer (endlichen) Spur t, max(t): Gilt für zwei endliche Spuren max(t_{1}) = max(t_{2}) = M und δ(q_{0}, t_{1})_{c} = δ(q_{0}, t_{2})_{c} für alle c ∈ M, so folgt damit t_{1} ∈ L(A) genau dann, wenn t_{2} ∈ L(A). Dies bedeutet, daß die lokalen Zustände der maximalen Elemente einer Spur die Akzeptanz durch den Automaten festlegen. Diese Eigenschaft folgt aus der Beziehung t = ∂_{max(t)}(t), womit der Wert μ(t) durch die Menge {μ(∂_{a}(t)) | a ∈ max(t)} festgelegt ist (μ ist eine asynchrone Abbildung). Diese Eigenschaft wird im Kapitel 2 bei der Konstruktion deterministischer asynchronzellulärer Muller Automaten eine wichtige Rolle spielen.

1.3 Erkennbare Sprachen reeller Spuren

Im Rahmen allgemeiner Monoide, wie z.B. des freien Monoids Σ^{∗} oder des Monoids der endlichen Spuren IM(Σ, D), haben wir Erkennbarkeit mit Hilfe von erkennenden Homomorphismen definiert. Ein ähnlicher Ansatz kann auch für reelle Spursprachen als Ausgangspunkt gewählt werden.

Sei η : IM(Σ, D) → S ein Homomorphismus und S ein Monoid. Wir sagen, daß eine reelle Spursprache L ⊆ IR(Σ, D) von η erkannt wird, wenn für beliebige Folgen von endlichen Spuren (t_{n})_{n≥0}, (t′_{n})_{n≥0} ⊆ IM(Σ, D), mit η(t_{n}) = η(t′_{n}) für alle n ≥ 0, gilt:

t_{0}t_{1} … ∈ L ⟺ t′_{0}t′_{1} … ∈ L .

Definition 1.3.1 [Gas91] Sei L ⊆ IR(Σ, D). L heißt erkennbar, wenn ein endliches Monoid S und ein Homomorphismus η : IM(Σ, D) → S derart existieren, daß L von η erkannt wird.

Bemerkung 1.3.2 Es läßt sich leicht zeigen, daß eine Sprache L, die vom Homomorphismus η erkannt wird, als L = ⋃_{(s,e)∈P_{L}} η^{−1}(s)η^{−1}(e)^{ω} sich darstellen läßt, wobei P_{L} = {(s, e) ∈ S^{2} | se = s, e^{2} = e und η^{−1}(s)η^{−1}(e)^{ω} ∩ L ≠ ∅}. Die Grundlage für diese Darstellung ist die Tatsache, daß L genau dann von η erkannt wird, wenn für jedes Paar (s, e) ∈ S mit se = s, e^{2} = e folgende Saturierungsbedingung gilt:

η^{−1}(s)η^{−1}(e)^{ω} ∩ L ≠ ∅ ⟹ η^{−1}(s)η^{−1}(e)^{ω} ⊆ L

Hierzu sei bemerkt, daß wir uns auf Paare (s, e) wie oben einschränken können, da wir zu einem gegebenen Homomorphismus jede reelle Spur t = φ(x_{0}x_{1} …) mit x_{i} ∈ Σ als t = t_{0}t_{1} … mit t_{i} ∈ IM(Σ, D) faktorisieren können, wobei η(t_{0}) = s und η(t_{n}) = e, n ≥ 1 für gewisse s, e ∈ S mit se = s und e^{2} = e gilt. Eine derartige Faktorisierung kann bekanntermaßen durch folgendes Ramsey-Argument erreicht werden: Wir definieren induktiv eine Sequenz (i_{n}, A_{n})_{n≥0} mit i_{n} ∈ IN, A_{n} ⊆ IN und |A_{n}| = ω und beginnen mit A_{0} = IN. Sei A_{n} bereits definiert und sei i_{n} = min A_{n}. Es existiert ein e ∈ S derart, daß die Menge A = {m ∈ A_{n} | η(x_{i_{n}}x_{i_{n}+1} … x_{m−1}) = e} unendlich ist, da S endlich ist. Wir setzen A_{n+1} = A. Damit erreichen wir, daß η(x_{i_{n}}x_{i_{n}+1} … x_{i_{n+p}−1}) unabhängig ist von p > 0. Sei e_{n} = η(x_{i_{n}}x_{i_{n}+1} … x_{i_{n+p}−1}). Ohne Einschränkung sei e_{n} = e für alle n ≥ 0 erfüllt (ansonsten wähle eine entsprechende Teilfolge von Indizes). Mit der Faktorisierung

t_{0} = φ(x_{0}x_{1} … x_{i_{1}−1})
t_{n} = φ(x_{i_{n}}x_{i_{n}+1} … x_{i_{n+1}−1}),  n ≥ 1

und mit s = η(t_{0}) (= s′e für ein s′ ∈ S) erreicht man das gewünschte Ergebnis, da e^{2} = e und se = s′ee = s′e = s gelten.

Eine alternative Definition von Rec(IR), der erkennbaren reellen Spursprachen, stützt sich auf den Begriff der syntaktischen Kongruenz, wie sie von A. Arnold [Arn85] für Sprachen unendlicher Wörter eingeführt wurde. Sei L ⊆ IR(Σ, D) gegeben. Zwei endliche Spuren t, t′ ∈ IM(Σ, D) heißen syntaktisch äquivalent, wenn für alle u, v, w ∈ IM(Σ, D) gilt:

u(tv)^{ω} ∈ L ⟺ u(t′v)^{ω} ∈ L
utvw^{ω} ∈ L ⟺ ut′vw^{ω} ∈ L

Wir bezeichnen die syntaktische Kongruenz einer Sprache L mit ≡_{L} und betrachten den zugehörigen kanonischen Epimorphismus η : IM(Σ, D) → IM(Σ, D)/_{≡_{L}}. In Analogie zum Fall der endlichen Spuren bzw. Wörter, kann gezeigt werden, daß die syntaktische Kongruenz gröber ist als jede Kongruenz, die L saturiert. Im allgemeinen jedoch ist sie selbst keine saturierende Kongruenz, wohl aber falls L erkennbar ist. Der folgende Satz faßt drei algebraische Charakterisierungen von Erkennbarkeit im Kontext reeller Spuren zusammen:

Satz 1.3.3 [Gas91] Eine reelle Spursprache L ⊆ IR(Σ, D) ist genau dann erkennbar, wenn eine der folgenden äquivalenten Bedingungen erfüllt ist:

1. φ^{−1}(L) ⊆ Σ^{∞} ist eine erkennbare Wortsprache.

2. L wird von einem Homomorphismus η : IM(Σ, D) → S erkannt, wobei S ein endliches Monoid ist.

3. Das syntaktische Monoid von L, Synt(L) = IM(Σ, D)/_{≡_{L}}, ist endlich und der syntaktische Homomorphismus η : IM(Σ, D) → Synt(L) erkennt L.

Bemerkung 1.3.4 Rec(IR) ist eine Boolesche Algebra. Dies folgt aus der ersten der obigen Charakterisierungen zusammen mit der Tatsache, daß die Familie der erkennbaren Mengen aus Σ^{∞} eine Boolesche Algebra bildet (φ^{−1} kommutiert mit den Booleschen Operationen).

Die Erkennung von Sprachen aus IR(Σ, D) durch asynchron-zelluläre Automaten erfordert geeignete zusätzliche Akzeptanzbedingungen für unendliche Spuren. Angelehnt an zwei klassische Akzeptanzbedingungen (Büchi bzw. Muller) wurden analoge verteilte Bedingungen vorgeschlagen [GP92], die wir im folgenden beschreiben. Sei einen π = (q_{0}, a_{0}, q_{1}, a_{1}, …) ein unendlicher (globaler) Übergangspfad im asynchron-zellulären Automaten A, mit q_{n} ∈ Q_{Σ} und a_{n} ∈ Σ für alle n ≥ 0 so, daß q_{n+1} ∈ δ(q_{n}, a_{n}). Wie bereits erwähnt, werden wir lokale Akzeptanzbedingungen angeben und betrachten daher diejenigen lokalen Zustände, die auf dem Pfad π unendlich oft vorkommen. Sei also inf_{a}(π) = {q_{a} ∈ Q_{a} | ∃^{∞}n : (q_{n})_{a} = q_{a}} die Menge der unendlich oft vorkommenden a-Zustände, a ∈ Σ. Ein asynchron-zellulärer Automat A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F) wird nun um eine Tafel T ⊆ ∏_{a∈Σ} P(Q_{a}) erweitert, die erlaubt, unendliche Pfade π gemäß den Zustandsmengen (inf_{a}(π))_{a∈Σ} zu akzeptieren.

Sieht man den um die Tafel T erweiterten Automaten A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, T ) als Büchi Automat an, so wird ein unendlicher Übergangspfad π von A akzeptiert, wenn ein Tafelelement T ∈ T derart existiert, daß T_{a} ⊆ inf_{a}(π) für alle a ∈ Σ gilt. Ist A hingegen ein Muller Automat, so wird der unendliche Pfad π akzeptiert, wenn ein T ∈ T existiert so, daß T_{a} = inf_{a}(π) für alle a ∈ Σ gilt. Anders ausgedrückt erfordert die Büchi Bedingung das unendliche Vorkommen gewisser lokaler Zustände, während eine Muller Bedingung erfordert, daß die unendlich oft wiederholten lokalen Zustände genau einem Tafelelement entsprechen.

Definition 1.3.5 Sei A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, T ) ein asynchron-zellulärer Automat. Die von A akzeptierte Sprache L(A) ⊆ IR(Σ, D) wird definiert wie folgt.

• Falls A ein Büchi Automat ist:

L(A) = {t ∈ IR(Σ, D) | ∃ Pfad π = (q_{0}, a_{0}, q_{1}, a_{1}, …) mit

t = φ(a_{0}a_{1} …) und ∃ T ∈ T mit T_{a} ⊆ inf_{a}(π), ∀ a ∈ Σ}
∪ {t ∈ IM(Σ, D) | δ(q_{0}, t) ∩ F ≠ ∅} .

• Falls A ein Muller Automat ist:

L(A) = {t ∈ IR(Σ, D) | ∃ Pfad π = (q_{0}, a_{0}, q_{1}, a_{1}, …) mit

t = φ(a_{0}a_{1} …) und ∃ T ∈ T mit T_{a} = inf_{a}(π), ∀ a ∈ Σ}
∪ {t ∈ IM(Σ, D) | δ(q_{0}, t) ∩ F ≠ ∅} .

Bemerkung 1.3.6 In der obigen Definition wird die akzeptierte Spursprache mittels Wortrepräsentanten erklärt. Man kann jedoch leicht zeigen, daß für t = φ(a_{0}a_{1} …) = φ(a′_{0}a′_{1} …), a′_{i} ∈ Σ, ein zu π äquivalenter Pfad π′ = (q_{0}, a′_{0}, q′_{1}, a′_{1}, …) existiert, der durch dasselbe Tafelelement T ∈ T akzeptiert wird. Dafür kann folgende Charakterisierung äquivalenter ω-Wörter benutzt werden ([DGP91]):

φ(a_{0}a_{1} …) = φ(a′_{0}a′_{1} …) ⟹

∃(x_{n})_{n≥0}, (y_{n})_{n≥0} ⊆ Σ^{∗}, ∃(k_{n})_{n≥0}, (l_{n})_{n≥0} ⊆ IN (k_{0} = l_{0} = 0) mit:

φ(a_{k_{n}} … a_{k_{n+1}−1}) = φ(x_{n}y_{n}) und
φ(a′_{l_{n}} … a′_{l_{n+1}−1}) = φ(y_{n−1}x_{n}) (mit y_{−1} := 1).

Wir wollen anhand eines einfachen Beispiels die beiden Akzeptanzbedingungen für reelle Spuren betrachten:

Beispiel 1.3.7 Es seien (Σ, D) mit b, c ∈ Σ, b ≠ c und D beliebig, und der asynchron-zelluläre Automat A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, T ) über (Σ, D) gegeben, mit

1. Q_{a} = {(q_{0})_{a}} und δ_{a}(q_{D(a)}) = (q_{0})_{a} für alle q und a ≠ b, c.

2. Für x ∈ {b, c} sei Q_{x} = {(q_{0})_{x}, r_{x}} und

δ_{x}(q_{D(x)}) = \{ \begin{matrix}r_{x} & falls q_{x} = (q_{0})_{x} \\ (q_{0})_{x} & falls q_{x} = r_{x} \end{matrix}

3. F = ∅.

4. T = {T } mit T = (∏_{a∈Σ\{b,c}} Q_{a}) × Q_{b} × {(q_{0})_{c}}.

Es ist leicht zu sehen, daß der obige Automat mit dem Muller Akzeptanzmodus die Sprache L(A) = {t ∈ IR(Σ, D) | b ∈ alphinf(t), |t|_{c} endlich, gerade} erkennt. Als Büchi Automat hingegen, erkennt er die Sprache L(A) = {t ∈ IR(Σ, D) | b ∈ alphinf(t), und (|t|_{c} = ω oder |t|_{c} gerade)}. An dieser Stelle sei auch angemerkt, daß Sprachen der Art Inf(A) := {t ∈ IR(Σ, D) | alphinf(t) = A} bzw. IR_{A} := {t ∈ IR(Σ, D) | D(alphinf(t)) = D(A)} erkennbar sind. Es genügt dafür, den obigen Automaten angemessen zu erweitern.

Die erste automaten-theoretische Charakterisierung erkennbarer reeller Spursprachen durch asynchrone Automaten geht auf die Arbeiten von P. Gastin und A. Petit zurück [GP92]:

Theorem 1.3.8 Rec(IR) ist äquivalent zur Familie der reellen Spursprachen, die durch nichtdeterministische, asynchron (-zelluläre) Büchi Automaten erkannt werden.

Die Konstruktion von P. Gastin und A. Petit ist modularer Natur und hat als Ausgangspunkt die Darstellung einer erkennbaren reellen Spursprache mittels rationaler Operatoren (siehe Bemerkung 1.3.2). Ihre Konstruktion ist daher aufgrund der Konkatenation (und ω-Iteration) innerhalb der rationalen Darstellung inhärent nichtdeterministisch. Wir werden im Kapitel 2 unter Verwendung eines algebraischen Ansatzes ([PP93]) eine Konstruktion deterministischer asynchronzellulärer Muller Automaten für Rec(IR) angeben, womit eine der wichtigen Fragen der Theorie der reellen Spuren (siehe auch [GP92]) beantwortet wird. Zum Abschluß dieser Einführung in Erkennbarkeit im Kontext reeller Spuren sei auf zwei weitere Charakterisierungen von Rec(IR) verwiesen. Zunächst sei c−Rat(IR) die Familie der c-rationalen Sprachen aus IR(Σ, D), d.h. die kleinste Teilmenge von P(IR(Σ, D)), die ∅ und {a}, a ∈ Σ, enthält und die unter Vereinigung ∪, Konkatenation ·, ∗- und ω-Iteration abgeschlossen ist, wobei die Iteration auf zusammenhängende Sprachen eingeschränkt ist (eine Spursprache L ist zusammenhängend, wenn jedes t ∈ L als Abhängigkeitsgraph gesehen zusammenhängend ist). Dann gilt:

Theorem 1.3.9 [GPZ91] Rec(IR) ist äquivalent zu c−Rat(IR).

Weiterhin betrachten wir die monadische Logik 2. Stufe, deren Formeln ausgehend von den Prädikaten x ≤ y, x ∈ X und P_{a}(x) gebildet werden, unter Verwendung der Booleschen Junktoren ∧, ∨, ¬ und der Quantoren ∃, ∀ (dabei bezeichnen x, y Individuenvariablen, X Mengenvariable; das Prädikat P_{a}(x) bedeutet, daß x mit a ∈ Σ beschriftet ist). Damit gilt:

Theorem 1.3.10 [EM93] Rec(IR) ist äquivalent zur Familie der reellen Spursprachen, die durch Formeln der monadischen Logik zweiter Stufe definierbar sind.

22

Das Theorem von McNaughton für IR(Σ, D)

Thema des vorliegenden Kapitels ist eine Verallgemeinerung des bekannten Theorems von McNaughton [McN66] von ω-Wortsprachen auf Sprachen reeller Spuren. Wir beantworten mit der Charakterisierung der Familie der erkennbaren Sprachen reeller Spuren durch deterministische asynchron-zelluläre Muller Automaten eine der wesentlichen Fragen auf diesem Gebiet. Die Ergebnisse dieses Kapitels sind auch in [DM93] erschienen. In den ersten beiden Abschnitten folgen wir Schützenberger’s Beweis für das Theorem von McNaughton, so wie er in [PP93] vorgestellt wird. Übertragen auf Spuren wird der Beweis wesentlich technischer und aufwendiger (vgl. 2.1.11), wobei die Grundideen beibehalten werden. Als erstes Ergebnis erhalten wir die Äquivalenz zwischen der Familie der erkennbaren reellen Spursprachen und dem Booleschen Abschluß der Familie der deterministischen reellen Spursprachen DRec(IR). Letztere Sprachfamilie ergibt sich als natürliche Verallgemeinerung der deterministischen ω-Wortsprachen, wobei jedoch kein direkter Zusammenhang zu deterministischen (asynchron-zellulären) Büchi Automaten mehr besteht, wie im Falle der ω-Wortsprachen. Wir diskutieren diesen Aspekt und begründen die Definition der Familie DRec(IR) in Kapitel 3. Schließlich zeigen wir im letzten Abschnitt die Äquivalenz von Erkennbarkeit in IR(Σ, D) und Akzeptanz durch deterministische asynchron-zelluläre Muller Automaten. Dies ist erneut ein nichttrivialer Schritt, der u.a. auf grundlegenden Eigenschaften asynchron-zellulärer Automaten basiert.

2.1 Algebraische Eigenschaften in Rec(IR)

Sei η : IM(Σ, D) → S ein Homomorphismus und S ein Monoid. Wir werden im folgenden die Bezeichnung IM_{s} := η^{−1}(s) für s ∈ S durchgehend verwenden, ohne den darunterliegenden Homomorphismus η explizit zu erwähnen, falls keine Verwechslung möglich ist. Weiterhin betrachten wir den präfixfreien Teil IP_{s} von IM_{s},

IP_{s} := IM_{s} \ IM_{s}IM_{+} (mit IM_{+} = IM \ 1)

IP_{s} besteht also aus den Spuren, deren η-Bild s ist und die keinen echten Präfix in IM_{s} besitzen. Bezüglich dem Homomorphismus η werden wir im ganzen Abschnitt voraussetzen, daß er surjektiv ist und eine alphabetische Information implizit beinhaltet. Für alle t, t′ ∈ IM(Σ, D) soll gelten: mit η(t) = η(t′) folgt alph(t) = alph(t′). Diese Eigenschaft kann leicht erzwungen werden, wenn wir S durch ein Untermonoid von S × P(Σ) ersetzen, wobei die Multiplikation in S × P(Σ) durch (s, A)(s′, A′) = (ss′, A ∪ A′) erklärt wird, (1, ∅) die neue Identität bildet und t ⟼ (η(t), alph(t)) der neue Homomorphismus ist. Damit und aufgrund der Surjektivität von η können wir alph(s) für s ∈ S als alph(s) = alph(t) für ein t ∈ η^{−1}(s) definieren. Die Menge der idempotenten Elemente von S, {e ∈ S | e^{2} = e}, wird mit E(S) bezeichnet. Wie wir im Abschnitt 1.3 gesehen haben, kann eine Sprache L ∈ Rec(IR), die von η : IM(Σ, D) → S erkannt wird, als Vereinigung von Sprachen der Form IM_{s}IM_{e}^{ω}, mit (s, e) ∈ P_{L} = {(s, e) | se = s, e ∈ E(S), IM_{s}IM_{e}^{ω} ∩ L ≠ ∅} dargestellt werden. Da es sich im allgemeinen um keine disjunkte Vereinigung handelt, wollen wir zunächst untersuchen, unter welchen Bedingungen zwei Mengen IM_{s}IM_{e}^{ω} und IM_{s′}IM_{e′}^{ω} einen nichtleeren Durchschnitt haben.

Zwei Paare (s, e), (s′, e′) ∈ S × E(S) mit se = s, s′e′ = s′ heißen konjugiert^{1}, wenn x, y ∈ S derart existieren, daß gilt:

e = xy, e′ = yx und s′ = sx.

Bemerkung 2.1.1 Die obige Definition ist wegen s = se = sxy = s′y symmetrisch. Weiterhin stellt die Konjugation eine Äquivalenzrelation auf der Menge {(s, e) ∈ S × E(S) | se = s} dar, wie man leicht sehen kann.

Der folgende Satz gibt uns nun eine Charakterisierung für den nichtleeren Durchschnitt zweier Mengen IM_{s}IM_{e}^{ω} und IM_{s′}IM_{e′}^{ω}.

Satz 2.1.2 Sei S ein endliches Monoid und η : IM(Σ, D) → S ein Homomorphismus. Es gilt IM_{s}IM_{e}^{ω} ∩ IM_{s′}IM_{e′}^{ω} ≠ ∅ genau dann, wenn die Paare (s, e) und (s′, e′) konjugiert sind.

Beweis: Die Definition von konjugierten Paaren und die Surjektivität von η zeigen, daß die Bedingung hinreichend ist. Umgekehrt sei t ∈ IM_{s}IM_{e}^{ω} ∩ IM_{s′}IM_{e′}^{ω} gegeben. Wir können also t auf zweifache Art faktorisieren, t = t_{0}t_{1} … = t′_{0}t′_{1} … so, daß t_{0} ∈ IM_{s}, t′_{0} ∈ IM_{s′}, t_{n} ∈ IM_{e} und t′_{n} ∈ IM_{e′}, n ≥ 1, gelten. Da wir Faktoren t_{n} (bzw. t′_{n}) mit n ≥ 1 zusammenfassen können (e, e′ ∈ E(S)), dürfen wir aus Symmetriegründen voraussetzen, daß für alle n ≥ 0 gilt:

1Siehe [PP93].

t′_{0}t′_{1} … t′_{n} ≤ t_{0}t_{1} … t_{n} ≤ t′_{0}t′_{1} … t′_{n+1} .

Damit existieren Folgen (u_{n})_{n≥0}, (v_{n})_{n≥0} ⊆ IM(Σ, D) mit:

t_{0}t_{1} … t_{n} = t′_{0}t′_{1} … t′_{n}u_{n} und
t′_{0}t′_{1} … t′_{n+1} = t_{0}t_{1} … t_{n}v_{n}

Daraus ergeben sich die Beziehungen

t_{n+1} = v_{n}u_{n+1}, t′_{n+1} = u_{n}v_{n}, t_{0} = t′_{0}u_{0} und
t = t′_{0}u_{0}v_{0}u_{1}v_{1} ….

Es seien nun 0 ≤ i < j so, daß η(u_{i}) = η(u_{j}) =: x gilt (die Existenz wird durch die Endlichkeit von S garantiert). Mit y := η(v_{i}u_{i+1} … v_{j−1}) erhalten wir abschließend:

s = η(t_{0}t_{1} … t_{i}) = η(t′_{0}t′_{1} … t′_{i−1})η(u_{i}) = s′x,
e′ = η(u_{i}v_{i} … u_{j−1}v_{j−1}) = xy und
e = η(v_{i}u_{i+1} … v_{j−1}u_{j}) = yx .
□

Korollar 2.1.3 Seien η : IM(Σ, D) → S ein Homomorphismus, S ein endliches Monoid und L = ⋃_{(s,e)∈P_{L}} IM_{s}IM_{e}^{ω} mit P_{L} = {(s, e) ∈ S×E(S) | ∅ ≠ IM_{s}IM_{e}^{ω} ⊆ L}. Dann wird L von η genau dann erkannt, wenn P_{L} unter Konjugation abgeschlossen ist.

Beweis: Wird L von η erkannt, so gilt auch P_{L} = {(s, e) ∈ S × E(S) | IM_{s}IM_{e}^{ω} ∩ L ≠ ∅} und damit folgt die Aussage. Sei P_{L} unter Konjugation abgeschlossen und sei (s, e) so, daß IM_{s}IM_{e}^{ω} ∩ L ∋ u für ein u ∈ IR(Σ, D). Aufgrund von u ∈ L existiert ein Paar (s′, e′) ∈ P_{L} mit u ∈ IM_{s′}IM_{e′}^{ω}, und dieses Paar ist nach Satz 2.1.2 konjugiert mit (s, e). Da schließlich P_{L} unter Konjugation abgeschlossen ist, erhalten wir (s, e) ∈ P_{L}. □

Im folgenden benötigen wir für A ⊆ Σ die Bezeichnungen Inf(A) und IR_{A} (vgl. Beispiel 1.3.7):

Inf(A) = { t ∈ IR(Σ, D) | alphinf(t) = A },
IR_{A} = { t ∈ IR(Σ, D) | D(alphinf(t)) = D(A) },

wobei für t ∈ IR(Σ, D) gilt alphinf(t) = {a ∈ Σ | |t|_{a} = ω}. Speziell werden wir die Bezeichnungen Inf(s) bzw. IR_{s} (s ∈ S) verwenden, und zwar als Abkürzungen für Inf(A) bzw. IR_{A}, wobei A = alph(s) gilt.

Bemerkung 2.1.4 Im Spezialfall der vollständigen Abhängigkeitsrelation D = Σ × Σ gilt IR_{A} = Σ^{ω} falls A ≠ ∅, bzw. IR_{∅} = Σ^{∗}.

Für die nun folgende Definition deterministischer Sprachen benötigen wir zuerst den für partielle Ordnungen üblichen Begriff einer gerichteten Menge:

Definition 2.1.5 Eine nichtleere Menge Y ⊆ IM(Σ, D) heißt gerichtet, wenn stets gilt, daß mit t_{1}, t_{2} ∈ Y eine obere Schranke t von t_{1}, t_{2} mit t ∈ Y existiert.

In [GR93, Kwi90] wurde gezeigt, daß jede gerichtete Menge reeller Spuren ein Supremum besitzt.

Definition 2.1.6 Sei L ⊆ IM(Σ, D). Wir definieren \overrightarrow{L} = \{t ∈ IR(Σ, D) | t = ⊔Y für eine gerichtete Menge Y ⊆ L}. Eine deterministische reelle Spursprache ist eine endliche Vereinigung von Sprachen \overrightarrow{L} ∩ IR_{A}, wobei A ⊆ Σ und L ∈ Rec(IM) eine erkennbare Sprache ist. Die Familie der deterministischen reellen Spursprachen wird mit DRec(IR) bezeichnet.

Bemerkung 2.1.7

1. Es ist leicht zu sehen, daß jede reelle Spursprache der Form \overrightarrow{L} mit L ∈ Rec(IM) erkennbar ist. Sei η : IM(Σ, D) → S ein Homomorphismus und S ein endliches

Monoid so, daß L von η erkannt wird. Es gilt dann \overrightarrow{L} = ⋃_{(s,e)∈P} IM_{s}IM_{e}^{ω}, mit P = {(s, e) ∈ S × E(S) | se = s, s ∈ η(L)}, wobei die rechte Seite der letzten Gleichung aufgrund von Abschlußeigenschaften von Rec(IR) (siehe [GP92]) eine erkennbare Menge ist.

2. Im Gegensatz zur Definition von \overrightarrow{L} im Wortfall verlangen wir nicht, daß die gerichtete Menge Y ⊆ L unendlich sein soll und damit erhalten wir die Beziehung L ⊆ \overrightarrow{L}. Die klassische Definition entspricht dann der Einschränkung \overrightarrow{L} ∩ Σ^{ω}, die hier über die Durchschnitte mit IR_{A}, A ≠ ∅, erreicht wird (siehe Bemerkung 2.1.4).

Die folgenden Sätze stellen die technische Grundlage aller Ergebnisse dar. Wir beginnen mit dem bekannten Lemma von Levi [Lev44].

Lemma 2.1.8 ([CP85]) Es seien t_{1}, t_{2}, x_{1}, x_{2} ∈ IM(Σ, D) mit t_{1}x_{1} = t_{2}x_{2}. Dann gilt

t_{1} = pf, t_{2} = pg, x_{1} = gy, und x_{2} = fy

für p = t_{1} ⊓ t_{2} und geeignete f, g, y ∈ IM(Σ, D) so, daß alph(f) × alph(g) ⊆ I.

Lemma 2.1.9 Sei (t_{n})_{n≥0} ⊆ IM(Σ, D) eine Folge endlicher Spuren so, daß ⨆_{n≥0} t_{n} existiert. Dann existiert eine unendliche Unterfolge von Indizes J ⊆ IN so, daß (t_{i})_{i∈J} bzgl. der Präfixordnung eine monoton wachsende Folge ist.

Beweis: Die Existenz von ⨆_{n≥0} t_{n} erlaubt uns, Lemma 2.1.8 anzuwenden und damit erhalten wir für i < j Spuren p_{ij} := t_{i} ⊓ t_{j} bzw. f_{ij}, g_{ij} ∈ IM(Σ, D) mit:

t_{i} = p_{ij}f_{ij}, t_{j} = p_{ij}g_{ij} und alph(f_{ij}) × alph(g_{ij}) ⊆ I .

Für ein festes i können wir ohne Einschränkung annehmen, daß p_{ij} = p_{i} (bzw. f_{ij} = f_{i}) für geeignete p_{i} (bzw. f_{i}) und alle j > i gilt. (Dafür benötigen wir natürlich eine geeignete unendliche Indexunterfolge.) Damit können die obigen Gleichungen folgendermaßen umgeschrieben werden:

t_{i} = p_{i}f_{i}, t_{j} = p_{i}g_{ij} und alph(f_{i}) × alph(g_{ij}) ⊆ I .

Aufgrund der Konstruktion erhalten wir für i < j die Beziehungen p_{i} ≤ t_{j} bzw. p_{i} ≤ t_{k} für alle j ≤ k. Mit p_{j} = t_{j} ⊓ t_{k} für alle j ≤ k gilt dann auch p_{i} ≤ p_{j}. Weiterhin gilt für alle i < j:

t_{j} = p_{i}g_{ij} = p_{j}f_{j} .

Aus alph(f_{j}) ⊆ alph(g_{ij}) (wegen p_{i} ≤ p_{j}) folgt nun mit der obigen Unabhängigkeitsbeziehung alph(f_{i}) × alph(f_{j}) ⊆ I. Wegen der Endlichkeit von Σ bedeutet dies, daß f_{i} = 1 für fast alle i gilt. Wir können daher eine unendliche Indexfolge J ⊆ IN so bestimmen, daß f_{i} = 1 für alle i ∈ J gilt und damit ist (t_{i})_{i∈J} eine monoton wachsende Spurfolge. □

Bemerkung 2.1.10 Man beachte, daß im letzten Hilfssatz nicht die Erhaltung des Supremums der ursprünglichen Folge gefordert wird, d.h. es wird nicht verlangt, daß ⨆_{i∈J} t_{i} = ⨆_{n≥0} t_{n} gelten soll. Diese Forderung kann auch nicht gestellt werden, wie das folgende Beispiel zeigt. Sei Σ = {a, b, c}, D = {(a, a), (b, b), (c, c)} und

t_{n} = \{ \begin{matrix}a^{2}bc^{n} & für n gerade \\ ab^{2}c^{n} & für n ungerade \end{matrix}

Es gilt ⨆_{n≥0} t_{n} = a^{2}b^{2}c^{ω}, aber weder ⨆_{n≥0} t_{2n} = a^{2}bc^{ω} noch ⨆_{n≥0} t_{2n+1} = ab^{2}c^{ω} ist gleich a^{2}b^{2}c^{ω}.

Satz 2.1.11 Gegeben seien die Folgen (t_{n})_{n≥0}, (w_{n})_{n≥0} ⊆ IM(Σ, D) mit der Eigenschaft, daß { t_{n}w_{n} | n ≥ 0 } eine unendliche, gerichtete Menge ist. Sei x = ⨆_{n≥0} t_{n}w_{n}. Dann existieren eine Unterfolge von Indizes (n_{i})_{i≥0} ⊆ IN und Folgen endlicher Spuren (s_{i})_{i≥0},(u_{i})_{i≥0}, (v_{i})_{i≥0} ⊆ IM(Σ, D) so, daß alph(v_{i}) × alph(s_{j}u_{j}) ⊆ I für alle 0 ≤ i < j, wobei für i ≥ 0 die Spuren t_{n_{i}}, w_{n_{i}} folgende Gestalt haben:

t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i} und
w_{n_{i}} = u_{i} v_{0} ⋯ v_{i−1}v_{i} .

Beweis: Da { t_{n}w_{n} | n ≥ 0 } gerichtet ist, dürfen wir ohne Einschränkung annehmen, daß t_{n}w_{n} ≤ t_{n+1}w_{n+1} für alle n ≥ 0 gilt. Weiterhin können wir mit Lemma 2.1.9 annehmen, daß die Folge (t_{n})_{n≥0} monoton wachsend ist. Für 0 ≤ i < j definieren wir die Folge (x_{i,j})_{i,j≥0} ⊆ IM(Σ, D) durch t_{j} = t_{i} x_{ij}. Aufgrund der Links-Kürzbarkeit von IM(Σ, D) ergibt sich aus den bisherigen Beziehungen w_{i} ≤ x_{ij} w_{j}. Die Anwendung des Lemma von Levi ergibt endliche Spuren u_{ij}, s_{ij}, y_{ij} mit alph(s_{ij}) × alph(y_{ij}) ⊆ I und

w_{i} = u_{ij} y_{ij}, x_{ij} = u_{ij} s_{ij}, y_{ij} ≤ w_{j} .

Wir betrachten nun für ein festes i ≥ 0 eine Unterfolge von Indizes so, daß für geeignete u_{i}, y_{i} gilt: u_{ij} = u_{i} und y_{ij} = y_{i}, für alle i < j. Damit lassen sich die obigen Gleichungen umschreiben in alph(s_{ij}) × alph(y_{i}) ⊆ I und

w_{i} = u_{i}y_{i}, x_{ij} = u_{i}s_{ij}, y_{i} ≤ w_{j} .

Wir werden im folgenden s_{i,i+1} mit s_{i+1} (bzw. x_{i,i+1} mit x_{i}) bezeichnen und erhalten

x_{ij} = x_{i}x_{i+1} ⋯ x_{j−1} = (u_{i}s_{i+1})(u_{i+1}s_{i+2}) ⋯ (u_{j−1}s_{j}) = u_{i}s_{ij} .

Damit folgt s_{ij} = s_{i+1}u_{i+1}s_{i+2} ⋯ u_{j−1}s_{j}. Mit der Bedingung alph(s_{ij})×alph(y_{i}) ⊆ I ergibt dies alph(y_{i}) × alph(s_{j}u_{j}) ⊆ I für alle 0 ≤ i < j. Weiterhin gilt y_{i} ≤ w_{i+1} = u_{i+1}y_{i+1}, und damit auch y_{i} ≤ y_{i+1} für i ≥ 0 (wegen alph(y_{i}) × alph(u_{i+1}) ⊆ I). Schließlich können wir mit y_{i} ≤ y_{i+1} Spuren (v_{i})_{i≥0} durch y_{i+1} = y_{i}v_{i+1} definieren (setze v_{0} = y_{0}) und erhalten abschließend alph(v_{i})×alph(s_{j}u_{j}) ⊆ I für j > i ≥ 0, und (vgl. Abbildung 2.1):

t_{i} = t_{0}x_{0} ⋯ x_{i−1} = s_{0}u_{0}s_{1} ⋯ u_{i−1}s_{i} (mit s_{0} := t_{0}),
w_{i} = u_{i} y_{i} = u_{i} v_{0}v_{1} ⋯ v_{i} .
□

Bemerkung 2.1.12 Durch Zusammenfassen von Faktoren und Umnumerierung kann die Existenz von Spurfolgen (s_{i})_{i≥0}, (u_{i})_{i≥0}, (v_{i})_{i≥0} mit alph(v_{i})×alph(s_{j}u_{j}) ⊆ I für alle i ≥ 0, j > 0 gezeigt werden.

Beispiel 2.1.13 Sei (Σ, D) = a − b − c − d. Wir betrachten die Folgen (t_{n})_{n≥0}, (w_{n})_{n≥0} ⊆ IM(Σ, D), t_{n} = c(ba)(b^{2}a) ⋯ (b^{n}a)b und w_{n} = d^{n+1}b^{n}a. Es gilt x = ⨆_{n≥0}(t_{n}w_{n}) = cd^{ω}(ba)(b^{2}a) . . .. Mit den Bezeichnungen aus Satz 2.1.11 erhalten wir s_{0} = cb, s_{i} = b für i ≥ 1, u_{i} = b^{i}a und v_{i} = d für i ≥ 0. Für die nachfolgenden Betrachtungen sei angemerkt, daß (w_{n})_{n≥0} eine präfix-freie Folge ist. Es existiert aber keine erkennbare, präfix-freie Menge K, die (w_{n})_{n≥0} enthält. Ersetzt man die Folge (w_{n})_{n≥0} durch (w′_{n})_{n≥0} mit w′_{n} = db^{n}a, so ändert sich die Folge (v_{i})_{i≥0} zu v′_{0} = d und v′_{i} = 1, für i ≥ 1. Das folgende Korollar zeigt, daß v′_{0} ≠ 1 durch d ∉ D(alphinf(x)) ermöglicht wird.

[figure: s_{0}; u_{0}; v_{0}; s_{1}; u_{1}; v_{1}; s_{i−1}; u_{i−1}; v_{i−1}; s_{i}; u_{i}; v_{i}; …; …; t_{i}; w_{i}]

Abbildung 2.1: Die Faktorzerlegung von t_{i}w_{i}, wobei w_{i} aus den markierten Bereichen besteht.

Korollar 2.1.14 Gegeben seien L, K ⊆ IM(Σ, D) mit K erkennbar und präfixfrei, d.h., KIM_{+}∩K = ∅. Seien (t_{n})_{n≥0} ⊆ L, (w_{n})_{n≥0} ⊆ K so, daß { t_{n}w_{n} | n ≥ 0 } unendlich und gerichtet ist, und sei x = ⨆{ t_{n}w_{n} | n ≥ 0 }. Schließlich gelte D(alph(y)) ⊆ D(alphinf(x)), für alle y ∈ K. Dann existieren eine Unterfolge von Indizes (n_{i})_{i≥0} ⊆ IN und Spurfolgen (s_{i})_{i≥0}, (u_{i})_{i≥0} ⊆ IM(Σ, D) mit x = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 } so, daß gilt:

t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i}  und  w_{n_{i}} = u_{i}.

Beweis: Wir können Satz 2.1.11 anwenden und erhalten eine (unendliche) Folge von Indizes und Spurfolgen (s_{i})_{i≥0}, (u_{i})_{i≥0}, (v_{i})_{i≥0} ⊆ IM(Σ, D) mit x = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 }, t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i}, w_{n_{i}} = u_{i}v_{0} ⋯ v_{i−1}v_{i}, und alph(v_{i})×alph(s_{j}u_{j}) ⊆ I, für alle 0 ≤ i < j. Wir werden zeigen, daß die zusätzlichen Bedingungen über die Präfixfreiheit von K und über alphinf(x) dazu führen, daß v_{i} = 1 für alle i angenommen werden kann. Sei η : IM(Σ, D) → S ein Homomorphismus auf ein endliches Monoid S so, daß K von η erkannt wird. Wir dürfen ohne Einschränkung annehmen, daß η(u_{i}) = η(u_{j}) für alle i, j gilt (dafür wählen wir eine Unterfolge von Indizes mit der Eigenschaft η(u_{m_{i}}) = η(u_{m_{j}}) für alle i, j und definieren s_{m_{i}} als s_{m_{i−1}+1}u_{m_{i−1}+1} ⋯ s_{m_{i}} bzw. v_{m_{i}} als v_{m_{i−1}+1}v_{m_{i−1}+2} ⋯ v_{m_{i}} um). Nun gilt u_{i}v_{0} ⋯ v_{i−2}v_{i−1} ≤ w_{n_{i}} ∈ K für alle i ≥ 1. Mit der Beziehung η(u_{i}) = η(u_{i−1}) folgt unmittelbar η(u_{i}v_{0} ⋯ v_{i−2}v_{i−1}) = η(u_{i−1}v_{0} ⋯ v_{i−2}v_{i−1}) = η(w_{i−1}), daher gilt u_{i}v_{0} ⋯ v_{i−2}v_{i−1} ∈ K, für alle i ≥ 1. Da K präfix-frei ist, muß damit v_{i} = 1 für alle i ≥ 1 gelten. Zusätzlich gilt für i = 0: Mit alph(v_{0})×alph(s_{i}u_{i}) ⊆ I folgt alph(v_{0}) ∩ D(alphinf(x)) = ∅. Da aber alph(v_{0}) ⊆ alph(w_{i}) und w_{i} ∈ K gelten, würde v_{0} ≠ 1 der zweiten zusätzlichen Voraussetzung widersprechen. Es folgt

\begin{matrix}t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i} und \\ w_{n_{i}} = u_{i}. \end{matrix}

□

2.2 Äquivalenz von Rec(IR) und dem Booleschen Abschluß der Familie deterministischer Sprachen

Ein erster Schritt für die Verallgemeinerung des Theorems von McNaughton auf reelle Spursprachen wird die Äquivalenz der Klasse der erkennbaren reellen Spursprachen und dem Booleschen Abschluß der Klasse der deterministischen Sprachen sein. Die nächsten Sätze stellen Verallgemeinerungen analoger Ergebnisse im Spezialfall der ω-Wortsprachen dar (vgl. [PP93]). Auf den ersten Blick besteht ein Unterschied durch die zusätzlichen alphabetischen Informationen, die bei Spursprachen mitgeführt werden. Man beachte jedoch, daß es sich dabei im Spezialfall D = Σ × Σ jeweils um triviale Durchschnitte mit Σ^{ω} handelt (vgl. Bemerkung 2.1.4). Im folgenden betrachten wir für ein endliches Monoid S und s ∈ S die Teilmenge der idempotenten Elemente E_{s} = {e ∈ E(S) | se = s} und die darauf definierte Halbordnung ≤, mit e ≤ f genau dann, wenn fe = e gilt. Die Notation e < f bedeutet, daß e ≤ f und f ≰ e gelten. Allgemeiner ist auf S die Halbordnung ≤_{R} erklärt durch s ≤_{R} s′ genau dann, wenn sS ⊆ s′S. Beachte, daß die Halbordnung ≤ die Einschränkung von ≤_{R} auf E_{s} ist. Weiterhin verwenden wir die links-invariante Äquivalenzrelation R auf S, mit s R s′ genau dann, wenn die zugehörigen Rechtsideale gleich sind, d.h. sS = s′S.

Satz 2.2.1 Sei S ein endliches Monoid, s, e ∈ S mit se = s, e ∈ E(S) und η : IM(Σ, D) → S ein Epimorphismus. Dann gilt:

IM_{s}IM_{e}^{ω} ⊆ \overrightarrow{IM_{s}IP_{e}} ∩ IR_{e} ⊆ ⋃_{f≤e} IM_{s}IM_{f}^{ω} .

Beweis: Die erste Inklusion ist leicht einzusehen, wenn man bedenkt, daß für eine Spur u = u_{0}u_{1} … mit u_{0} ∈ IM_{s} und u_{n} ∈ IM_{e} für n ≥ 1, geeignete (u′_{n})_{n≥1} ⊆ IP_{e} gewählt werden können. Damit erreicht man u = ⊔_{n≥0}u_{0}u_{1} ⋯ u_{n}u′_{n+1}, wobei gilt: u_{0}u_{1} ⋯ u_{n}u′_{n+1} ∈ IM_{s}IP_{e}. Für die Umkehrung wenden wir Korollar 2.1.14 auf die Spur x = ⊔_{n≥0}t_{n}w_{n} an, wobei (t_{n})_{n≥0} ⊆ IM_{s}, (t′_{n})_{n≥0} ⊆ IP_{e} und D(alphinf(x)) = D(alph(e)). Dies ergibt die Existenz einer Indexfolge (n_{i})_{i≥0} ⊆ IN und zweier Spurfolgen (s_{i})_{i≥0}, (u_{i})_{i≥0} ⊆ IM(Σ, D) so, daß t_{n_{i}} und w_{n_{i}} folgendermaßen dargestellt werden können:

t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i} und w_{n_{i}} = u_{i},

wobei weiterhin gilt x = ⊔_{i≥0}t_{n_{i}}w_{n_{i}}. Die Spur x = s_{0}u_{0}s_{1} … kann nun so faktorisiert werden, daß für eine Indexfolge (m_{i})_{i≥0} und Monoidelemente r ∈ S, f ∈ E(S) gilt:

r = η(s_{0}u_{0} ⋯ s_{m_{1}}) und f = η(u_{m_{i}}s_{m_{i}+1} ⋯ s_{m_{j}}), für alle 0 ≤ i < j .

Es ist leicht zu sehen, daß rf = r folgt. Weiterhin gilt natürlich s = r, sowie f ∈ η(u_{n})S = eS, und damit f ≤_{R} e, d.h. f ≤ e. Dies zeigt x ∈ ⋃_{f≤e} IM_{s}IM_{f}^{ω}.

□

Korollar 2.2.2 Mit den Voraussetzungen des Satzes 2.2.1 gilt:

1. IM_{e}^{ω} = \overrightarrow{IM_{e}IP_{e}} ∩ IR_{e}

2. ⋃_{f≤e} IM_{s}IM_{f}^{ω} = ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}).

Beweis: (1) Man beachte, daß mit s = e in Satz 2.2.1 ef = e gilt. Weiterhin ist f ≤ e gleichbedeutend mit ef = f, woraus e = f und die erste Aussage folgt.

(2) Mit Satz 2.2.1 erhalten wir:

⋃_{f≤e} IM_{s}IM_{f}^{ω} ⊆ ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) ⊆
⋃_{f≤e} ⋃_{h≤f} IM_{s}IM_{h}^{ω} ⊆ ⋃_{h≤e} IM_{s}IM_{h}^{ω},

wobei die letzte Inklusion mit der Transitivität der Halbordnung ≤ folgt. □

Wir können nun das Hauptergebnis dieses Abschnitts zeigen, und zwar die Äquivalenz von Rec(IR) und dem Booleschen Abschluß der Familie der deterministischen Sprachen reeller Spuren DRec(IR). Der Beweis verläuft analog zu [PP93]. Erneut erhalten wir die Verallgemeinerung des entsprechenden Resultats für ω-Wortsprachen.

Theorem 2.2.3 Sei S ein endliches Monoid und η : IM(Σ, D) → S ein surjektiver Homomorphismus, der L ⊆ IR(Σ, D) erkennt. Sei weiterhin P_{L} = { (s, e) ∈ S × E(S) | se = s, IM_{s}IM_{e}^{ω} ∩ L ≠ ∅ }. Dann läßt sich L darstellen als

L = ⋃_{(s,e)∈P_{L}} ( ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) \ ⋃_{f<e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f})) .

Beweis: Es seien (s, e) ∈ P_{L} und f ∈ E(S) mit f R e. Damit sind die Paare (s, e) und (s, f) mit x = e und y = f konjugiert, woraus mit Lemma 2.1.2 (s, f) ∈ P_{L} folgt. Dies ergibt zusammen mit der trivialen Beziehung e R e:

L = ⋃_{(s,e)∈P_{L}} IM_{s}IM_{e}^{ω} ⊆ ⋃_{(s,e)∈P_{L}} ⋃_{fRe} IM_{s}IM_{f}^{ω} ⊆ L ,

woraus die Darstellung L = ⋃_{(s,e)∈P_{L}} ⋃_{f R e} IM_{s}IM_{f}^{ω} folgt. Damit genügt es, die Sprache ⋃_{f R e} IM_{s}IM_{f}^{ω} als Boolesche Kombination deterministischer Sprachen darzustellen. Definitionsgemäß ist f R e äquivalent zu ef = f und fe = e. Somit gilt f R e genau dann, wenn f ≤ e und f ≮ e gelten. Die folgende Feststellung spielt eine wichtige Rolle im Beweis. Die Beziehung f < e hat nämlich zur Folge, daß IM_{s}IM_{e}^{ω} ∩ IM_{s}IM_{f}^{ω} = ∅ (∗) gilt. Wären IM_{s}IM_{e}^{ω} und IM_{s}IM_{f}^{ω} nicht disjunkt, so wären (s, e) und (s, f) nach Satz 2.1.2 konjugiert, d.h. es würde sx = s, e = xy und f = yx für gewisse x, y ∈ S gelten. Damit erhielten wir für n ≥ 0:

e = e^{2} = xyxy = xfy =^{f<e} xefy = x^{n}e(fy)^{n}.

Da S endlich ist, existieren n, q ∈ IN, q ≠ 0 so, daß für alle z ∈ S gilt: z^{n+q} = z^{n}.

Dies führt jedoch über e = x^{n}e(fy)^{n} = x^{n}e(fy)^{n+q} = e(fy)^{q} = ef(yf)^{q−1}y ∈^{ef=f}

fS zu e ≤ f (i.e. f ≮ e), und widerspricht damit der Voraussetzung über f, e. Schließlich erhalten wir

⋃_{f R e} IM_{s}IM_{f}^{ω} = ⋃_{f≤e,f≮e} IM_{s}IM_{f}^{ω}
=^{(∗)} ⋃_{f≤e} IM_{s}IM_{f}^{ω} \ ⋃_{f<e} IM_{s}IM_{f}^{ω}  (wegen f R e, h < e ⇒ h < f)
= ⋃_{f≤e} IM_{s}IM_{f}^{ω} \ ⋃_{f<e} ⋃_{g≤f} IM_{s}IM_{g}^{ω}
=^{2.2.2} ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) \ ⋃_{f<e} ⋃_{g≤f}(\overrightarrow{IM_{s}IP_{g}} ∩ IR_{g})
= ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) \ ⋃_{f<e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) .
□

Mit dem Abschluß von Rec(IR) unter Booleschen Operationen und der Erkennbarkeit deterministischer Sprachen erhalten wir das angekündigte Ergebnis:

Korollar 2.2.4 Es gilt:

Rec(IR) = Bool (DRec(IR)).

2.3 Deterministische asynchrone Muller Automaten

Thema dieses Abschnitts ist eine Konstruktion deterministischer asynchron-zellu-lären Muller Automaten für die Klasse der deterministischen reellen Spursprachen. Mit der in Abschnitt 2.2 gezeigten Äquivalenz von Rec(IR) und dem Booleschen Abschluß der Klasse der deterministischen Sprachen genügt es nämlich, asynchron-zelluläre Muller für diese Unterklasse anzugeben. Genauer gesagt, werden wir Automaten für Sprachen \overrightarrow{L} mit L ∈ Rec(IM) konstruieren (für Sprachen IR_{A}, A ⊆ Σ, vgl. Beispiel 1.3.7).

Die Idee der Konstruktion besteht in der Einschränkung auf gewisse Sprachen \overrightarrow{L}, deren Elemente eine spezielle Form im unendlichen Teil besitzen und daher mit lokalen Bedingungen erkennbar sind. Konkret werden wir uns auf ein Alphabet A mit A = alphinf(t) für alle t ∈ \overrightarrow{L} einschränken. Anschließend betrachten

wir nur Sprachen L mit der Eigenschaft, daß die Spuren aus \overrightarrow{L} mit L-Präfixen approximierbar sind, die für jede Zusammenhangskomponente von A genau ein maximales Element besitzen. Das folgende Lemma zeigt, daß wir uns auf solche \overrightarrow{L} einschränken dürfen.

Lemma 2.3.1 Sei A ⊆ Σ und A = ⋃_{i=1}^{k} A_{i} die Zerlegung in Zusammenhangskomponenten, d.h. es gilt:

A_{i} × A_{j} ⊆ I  für i ≠ j, und
A_{i} ist zusammenhängend für alle i = 1, …, k.

Seien weiterhin a_{i} ∈ A_{i}, i = 1, …, k, fest gewählt. Wir definieren folgende erkennbare Mengen:

IM_{A,i} = { t | alph(t) = A_{i} und max(t) = {a_{i}} }
IP_{A,i} = IM_{A,i} \ IM_{A,i}IM_{+} .

Damit gilt für L ⊆ IM(Σ, D):

\overrightarrow{L} ∩ Inf(A) = \overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A).

Beweis: Sei u ∈ \overrightarrow{L} mit alphinf(u) = A = ⋃_{i=1}^{k} A_{i} und betrachten wir eine Zerlegung u = u_{0}u_{1}u_{2} … von u, wobei alph(u_{n}) = A für n ≥ 1, und u_{0}u_{1} ⋯ u_{n} ∈ L für n ≥ 0. Weiterhin können wir jedes u_{n} als Produkt u_{n} = u_{n,1} ⋯ u_{n,k} mit alph(u_{n,i}) = A_{i}, 1 ≤ i ≤ k, schreiben. Betrachte für n ≥ 1 und 1 ≤ i ≤ k die Folge u_{n,i}u_{n+1,i} . . .. Da die Teilalphabete A_{i} zusammenhängend sind, besitzt diese Folge ein (bzgl. der Präfixordnung) kleinstes Präfix u′_{n,i} mit max(u′_{n,i}) = {a_{i}} und alph(u′_{n,i}) = A_{i}. Damit sind k Folgen (u′_{n,i})_{n≥1} ⊆ IP_{A,i} definiert so, daß gilt: u_{0} ⋯ u_{n−1}u′_{n,1} ⋯ u′_{n,k} ∈ LIP_{A,1} ⋯ IP_{A,k} für n ≥ 1. Es gilt natürlich weiterhin

u = ⨆\{ u_{0} ⋯ u_{n−1}u′_{n,1} ⋯ u′_{n,k} | n ≥ 1 \}. Daraus folgt u ∈ \overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A). Für die Rückrichtung betrachte x = ⨆{t_{n}w_{n} | t_{n} ∈ L, w_{n} ∈ IP_{A,1} ⋯ IP_{A,k}, n ≥ 0} mit alphinf(x) = A. Da IP_{A,1} ⋯ IP_{A,k} erkennbar und präfixfrei ist, zusammen mit der Beziehung D(alph(IP_{A,1} ⋯ IP_{A,k})) = D(A), ergibt Korollar 2.1.14 eine Indexfolge (n_{i})_{i≥0} ⊆ IN und zwei Folgen endlicher Spuren (s_{i})_{i≥0}, (u_{i})_{i≥0} ⊆ IM(Σ, D) mit x = ⨆_{i≥0} t_{n_{i}}w_{n_{i}} und folgender Darstellung für t_{n_{i}}, w_{n_{i}}:

t_{n_{i}} = s_{0}u_{0}s_{1} ⋯ s_{i−1}u_{i−1}s_{i} ∈ L
w_{n_{i}} = u_{i} ∈ IP_{A,1} ⋯ IP_{A,k} ,

woraus x ∈ \overrightarrow{L} direkt folgt. □

Für das nachfolgende Theorem verwenden wir zur Vereinfachung folgende grundlegende Eigenschaft der asynchron-zellulären Automaten, die aus der Konstruktion von Zielonka hervorgehen (d.h., die auf einer asynchronen Abbildung beruhen): Die lokalen Zustände der maximalen Elemente einer Spur legen bereits die Akzeptanz durch den Automaten fest (vgl. die Anmerkung in Abschnitt 1.2).

Theorem 2.3.2 Jede reelle Spursprache der Form \overrightarrow{L}, mit L ∈ Rec(IM) erkennbar, kann von einem deterministischen asynchron-zellulären Muller Automaten erkannt werden.

Beweis: Wegen der Beziehung

\overrightarrow{L} = ⋃_{A⊆Σ}(\overrightarrow{L} ∩ Inf(A))
=^{2.3.1} ⋃_{A⊆Σ}(\overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A)),

wobei die Mengen IP_{A,1}, … IP_{A,k} wie im Lemma 2.3.1 definiert sind, genügt es offensichtlich, deterministische asynchron-zelluläre Muller Automaten für Sprachen der Form \overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A), A ≠ ∅, anzugeben. Sei dafür A′ = ((Q′_{a})_{a∈Σ}, (δ′_{a})_{a∈Σ}, q′_{0}, F′) ein asynchron-zellulärer Automat, der LIP_{A,1} ⋯ IP_{A,k} erkennt und aus der Konstruktion von Zielonka hervorgeht. Wir definieren für f ∈ F′:

L_{A,f} = { t ∈ IR(Σ, D) | alphinf(t) = A, t = ⊔_{n≥0}t_{n} mit t_{0} ≤ t_{1} ≤ …
und δ′(q′_{0}, t_{n}) = f, für n ≥ 0 }

Sei ohne Einschränkung A ≠ ∅. Wir definieren einen deterministischen asynchron-zellulären Muller Automat A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, ∅, T ) durch

• Q_{a} = Q′_{a} × ZZ/2ZZ,

• δ_{a}((q, i)_{D(a)}) = (δ′_{a}(q_{D(a)}), i_{a} + 1),

• q_{0} = (q′_{0}_{a}, 0)_{a∈Σ}, und werden zeigen, daß L_{A,f} ⊆ L(A) ⊆ \overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A) folgt. Durch die Hinzunahme der ZZ/2ZZ Komponente in jedem lokalem Zustand erreichen wir die Eigenschaft δ_{a}(s_{D(a)}) ≠ s_{a} für alle s_{a} ∈ Q_{a}, a ∈ Σ. Damit läßt sich das Alphabet alphinf(t) für t ∈ IR(Σ, D), eindeutig feststellen; es gilt a ∈ alphinf(t) genau dann, wenn |inf_{a}(t)| ≥ 2. Beachte, daß inf_{a}(t) die Menge der lokalen a-Zustände bezeichnet, die auf dem mit t beschrifteten Übergangspfad unendlich oft wiederholt werden. Die Tafel T wird nun definiert durch

T = (T_{a})_{a∈Σ} ∈ T ⟺ es existieren (i_{a})_{a∈Σ} ∈ (ZZ/2ZZ)^{Σ} mit
(i) T_{a} = {(f_{a}, i_{a})} für a ∈ Σ \ A,
(ii) (f_{a}, i_{a}) ∈ T_{a} und |T_{a}| ≥ 2, für a ∈ A .

Es ist leicht zu sehen, daß L_{A,f} ⊆ L(A) gilt. Umgekehrt sei t ∈ L(A) so, daß t mit T ∈ T akzeptiert wird. Mit der obigen Bemerkung folgt alphinf(t) = { a ∈ Σ | |T_{a}| ≥ 2 } = A, und wir können t als t = t_{0}t_{1} … faktorisieren, wobei für geeignete (i_{a})_{a∈Σ} ∈ (ZZ/2ZZ)^{Σ}) gilt:

alph(t_{n}) = A  für n ≥ 1,
δ(q_{0}, t_{0}t_{1} ⋯ t_{n})_{a} = (f_{a}, i_{a})  für a ∈ (Σ \ A) ∪ {a_{1}, …, a_{k}}, n ≥ 0,
max(t_{0} ⋯ t_{n}) ∩ A = {a_{1}, …, a_{k}} für n ≥ 0.

(Die Existenz einer derartigen Faktorisierung basiert auf der Tatsache, daß jede Zusammenhangskomponente von A = alphinf(t) genau ein a_{i}, 1 ≤ i ≤ k, enthält.) Aufgrund der Definition von LIP_{A,1} ⋯ IP_{A,k} ist andererseits max(u) ⊆ (Σ \ A) ∪ {a_{1}, …, a_{k}} für alle u ∈ LIP_{A,1} ⋯ IP_{A,k} gegeben. Mit B := (Σ \ A) ∪ {a_{1}, …, a_{k}} folgt daher:

max(LIP_{A,1} ⋯ IP_{A,k}), max(t_{0} ⋯ t_{n}) ⊆ B und
δ′(q′_{0}, t_{0} ⋯ t_{n})_{B} = f_{B}.

Mit der Bedeutung der lokalen Zustände der maximalen Elemente für die Akzeptanz (durch A′) folgt letztendlich t_{0} ⋯ t_{n} ∈ LIP_{A,1} ⋯ IP_{A,k}. □

Mit Satz 2.3.2 erhalten wir abschließend das Hauptergebnis dieses Kapitels:

Haupttheorem 2.3.3 Die Klasse der erkennbaren reellen Spursprachen ist identisch zur Klasse der Sprachen, die von deterministischen asynchron-zellulären Muller Automaten erkannt werden.

Beweis: Die erste Inklusion folgt mit Korollar 2.2.4 und Theorem 2.3.2. Für die Rückrichtung ist es leicht zu sehen, daß eine asynchron-zelluläre Muller Akzeptanzbedingung als Boolesche Kombination von asynchron-zellulären Büchi Bedingungen umgeschrieben werden kann. □

Da asynchron-zelluläre Automaten automatisch die I-Diamant Eigenschaft besitzen, können wir eine weitere automaten-theoretische Charakterisierung folgern. Man beachte, daß das folgende Ergebnis auch mit den Sätzen 2.2.4 und 3.3.2 aus dem nächsten Kapitel folgt.

Korollar 2.3.4 Jede erkennbare, abgeschlossene ω-Wortsprache kann mit einem deterministischen Muller Automaten mit I-Diamant Eigenschaft erkannt werden.

Die Frage, welche deterministischen I-Diamant Muller (bzw. Büchi) Automaten abgeschlossene Sprachen erkennen, sowie eine komplexitätstheoretische Untersuchung dieses Problems bilden das Thema von Kapitel 6.

Deterministische reelle Spursprachen

Ziel dieses Kapitels ist die nähere Untersuchung der Familie der deterministischen Spursprachen DRec(IR) (siehe Definition 2.1.6). Nach einer kurzen Einleitung, die den Abschluß dieser Sprachklasse unter Boolesche Operationen behandelt, wenden wir uns dem Problem einer geeigneten Charakterisierung durch deterministische Automaten zu. Wir zeigen, daß die Äquivalenz zwischen deterministischen Sprachen und deterministischen Büchi Automaten im Falle der asynchron (-zellulären) Automaten nicht bestehen kann. Damit ist der enge Zusammenhang, der für ω-Wortsprachen existiert, nicht auf reelle Spuren übertragbar. Wir können jedoch eine schwächere Charakterisierung angeben, wonach die deterministischen reellen Spursprachen den abgeschlossenen Wortsprachen entsprechen, die durch deterministische I-Diamant Büchi Automaten mit einer erweiterten Akzeptanzbedingung erkannt werden.

3.1 Abschlußeigenschaften deterministischer Sprachen

Wir wollen in diesem Abschnitt die Definition deterministischer Sprachen aus der Sicht des Abschlusses unter Vereinigung und Durchschnitt erläutern. Wir zeigen, daß DRec(IR) unter diesen Operationen abgeschlossen ist. Für diese Eigenschaft kann in der Definition deterministischer Sprachen als endliche Vereinigung von Sprachen \overrightarrow{L} ∩ IR_{A} mit L ∈ Rec(IM), A ⊆ Σ, weder auf die endliche Vereinigung, noch auf die Durchschnitte mit IR_{A} verzichtet werden. Direkt aus der Definition deterministischer Sprachen folgt, daß DRec(IR) unter der Vereinigung abgeschlossen ist. Es gilt auch:

Satz 3.1.1 DRec(IR) ist abgeschlossen unter Durchschnitt.

Beweis: Es genügt zu zeigen, daß \overrightarrow{L} ∩ \overrightarrow{K} eine deterministische Sprache ist, wobei L, K ∈ Rec(IM).

Da L, K erkennbar sind, können wir ohne Einschränkung von einem endlichen Monoid S und einem Homomorphismus η : IM(Σ, D) → S (mit alphabetischer Information, vgl. 2.1) ausgehen so, daß beide Sprachen von η erkannt werden.

Wir zeigen im folgenden, daß der Durchschnitt \overrightarrow{L} ∩ \overrightarrow{K} folgende Gestalt hat:

\overrightarrow{L} ∩ \overrightarrow{K} = ⋃_{{s_{1} ∈ η(L) \atop s_{1}s_{2} ∈ η(K)}} (\overrightarrow{IM_{s_{1}}IP_{s_{2}}} ∩ IR_{s_{2}}) .

Ist t ∈ \overrightarrow{L} ∩ \overrightarrow{K}, so finden wir eine geeignete Faktorisierung t = v_{0}u_{0}v_{1}u_{1} … mit v_{n}, u_{n} ∈ IM(Σ, D) so, daß für gewisse s_{1}, s_{2} ∈ S gilt: η(v_{0}u_{0} … v_{n}) = s_{1} und η(u_{n}) = s_{2} für n ≥ 0. Weiterhin fordern wir D(alph(s_{2})) = D(alphinf(t)), und schließlich wählen wir die Faktoren u_{n} präfixfrei mit den obigen Eigenschaften. Für die umgekehrte Richtung betrachten wir eine Spur t = ⨆_{n≥0} t_{n}t′_{n} mit (t_{n})_{n≥0} ⊆ IM_{s_{1}}, (t′_{n})_{n≥0} ⊆ IP_{s_{2}} und D(alph(s_{2})) = D(alphinf(t)). Die Voraussetzungen des

Korollars 2.1.14 sind erfüllt und damit folgt direkt t ∈ \overrightarrow{L}. Mit IM_{s_{1}}IP_{s_{2}} ⊆ K gilt

natürlich auch t ∈ \overrightarrow{K}. □

Die Familie der Sprachen \overrightarrow{L} mit L ∈ Rec(IM) ist im Gegensatz zu DRec(IR) nicht unter Durchschnitt abgeschlossen, wie das folgende Beispiel zeigt.

Beispiel 3.1.2 Sei Σ = {a, b} mit I = {(a, b)}. Betrachte die Sprachen L_{1} =

(aa)^{∗}(bb)^{∗} und L_{2} = abL_{1}. L_{1} und L_{2} sind beide erkennbar, aber \overrightarrow{L_{1}}∩\overrightarrow{L_{2}} = \{a^{ω}b^{ω}\}

ist das klassische Beispiel einer Sprache, die nicht in der Form \overrightarrow{L} mit L ∈ Rec(IM) dargestellt werden kann.

Schließlich sei noch erwähnt, daß DRec(IR) nicht unter Komplement abgeschlossen ist (bereits die Klasse der deterministischen Wortsprachen ist nicht abgeschlossen unter Komplement).

3.2 Deterministische Automaten für DRec(IR)

Im Kontext unendlicher Wörter entsprechen die deterministischen Sprachen \overrightarrow{L} mit L ∈ Rec(Σ^{∗}) genau den von deterministischen Büchi Wortautomaten akzeptierten Sprachen. Es stellt sich natürlich die Frage, ob die Klasse DRec(IR) nicht analogerweise durch deterministische, asynchron-zelluläre Büchi Automaten charakterisiert werden kann. Das folgende Beispiel zeigt jedoch, daß die deterministischen asynchron-zellulären Büchi Automaten ein zu schwaches Automatenmodell sind. Dies gilt sogar wenn die Akzeptanz so modifiziert werden würde, daß D(alphinf(t)) einbezogen ist.

Beispiel 3.2.1 Sei (Σ, D) = a −c −b und L = IMa^{+}b^{+} ∈ Rec(IM). Wir zeigen, daß es keinen deterministischen asynchron-zellulären Büchi Automaten gibt, der \overrightarrow{L} ∈ DRec(IR) akzeptiert. Der Einfachheit halber verwenden wir hier eine leicht veränderte Akzeptanzbedingung für asynchron-zelluläre Büchi Automaten, die sich leicht als gleichwertig zur Definition 1.3.5 nachweisen läßt. Es sei daran erinnert, daß in der Definition 1.3.5 jedes Tafelelement für jeden Buchstaben a ∈ Σ eine Teilmenge von Q_{a} enthält, deren Elemente für die Akzeptanz eines Berechnungspfades unendlich oft wiederholt werden müssen. Wir betrachten asynchron-zelluläre Büchi Automaten A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, F), wobei die Tafel F ⊆ ∏_{a∈Σ} Q_{a} × P(Σ) um eine alphabetische Komponente erweitert ist. Wir bezeichnen mit δ die globale Übergangsrelation des Automaten. Ein Berechnungspfad π = (q_{0}, a_{0}, q_{1}, a_{1}, …), mit q_{n} ∈ ∏_{a∈Σ} Q_{a}, q_{n+1} ∈ δ(q_{n}, a_{n}), und a_{n} ∈ Σ wird akzeptiert, wenn ein (f, A) ∈ F existiert so, daß gilt:

1. f_{a} ∈ inf_{a}(π) = {q_{a} | ∃^{∞}n : (q_{n})_{a} = q_{a}} für alle a ∈ Σ, und

2. A ⊆ alphinf(t).

Nehmen wir an, daß \overrightarrow{L} = L(A) für einen deterministischen asynchron-zellulären Büchi Automaten A gilt. Wir werden eine Spur u ∈ IR(Σ, D) induktiv durch eine

Sequenz (u_{n})_{n≥0} so definieren, daß u ∈ L(A), aber u ∉ \overrightarrow{L} gilt. Sei zunächst u_{0} = 1. Angenommen, für n ≥ 0 ist u_{n} ∈ IM(Σ, D) bereits definiert,

dann gilt u_{n}ca^{ω}b^{ω} ∈ \overrightarrow{L} = L(A) und damit existiert ein Paar (f_{n+1}, A_{n+1}) ∈ F womit u_{n}ca^{ω}b^{ω} akzeptiert wird; d.h. es existieren k_{n+1}, l_{n+1} > 0 so, daß gilt: δ(q_{0}, u_{n}ca^{k_{n+1}}b^{l_{n+1}}) = f_{n+1} (man beachte, daß für die vorliegende Spur die unendliche Wiederholung der lokalen Komponenten von f_{n+1} zu einer Aussage über den ”globalen“ Zustand f_{n+1} führt). Weiterhin sei m := max{i ≤ n | f_{i} = f_{n+1}}, falls der Zustand f_{n+1} in der Konstruktion bereits vorgekommen ist; sonst sei m := n + 1. Wir definieren nun u_{n+1} als

u_{n+1} = \{ \begin{matrix}u_{n} c b^{l_{n+1}} & falls m ≠ n + 1 und u_{m} ∈ IMca^{+} \\ u_{n} c a^{k_{n+1}} & sonst. \end{matrix}

Sei u := ⨆_{n≥0} u_{n} und (f, A) ∈ F ein Paar, das in der Folge (f_{n}, A_{n})_{n≥0} unendlich oft vorkommt. Durch die alternierende Definition von (u_{n})_{n≥0} gilt:

δ(q_{0}, u_{n})_{a,c} = f_{a,c} für unendlich viele u_{n} ∈ IMca^{+}
und δ(q_{0}, u_{n})_{b,c} = f_{b,c} für unendlich viele u_{n} ∈ IMcb^{+} .

und damit wird u mit (f, A) ∈ F akzeptiert, da f_{x} ∈ inf_{x}(u) für alle x ∈ {a, b, c}

gilt, zusammen mit A ⊆ alphinf(u) = Σ. Andererseits gilt aber u ∉ \overrightarrow{L}.

Abschließend sei angemerkt, daß eine zusätzliche Information wie z. B. über D(alphinf(u)) ebensowenig für die Erkennung der obigen Sprache ausreicht (es gilt D(alphinf(u)) = D(alphinf(u_{n}ca^{ω}b^{ω})) = Σ für alle n ≥ 0). Ein analoges Beispiel kann mit einem erweiterten Abhängigkeitsalphabet auch für deterministische asynchrone Büchi Automaten angegeben werden, womit auch dieses Modell für die Charakterisierung von DRec(IR) scheitert.

3.3 DRec(IR) und I-Diamant Büchi Automaten

Thema dieses Abschnitts ist eine automatentheoretische Charakterisierung der Klasse DRec(IR). Wir zeigen, daß die deterministischen reellen Spursprachen genau den abgeschlossenen (Wort-) Sprachen entsprechen, die von deterministischen I-Diamant Büchi Automaten mit verallgemeinerter Akzeptanz erkannt werden. Dabei bezeichnen wir hier als Büchi Automat ein 4-Tupel A = (Q, δ, q_{0}, F_{0}, F) mit Endzustandsmenge F_{0} ⊆ Q und Tafel F ⊆ P(Q) × P(Σ). Ein unendliches Wort w ∈ Σ^{ω} wird akzeptiert, wenn (F, A) ∈ F und ein mit w markierter Berechnungspfad π derart existieren, daß F ⊆ inf(π) und D(alphinf(w)) = D(A) gelten. Endliche Wörter werden mittels F_{0} akzeptiert. Man beachte, daß die Operationen Vereinigung und Durchschnitt bei diesem Automatentyp durch die Standard-Produktautomaten-Konstruktion erfolgen können, wobei im Falle des Durchschnitts die I-Diamant Eigenschaft aufgrund der verallgemeinerten Akzeptanzbedingung aufrechterhalten werden kann. Weiterhin sei angemerkt, daß mit Satz 3.1.1 gilt: Die von I-Diamant Automaten erkannten, abgeschlossenen Sprachen sind Urbilder deterministischer Sprachen. Mit den folgenden Sätzen erreichen wir auch die Umkehrung.

Zunächst vereinbaren wir einige Bezeichnungen. Für ∅ ≠ A, C ⊆ Σ seien folgende Mengen definiert:

IM_{A,C} = {t ∈ IM(Σ, D) | D(alph(t)) ⊆ D(A) ∧ (C ∩ D(A)) \ alph(t) ≠ ∅}, (mit der Konvention IM_{∅,C} = {1}), und Max(C) = {φ^{−1}(t) | t = ⊔_{n≥0}t_{n}, mit max(t_{n}) ⊆ C, für alle n ≥ 0} ⊆ Σ^{∞}.

Weiterhin sei Σ_{A}^{∞} = φ^{−1}(IR_{A}) und Inf_{⊆}(A) = {w ∈ Σ^{∞} | A ⊆ alphinf(w)}.

Satz 3.3.1 Seien L ⊆ IM(Σ, D), A, C ⊆ Σ so, daß max(t) = C, für alle t ∈ L. Dann gilt:

φ^{−1}(\overrightarrow{L} ∩ IR_{A}) = \overrightarrow{φ^{−1}(LIM_{A,C})} ∩ Max(C) ∩ Inf_{⊆}(C ∩ D(A)) ∩ Σ_{A}^{∞}.

Beweis: Die Inklusion von links nach rechts kann leicht nachgeprüft werden. Ohne Einschränkung sei A ≠ ∅. Sei p = ⊔_{n≥0}p_{n} mit p_{n} ∈ φ^{−1}(LIM_{A}), n ≥ 0. Es gelte p ∈ Max(C) ∩ Σ_{A}^{∞} mit C ∩ D(A) ⊆ alphinf(p). Mit p_{n} ∈ φ^{−1}(LIM_{A}) existieren Spurfolgen (t_{n})_{n≥0} ⊆ L, (w_{n})_{n≥0} ⊆ IM_{A,C} mit φ(p_{n}) = t_{n}w_{n}, d.h. φ(p) =: x = ⊔_{n≥0}t_{n}w_{n}. Sei ohne Einschränkung a ∈ (C ∩ D(A)) \ alph(w_{n}) für alle n ≥ 0. Mit Satz 2.1.11 existiert eine Darstellung von x mit geeigneten Folgen (s_{n})_{n≥0}, (u_{n})_{n≥0}, (v_{n})_{n≥0} ⊆ IM(Σ, D) so, daß gilt: alph(s_{n}) = A_{s} und alph(v_{n}) = A_{v} für n ≥ 1, bzw. alph(u_{n}) = A_{u} ⊆ A_{s}, für n ≥ 0 (vgl. Bem. 2.1.12); weiterhin gilt (A_{v} ∪ alph(v_{0})) × A_{s} ⊆ I und

t_{n} = s_{0}u_{0}s_{1} ⋯ s_{n} und w_{n} = u_{n} v_{0}v_{1} ⋯ v_{n}.

Man beachte zunächst, daß A_{s} ≠ ∅. Denn sonst folgt aus A_{s} = ∅ (damit auch A_{u} = ∅) zusammen mit a ∉ alph(w_{n}) ein Widerspruch zu a ∈ C ∩ D(A) ⊆ alphinf(x) = A_{v}. Nach Voraussetzung gilt auch p ∈ Max(C). Man beachte zunächst, daß A_{v} ×C ⊆ I gelten muß (falls A_{v} ≠ ∅). Ansonsten folgt aus b ∈ A_{v} ⊆ alphinf(x) und c ∈ C ∩ D(b) unmittelbar c ∈ C ∩D(A) ⊆ alphinf(x), und mit max(t_{n}) = C, auch c ∈ A_{s}. Dies widerspricht jedoch der Beziehung A_{s} × A_{v} ⊆ I. Die letzte Überlegung führt

nun zu x =^{p∈Max(C)} ⊔_{n≥0}∂_{C}(t_{n}w_{n}) = ∂_{C}(s_{0}u_{0}v_{0}s_{1}u_{1} ⋯ s_{n−1}u_{n−1}s_{n}), und damit auch

v_{n} = 1, für alle n ≥ 1. Wegen D(alphinf(x)) = D(A), zusammen mit (w_{n})_{n≥0} ⊆ IM_{A,C}, folgt auch v_{0} = 1 und damit die Aussage. □

Satz 3.3.2 Jede deterministische reelle Spursprache kann mit einem deterministischen I-Diamant Büchi Automaten mit verallgemeinerter Akzeptanz erkannt werden.

Beweis: Nach Satz 3.3.1 genügt es, einen verallgemeinerten Büchi Automaten mit den obigen Eigenschaften für Sprachen der Art Max(C), C ⊆ Σ, anzugeben. Wir betrachten den Automaten A = (Q = P(Σ), ·, ∅, F_{0}, F) mit folgender Übergangsfunktion:

A · a = (A ∩ I(a)) ∪ {a}.

Offensichtlich gilt für w ∈ Σ^{∗}: ∅ · w = max(φ(w)). Die Tafel F ⊆ P(Q) sei definiert wie folgt: F ∈ F genau dann, wenn für alle A ∈ F, a ∈ A Teilalphabete A = A_{0}, A_{1}, …, A_{k} und Buchstaben a_{i} ∈ A_{i}, 0 ≤ i ≤ k, derart existieren, daß gilt:

• A_{i} ∈ F, für alle 0 ≤ i ≤ k,

• (a_{i}, a_{i+1}) ∈ D, für alle 0 ≤ i ≤ k − 1,

• a_{0} = a und a_{k} ∈ C.

Die Endzustandsmenge sei definiert durch F_{0} = {A | A ⊆ C}. Mit der obigen Eigenschaft der Übergangsfunktion ist es nicht schwer zu sehen, daß L(A) = Max(C) gilt. □

Korollar 3.3.3 Die Familie {φ^{−1}(L) | L ∈ DRec(IR)} ist äquivalent zur Familie der Sprachen, die von deterministischen I-Diamant Büchi Automaten mit verallgemeinerter Akzeptanz erkannt werden.

Wir schließen dieses Kapitel mit einer weiteren Anmerkung zum Automatenmodell. Betrachte die deterministischen I-Diamant Büchi Automaten mit Tafel F ⊆ Q × P(Σ). Ein Wort w ∈ Σ^{ω} wird mit einem Tafelelement (f, A) akzeptiert, wenn f ∈ inf(w) unendlich oft wiederholt wird und D(alphinf(w)) = D(A) gilt. Wir zeigen, daß dies ein schwächeres Automatenmodell ist als das zuerst eingeführte.

Beispiel 3.3.4 Sei das Abhängigkeitsalphabet (Σ, D) = a −c b −d und die Wortsprache L_{a,b} = {w ∈ Σ^{ω} | |w|_{a} = |w|_{b} = ω} gegeben. Es gilt: L_{a,b} ist das Urbild einer deterministischen reellen Spursprache, aber kein deterministischer I-Diamant Büchi Automat A = (Q, δ, q_{0}, F) mit Tafel F ⊆ Q × P(Σ) erkennt L_{a,b}. Denn gäbe es einen solchen Automaten A, so würde eine abgeschlossene,

erkennbare Wortsprache L ⊆ Σ^{∗} mit L_{a,b} = \overrightarrow{L} ∩ Σ_{\{a,b\}}^{∞} existieren. Mit dem Theorem von Mezei [Ber79] läßt sich aber φ(L) ∈ Rec(IM) als endliche Vereinigung direkter Produkte K ×M mit K ∈ Rec({a, c}^{∗}), M ∈ Rec({b, d}^{∗}) schreiben. Damit läßt sich die abgeschlossene Sprache L = φ^{−1}φ(L) als endliche Vereinigung von φ^{−1}(KM) darstellen.

Nun betrachte das Wort u = a^{n}c^{n}b^{n}d^{n} und u^{ω} ∈ L_{a,b} = \overrightarrow{L} ∩ Σ_{\{a,b\}}^{∞}, für ein n ≥ 0. Ohne Einschränkung sei 0 ≤ q ≤ n so, daß u^{m}a^{n}c^{n}b^{n}d^{q} ∈ L für unendlich viele m ≥ 0 erfüllt ist (der Fall u^{m}a^{n}c^{n}b^{q} ∈ L verläuft analog). Mit der obigen Darstellung von L folgt für ein Paar von Sprachen K, M mit φ^{−1}(KM) ⊆ L und für eine unendliche Folge m_{1} < m_{2} < … aus IN: u_{a,c}^{m}a^{n}c^{n} ∈ K bzw. u_{b,d}^{m}b^{n}d^{q} ∈ M für m = m_{i} (u_{x,y} bezeichne die Projektion von u auf {x, y}^{∗}). Sei m_{0} fest und n genügend groß so, daß für ein geeignetes p ∈ IN gilt: u_{a,c}^{m_{0}}a^{n}c^{n+pIN} ⊆ K (beachte K erkennbar). Andererseits gilt u_{b,d}^{m_{i}}b^{n}d^{q} ∈ M für i ≥ 1. Mit φ^{−1}(KM) ⊆ L folgt abschließend

(u_{a,c}^{m_{0}}a^{n}c^{n})(c^{p}u_{b,d}^{m_{1}+1})(c^{p}u_{b,d}^{m_{2}−m_{1}}) … (c^{p}u_{b,d}^{m_{k}−m_{k−1}−1}b^{n}d^{q}) ∈ L,

und damit folgt z := (u_{a,c}^{m_{0}}a^{n}c^{n})(c^{p}u_{b,d}^{m_{1}+1})(c^{p}u_{b,d}^{m_{2}−m_{1}}) ⋯ (c^{p}u_{b,d}^{m_{k}−m_{k−1}}) … ∈ \overrightarrow{L}. Außerdem gilt z ∈ IR_{{b,c,d}} = IR_{{a,b}}, aber gleichzeitig z ∉ L_{a,b}.

Sternfreie und aperiodische reelle Spursprachen

Im Rahmen der Untersuchung erkennbarer Sprachen entsteht durch die Einschränkung auf rationale Ausdrücke, die keine Iteration enthalten dürfen und dafür die Komplement-Operation erlauben, eine besonders interessante Sprachfamilie. Die sternfreien Sprachen wurden auf vielfache Art charakterisiert, u.a. im Kontext des freien Monoids Σ^{∗} und der ω-Wortsprachen. Vom algebraischen Standpunkt aus ist Sternfreiheit äquivalent zu einer fundamentalen Varietät von Monoide, der aperiodischen (d.h. gruppenfreien) Monoide. Schützenberger’s bekanntes Theorem über die Äquivalenz von Sternfreiheit und Aperiodizität im freien Monoid [Sch65] ist eines der klassischen Ergebnisse der Varietätentheorie. Die Erweiterung zu ω-Wortsprachen ist ein Ergebnis von D. Perrin [Per]. Ein analoges Resultat wurde auch für freie, partiell kommutative Monoide erzielt [GRS91]. Eine weitere bedeutungsvolle Charakterisierung der Sternfreiheit entsteht im Rahmen der Logik, wenn sie auf die Logik 1. Stufe eingeschränkt wird. Während die monadische Logik 2. Stufe die gesamte Familie der erkennbaren reellen Spursprachen erfaßt, erweist sich die Einschränkung auf Logik 1. Stufe äquivalent zur Sternfreiheit [EM93]. Wir wollen in diesem Kapitel den Zusammenhang zwischen Sternfreiheit und Aperiodizität betrachten und verweisen auf die Charakterisierung im Rahmen der Logik in [Tho90b, TZ90, EM93]. Im folgenden bezeichnen wir mit SF(IM) die Familie der sternfreien Sprachen endlicher Spuren, d.h. SF(IM) ist die kleinste Familie von Sprachen aus IM(Σ, D), die die leere Menge ∅, sowie die einelementigen Mengen {a}, a ∈ Σ, enthält, und unter Konkatenation und Booleschen Operationen abgeschlossen ist [GRS91]. Analog definieren wir:

Definition 4.0.5 Die Familie der sternfreien reellen Spursprachen, SF(IR), ist die kleinste Familie F ⊆ P(IR(Σ, D)) mit den Eigenschaften:

1. SF(IM) ⊆ F.

2. Für alle L, K ∈ F mit L ⊆ IM(Σ, D) gilt LK ∈ F.

3. F ist abgeschlossen unter den Booleschen Operationen ∪, ∩ und dem Komplement ^{co} (wobei die Komplementierung bzgl. IR(Σ, D) durchgeführt wird).

Bemerkung 4.0.6 Man beachte, daß für L ∈ SF(IR), L ⊆ IM(Σ, D), das Komplement bzgl. IM(Σ, D) durch L^{co} ∩ IM(Σ, D) gegeben ist.

Ein Monoid S heißt aperiodisch, wenn es für ein n > 0 die Gleichung x^{n} = x^{n+1} erfüllt. Es ist leicht zu sehen, daß dies genau die Monoide charakterisiert, die nur triviale Untergruppen enthalten.

Definition 4.0.7 Eine reelle Spursprache L ∈ IR(Σ, D) heißt aperiodisch, wenn ein endliches, aperiodisches Monoid S und ein Homomorphismus η : IM(Σ, D) → S existieren so, daß L von η erkannt wird. Die Familie der aperiodischen reellen Spursprachen wird mit AP(IR) bezeichnet.

Bemerkung 4.0.8 Wir erhalten eine äquivalente Definition, wenn wir fordern, daß das syntaktische Monoid Synt(L) endlich und aperiodisch ist.

Zusätzlich zu den Notationen des Abschnitts 2.1 werden wir im folgenden für einen Homomorphismus η : Σ^{∗} → S zu einem (endlichen) Monoid S und für s ∈ S folgende Bezeichnungen verwenden:

X_{s} = η^{−1}(s), P_{s} = X_{s} \ X_{s}Σ^{+}.

Damit enthält P_{s} alle Wörter, die durch η auf s abgebildet werden, aber keinen echten Präfix mit dieser Eigenschaft besitzen. Weiterhin bezeichnen wir mit SF(Σ^{∞}) bzw. AP(Σ^{∞}) (analog SF(Σ^{∗}) bzw. AP(Σ^{∗})) die Familie der sternfreien bzw. aperiodischen Sprachen (un)endlicher Wörter (bzw. endlicher Wörter) . Für den folgenden Satz setzen wir voraus, daß für jeden Homomorphismus η : IM(Σ, D) → S gilt: mit η(t) = η(t′) folgt alph(t) = alph(t′), für alle t, t′ (siehe Abschnitt 2.1; beachte auch, daß die Aperiodizität des Monoids erhalten bleibt).

Theorem 4.0.9 Sei L ∈ Rec(IR) eine erkennbare reelle Spursprache. Folgende Aussagen sind äquivalent:

1. L ∈ SF(IR).

2. L ∈ AP(IR).

3. Synt(L) ist aperiodisch.

4. L läßt sich als endliche Vereinigung von Sprachen KN^{ω} darstellen, wobei K, N^{∗} ∈ SF(IM).

5. L ist eine Boolesche Kombination von Sprachen der Form \overrightarrow{K} ∩ IR_{A}, wobei K ∈ SF(IM) und A ⊆ Σ.

Beweis: Die Äquivalenz von 2. und 3. ist eine Konsequenz der Eigenschaft der syntaktischen Kongruenz einer Sprache L ⊆ Rec(IR), die gröbste Kongruenz zu sein, die L saturiert [Gas91]. 2 ⇒ 4: Diese Implikation folgt unmittelbar aus der bekannten Darstellung einer erkennbaren reellen Spursprache als endliche Vereinigung von Sprachen der Art IM_{s}IM_{e}^{ω}, zusammen mit der Äquivalenz zwischen AP(IM) und SF(IM). 5 ⇒ 1: Sei η : IM(Σ, D) → S ein Homomorphismus zu einem endlichen, aperiodi-

schen Monoid S, der K ∈ SF(IM) erkennt. Das Komplement von \overrightarrow{K} kann nun folgendermaßen dargestellt werden (vgl. [Per]):

\overrightarrow{K}^{co} = ⋃_{x∈S} (IM_{x} ( ⋃_{y mit xy∈η(K)}IM_{y} IR(Σ, D))^{co}) ,

da t ∈ IR(Σ, D) \ \overrightarrow{K} genau dann gilt, wenn ein endliches Präfix u ≤ t von t derart existiert, daß für alle uu′ ≤ t mit u′ ∈ IM(Σ, D) folgt: uu′ ∉ K. Mit SF(IM) = AP(IM) folgt anschließend die Behauptung. 1 ⇒ 2: Für diese Implikation genügt es zu zeigen, daß aus L ∈ SF(IR) die Sternfreiheit von φ^{−1}(L) ⊆ Σ^{∞} folgt. Die Begründung liegt in der Äquivalenz SF(Σ^{∞}) = AP(Σ^{∞}), zusammen mit der Tatsache, daß L und φ^{−1}(L) dasselbe syntaktische Monoid besitzen. Im folgenden führen wir Induktion über den sternfreien Ausdruck, der L darstellt. Sei zunächst L ∈ SF(IM). Mit SF(IM) = AP(IM) folgt direkt φ^{−1}(L) ∈ SF(Σ^{∗}) = AP(Σ^{∗}). Sei nun L = L_{1} ∪ L_{2} (bzw. L = L_{1} ∩ L_{2}, bzw. L = L_{1}^{co}), mit φ^{−1}(L_{i}) ∈ SF(Σ^{∞}), i = 1, 2. Damit folgt ebenfalls φ^{−1}(L) ∈ SF(Σ^{∞}), aufgrund der Vertauschbarkeit von φ^{−1} mit den Booleschen Operationen. Schließlich sei L = L_{1}L_{2}. Im folgenden bezeichnen wir L′_{1} = φ^{−1}(L_{1}) ∈ SF(Σ^{∗}), bzw. L′_{2} = φ^{−1}(L_{2}) ∈ SF(Σ^{∞}). Weiterhin sei _{D} die D-Shuffle Operation, die für K_{1}, K_{2} ⊆ Σ^{∞} definiert ist durch

K_{1} _{D} K_{2} = { u_{0}v_{0}u_{1}v_{1} … | u_{n}, v_{n} ∈ Σ^{∗}, u_{0}u_{1} … ∈ K_{1}, v_{0}v_{1} … ∈ K_{2}
und alph(v_{n}) × alph(u_{m}) ⊆ I, für n < m }

Insbesondere gilt hier wegen L′_{1} ⊆ Σ^{∗}:

L′_{1} _{D} L′_{2} = { u_{0}v_{0} … u_{n}v_{n}w | u_{k}, v_{k} ∈ Σ^{∗}, w ∈ Σ^{∞}, u_{0}u_{1} … u_{n} ∈ L′_{1}, v_{0}v_{1} … v_{n}w ∈ L′_{2} und alph(v_{i}) × alph(u_{k}) ⊆ I, für i < k ≤ n } .

Es sei nun für i = 1, 2, η_{i} : Σ^{∗} → S_{i} ein Homomorphismus, der L′_{i} erkennt. Aufgrund der Äquivalenz SF(Σ^{∞}) = AP(Σ^{∞}) können wir voraussetzen, daß S_{1}, S_{2} aperiodische Monoide sind. Wir bezeichnen im folgenden mit P ⊆ S_{2}×S_{2} die Menge P = { (s_{2}, e_{2}) ∈ S_{2}×S_{2} | s_{2}e_{2} = s_{2}, e_{2}^{2} = e_{2}, X_{s_{2}}X_{e_{2}}^{ω} ∩ L′_{2} ≠ ∅ }. Ohne Einschränkung sei X_{1} = η_{2}^{−1}(1) = {1}, wobei mit 1 die Identität in S_{2} (bzw. das leere Wort) bezeichnet wird. Wegen X_{1}^{ω} = {1} kann L′_{2} ⊆ Σ^{∞} dargestellt werden als L′_{2} = ⋃_{(s_{2},e_{2})∈P} X_{s_{2}}X_{e_{2}}^{ω}. Für L′_{1} gilt natürlich L′_{1} = η_{1}^{−1}η_{1}(L′_{1}). Offensichtlich kann nun die Wortsprache φ^{−1}(L) = L′_{1} _{D} L′_{2} dargestellt werden als

L′_{1} _{D} L′_{2} = ⋃_{s_{1}∈η_{1}(L′_{1})} ⋃_{(s_{2},e_{2})∈P} (X_{s_{1}} _{D} X_{s_{2}})X_{e_{2}}^{ω} .

Die Wortsprachen L′_{i}, i = 1, 2, sind aber abgeschlossen, d.h. es gilt φ^{−1}φ(L′_{i}) = L′_{i}. Damit sind für s_{i} ∈ S_{i}, i = 1, 2, X_{s_{1}} bzw. X_{s_{2}} ebenfalls abgeschlossen. Aus [GRS91] folgt unmittelbar die Sternfreiheit des D-Shuffle zweier sternfreien, abgeschlossenen Wortsprachen, und damit gilt X_{s_{1}} _{D} X_{s_{2}} ∈ SF(Σ^{∗}). Weiterhin ist

e_{2} ∈ S_{2} idempotent, und es läßt sich zeigen, daß X_{e_{2}}^{ω} = \overrightarrow{X_{e_{2}}IP_{e_{2}}} ∈ SF(Σ^{∞}) ebenfalls sternfrei ist [Per]. Zusammen mit der obigen Darstellung für φ^{−1}(L) folgt die Behauptung. 4 ⇒ 1: Es genügt zu zeigen, daß N^{ω} sternfrei ist, wobei ohne Einschränkung N = N^{∗} ∈ SF(IM) gilt. Sei S ein endliches, aperiodisches Monoid und η : IM(Σ, D) → S ein Homomorphismus, der N erkennt. Für s ∈ S bezeichnen wir mit N_{s} ⊆ N die Teilmenge N ∩ η^{−1}(s). Wir können nun wegen N^{ω} = ⋃_{(s,e)∈P} N_{s}N_{e}^{ω} mit P = {(s, e) ∈ η(N)^{2} | se = s, e ∈ E(S)} uns auf N_{e}^{ω} mit idempotenten e ∈ E(S) einschränken. Für A ⊆ Σ sei N′_{e,A} = (N_{e} \ N_{e}IM_{+}) ∩ {t ∈ IM(Σ, D) | D(alph(t)) ⊆ D(A)} die Untermenge von N_{e}, deren Elemente t keinen echten Präfix in N_{e} besitzen und für die D(alph(t)) ⊆ D(A) gilt. Mit der Implikation 5 ⇒ 1 (zusammen mit IR_{A} ∈ SF(IR)) genügt es zu zeigen:

N_{e}^{ω} = ⋃_{A⊆Σ}(\overrightarrow{N_{e}N′_{e,A}} ∩ IR_{A}).

Die Inklusion der linken in der rechten Seite ist leicht zu sehen. Für die umgekehrte Inklusion können wir mit zwei Folgen (t_{n})_{n≥0} ⊆ N_{e} bzw. (w_{n})_{n≥0} ⊆ N′_{e,A} und x := ⨆{ t_{n}w_{n} | n ≥ 0 } Korollar 2.1.14 anwenden. Damit existieren Spurfolgen (s_{n})_{n≥0}, (u_{n})_{n≥0} ⊆ IM(Σ, D) mit:

t_{n} = s_{0}u_{0} ⋯ s_{n−1}u_{n−1}s_{n} und w_{n} = u_{n} ,

(eventuell unter Verwendung einer Unterfolge von Indizes). Mit der üblichen Zusammenfassung von Faktoren findet man eine Indexfolge (n_{i})_{i≥0} so, daß für geeignete s ∈ S, f ∈ E(S) mit sf = s gilt: η(s_{0}u_{0} ⋯ s_{n_{0}}) = s und η(u_{n_{i}}s_{n_{i}+1} ⋯ s_{n_{i+1}}) = f, für alle i ≥ 0. Es folgt s = e, daher auch ef = e. Andererseits gilt f = η(u_{n})x = ex für ein x ∈ S, damit auch ef = f (wegen e ∈ E(S)) und schließlich folgen e = f und x ∈ N_{e}^{ω}. 2 ⇒ 5: Folgt direkt mit Theorem 2.2.3, zusammen mit der Äquivalenz zwischen Sternfreiheit und Aperiodizität in IM(Σ, D). □

48

Komplementierung asynchroner Büchi Automaten

Die Komplementierung nichtdeterministischer Büchi Automaten für ω-Wortspra-chen markierte in den 60’er Jahren den Anfangspunkt der Untersuchung von Erkennbarkeit im Kontext unendlicher Wörter [Büc60]. Ursprünglich für die Entscheidbarkeit der monadischen Logik zweiter Stufe mit Nachfolgerelation benötigt, erwies sich eine effiziente Komplementierung für Büchi Automaten als grundlegend in verschiedenen Theorien temporaler Logik. Von den existierenden Lösungen des Komplementierungsproblems für Wortautomaten haben wir die elegante Methode des Fortschrittsmaßes von N. Klarlund [Kla91] ausgewählt, um asynchron-zelluläre Büchi Automaten zu komplementieren. Der Ausgangspunkt dieser Konstruktion ist ein klassischer Potenzautomat, wodurch bei asynchron-zellulären Automaten die erste Schwierigkeit auftritt. Das Problem der Determinisierung für asynchron (zelluläre) Automaten war lange Zeit offen. Etwa zur selben Zeit, zu der die vorliegende Arbeit entstand, ist eine weitere Potenzautomaten-Konstruktion für asynchrone Automaten durch Klarlund et. al. entstanden [KMS94]. Die Ergebnisse dieses Kapitels erscheinen in [Mus94]. Im folgenden Abschnitt stellen wir eine Determinisierungs-Konstruktion für asynchron-zelluläre Automaten vor, die auf dem Begriff der asynchronen Abbildung von Zielonka (vergleiche Abschnitt 1.2) beruht.

5.1 Determinisierung asynchron-zellulärer Automaten

Ein wesentlicher Aspekt in der Konstruktion von Zielonka für asynchron-zelluläre Automaten ist durch eine zeitliche Markierung mit beschränktem Wertebereich gegeben. Diese erlaubt, die Aktualität von indirekt übertragener Information festzustellen, indem z.B. für zwei Prozesse a, b bestimmt wird, welcher von den beiden das letzte Vorkommen des Prozesses c “gesehen” hat. Im folgenden werden wir für A, B ⊆ Σ mit ∂_{A,B}(t) den Präfix ∂_{A}(∂_{B}(t)) von t ∈ IM(Σ, D) bezeichnen, sowie statt ∂_{{a}}(t), direkt ∂_{a}(t) schreiben. Die Abbildung ν : IM(Σ, D) → {0, …, |Σ|}^{Σ×Σ}, die die Zeitmarkierung realisiert, ist nun induktiv definiert:

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

• Für t ≠ ∂_{a,b}(t) sei ν(t)(a, b) = ν(∂_{a,b}(t))(a, a).

• Für t = ∂_{a}(t) mit t ≠ 1 sei

ν(t)(a, a) = min{n > 0 | n ≠ ν(t)(a, c) für alle c ≠ a} .

Der Wert ν(t) der Zeitmarkierung für eine Spur t ∈ IM(Σ, D) stellt grundlegende Informationen über Ordnungs-Beziehungen zwischen Präfixen ∂_{a}(t) von t, a ∈ Σ, bereit. Genauer gilt für t ∈ IM(Σ, D), a, b, c ∈ Σ:

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

Beachte weiterhin die leicht überprüfbare Beziehung ν(∂_{A}(t))(c, a) = ν(t)(c, a) für a ∈ A. Es seien nun t ∈ IM(Σ, D), A, B ⊆ Σ gegeben. Weiterhin seien die Mengen C_{a,b} = {c ∈ Σ | ∂_{c,a}(t) = ∂_{c,b}(t)} für alle a, b ∈ A ∪ B bekannt (beispielsweise durch den Wert ν(t), oder alternativ, über die Werte ν(∂_{A}(t)), ν(∂_{B}(t))). Damit kann für jedes c ∈ Σ bestimmt werden, welcher der drei verschiedenen Fälle vorliegt: ∂_{c,A}(t) = ∂_{c,B}(t), ∂_{c,A}(t) < ∂_{c,B}(t) oder ∂_{c,B}(t) < ∂_{c,A}(t).

Faktum 5.1.1 ([CMZ93, Die90]) Die Abbildung ν ist asynchron.

Für die Determinisierung von nichtdeterministischen asynchron-zellulären Automaten nehmen wir die Zeitmarkierung ν als Basis und erweitern sie durch eine Abbildung ρ, die alle Abläufe des gegebenen asynchron-zellulären Automaten A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F) beschreibt. Im folgenden werden wir die Menge der globalen Zustände dea Automaten A, ∏_{a∈Σ} Q_{a}, mit Q bezeichnen. Weiterhin bezeichnen wir mit R_{A}(t), t ∈ IM(Σ, D), die Menge der Abläufe des Automaten A auf der Spur t, die im Startzustand q_{0} beginnen. Ein Ablauf r ∈ R_{A}(t) im Automaten A wird dabei als Abbildung r : V_{t} → ˙⋃_{a∈Σ} Q_{a} angesehen, d.h. als Beschriftung des Abhängigkeitsgraphen [V_{t}, E_{t}, λ_{t}] von t mit lokalen Zuständen so, daß r sowohl mit der alphabetischen Beschriftung λ_{t} als auch mit den lokalen Übergangsrelationen (δ_{a})_{a∈Σ} konsistent ist. Genauer, sei (a, n_{a}) ∈ V_{t} ein Knoten und betrachte die Ablaufbeschriftung q_{b} = r(b, n_{b}), wobei (b, n_{b}) der letzte mit b beschriftete Knoten vor (a, n_{a}) ist, falls ein solcher existiert. Ansonsten sei q_{b} = (q_{0})_{b} festgelegt. Dann wird gefordert, daß die Abbildung r die Beziehung r(a, n_{a}) ∈ δ_{a}((q_{b})_{b∈D(a)}) erfüllt. Weiterhin bezeichnen wir für u ∈ IM(Σ, D) und einen Ablauf r ∈ R_{A}(u) mit δ(r, u) ∈ Q den globalen Zustand, der im Ablauf r auf der Spur u erreicht wird. Sei nun ρ : IM(Σ, D) → P(Q^{Σ}) definiert für t ∈ IM(Σ, D) durch

ρ(t) = {f ∈ Q^{Σ} | ∃r ∈ R_{A}(t) so, daß f(a) = δ(r, ∂_{a}(t)), ∀ a ∈ Σ} .

Damit entspricht jedes Element f von ρ(t) einem Ablauf r auf t so, daß für alle a, b ∈ Σ gilt: f(a)_{b} ist der lokale b-Zustand, der im Ablauf r auf dem Präfix ∂_{b,a}(t) von t erreicht wird. Der folgende Satz legt die Basis des Potenzautomaten des Automaten A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F).

Satz 5.1.2 Die Abbildung (ν, ρ) ist asynchron. Zusätzlich gilt:

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

Beweis: Durch Faktum 5.1.1 ist bereits bekannt, daß die erste Komponente der obigen Abbildung (ν) asynchron ist. Es seien nun t ∈ IM(Σ, D), a ∈ Σ, A, B ⊆ Σ. Angenommen, der Wert ρ(∂_{D(a)}(t)) und der Buchstabe a sind gegeben, so definieren wir R ⊆ Q^{Σ} durch g ∈ R genau dann, wenn für ein f ∈ ρ(∂_{D(a)}(t)) gilt:

• g(b) = f(b), für b ≠ a;

• g(a) = q′ = (q_{x}′)_{x∈Σ}, wobei

1. q_{x}′ = f(c)_{x} für x ≠ a, mit c ∈ D(a) so, daß ∂_{x,b}(t) ≤ ∂_{x,c}(t) für alle b ∈ D(a) (d.h., es gilt ∂_{x,c}(t) = ∂_{x,D(a)}(t));

2. q_{a}′ ∈ δ_{a}((f(b)_{b})_{b∈D(a)}).

Für jedes Paar f, g wie oben, mit q = f(a) und q′ = g(a), werden wir im nächsten Abschnitt die Bezeichnung q →^{(a)} q′ verwenden. Dies bedeutet, daß für einen Ablauf r ∈ R_{A}(∂_{a}(ta)) von A auf dem Präfix ∂_{a}(ta) gilt: q = δ(r, ∂_{a}(t)) und q′ = δ(r, ∂_{a}(ta)). Es ist leicht zu sehen, daß R = ρ(∂_{a}(ta)) gilt, da Abläufe auf ∂_{a}(ta) genau durch Erweiterung von Abläufen auf dem Präfix ∂_{D(a)}(t) mittels einem a-Übergang entstehen. Man beachte weiterhin, daß die obige Bedingung mit der Beziehung ν(t)(x, b) = ν(∂_{D(a)}(t))(x, b), für alle b ∈ D(a), überprüft werden kann (siehe auch die Bemerkung vor Faktum 5.1.1). Wir betrachten nun A, B ⊆ Σ, t_{1} = ∂_{A}(t), t_{2} = ∂_{B}(t), s = t_{1} ⊓ t_{2} mit t_{1} = su und t_{2} = sv, wobei alph(u) × alph(v) ⊆ I gilt. Weiterhin bezeichnen wir mit C die Menge

C = {c ∈ Σ | ∂_{c}(t_{1}) = ∂_{c}(t_{2})}.

Angenommen, die Werte ρ(t_{1}), ρ(t_{2}) sind gegeben. Dann definieren wir R ⊆ Q^{Σ} durch f ∈ R genau dann, wenn für gewisse f_{i} ∈ ρ(t_{i}) (i = 1, 2), die die Beziehung f_{1}(c) = f_{2}(c) für alle c ∈ C erfüllen, gilt (a, b ∈ Σ):

f(a)_{b} = \{ \begin{matrix}f_{1}(a)_{b} & falls ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1}) \\ f_{2}(a)_{b} & falls ∂_{b,C}(t_{2}) < ∂_{b,a}(t_{2}) \\ f_{1}(d)_{b} & sonst, für ein d mit ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}). \end{matrix}

Wir werden anschließend zeigen, daß f auch im letzten Fall der obigen Festlegung wohldefiniert ist. Zunächst sei die Bedeutung der Definition erklärt. Die Grundidee besteht darin, daß Abläufe des Automaten auf den Spuren t_{1} bzw. t_{2} miteinander kombinierbar sind, falls sie denselben globalen Zustand auf dem gemeinsamen Präfix s = t_{1} ⊓ t_{2} erreichen. Mit der Beziehung ∂_{C}(t_{1}) = ∂_{C}(t_{2}) = ∂_{C}(s) = s (vgl. [CMZ93, Die90]) gilt für zwei Abläufe r_{i} ∈ R_{A}(t_{i}) und dazugehörige Abbildungen f_{i} mit f_{i}(a) = δ(r_{i}, ∂_{a}(t_{i})), a ∈ Σ:

f_{1}(c) = f_{2}(c), ∀c ∈ C ⟹ δ(r_{1}, s) = δ(r_{2}, s)

(Man beachte, daß mit max(s) ⊆ C auch ∂_{a}(s) = ∂_{a,c}(s) = ∂_{a,c}(t_{i}) für ein geeignetes c ∈ C, i = 1, 2 gilt.) Damit ist die Abbildung r, die die Knoten des Abhängigkeitsgraphen von t_{1} ⊔ t_{2} mit lokalen Zuständen gemäß dem Ablauf r_{1} auf dem Faktor su bzw. gemäß r_{2} auf dem Faktor v beschriftet, ein wohldefinierter Ablauf des Automaten A auf t_{1} ⊔ t_{2}. Die obige Abbildung f entspricht aber genau dem Ablauf r, da für alle a, b ∈ Σ gilt:

1. ∂_{b,a}(t) = ∂_{b,a}(t_{1}), falls ∂_{a}(t_{2}) ≤ ∂_{a}(t_{1});

2. ∂_{b,a}(t) = ∂_{b,a}(t_{2}), falls ∂_{b,C}(t_{2}) < ∂_{b,a}(t_{2}). Beachte, daß in diesem Fall gilt: ∂_{b,a}(t) ≰ s.

3. Schließlich seien ∂_{a}(t_{1}) < ∂_{a}(t_{2}) und ∂_{b,a}(t_{2}) ≤ ∂_{b,C}(t_{2}) erfüllt. Ohne Einschränkung sei ∂_{b,a}(t_{2}) ≠ 1 (ansonsten wähle d = a) und betrachte die Menge C′ = {d ∈ Σ | ∂_{d,a}(t_{2}) = ∂_{d,C}(t_{2}) (= ∂_{d}(s))}. Im folgenden bezeichnen wir mit s′ den gemeinsamen Präfix von s und ∂_{a}(t_{2}), d.h. es sei s′ = s ⊓ ∂_{a}(t_{2}), mit s = s′x bzw. ∂_{a}(t_{2}) = s′y für geeignete x, y ∈ IM(Σ, D), wobei alph(x) × alph(y) ⊆ I. Man beachte, daß max(s′) ⊆ C′. Aufgrund der Beziehung ∂_{b,a}(t_{2}) ≤ ∂_{b,C}(t_{2}) = ∂_{b}(s) gilt offensichtlich auch ∂_{b,a}(t_{2}) = ∂_{b}(s′) = ∂_{b,C′}(s), und damit auch s′ ≠ 1 bzw. C′ ≠ ∅. Es folgt ∂_{b,a}(t_{2}) = ∂_{b,d}(s′) = ∂_{b,d}(s) für ein geeignetes d ∈ max(s′) ⊆ C′. Es genügt zu zeigen, daß ∂_{d}(s) = ∂_{d}(t_{1}) gilt. Aufgrund der Definition von C′, s′, x, y folgt unmittelbar C′ ∩ alph(x) = ∅. Nehmen wir nun an, daß d ∈ alph(u) gilt. Wegen d ∈ max(s′) existiert auch ein e ∈ alph(y) (damit e ∈ alph(v)) mit (d, e) ∈ D (ansonsten würde ∂_{a}(t_{2}) ≤ s gelten). Damit wäre ein Widerspruch zu d ∈ alph(u) erreicht. Schließlich folgt daraus mit t_{1} = s′xu die Beziehung ∂_{d}(t_{1}) = ∂_{d}(s′) (= ∂_{d}(s)). Somit erhalten wir die gewünschte Gleichheit ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}).

Ein Buchstabe d mit 1 ≠ ∂_{b,a}(t_{2}) = ∂_{b,d}(t_{1}) wird nun konkret wie folgt berechnet: unter Verwendung von ν(t_{1}), ν(t_{2}) bestimmen wir zunächst C und das Alphabet von v, alph(v) [CMZ93]; unter erneuter Verwendung von ν(t_{2}) wird anschließend C′ berechnet. Schließlich wählen wir d ∈ C′∩D(alph(v)) so, daß ∂_{b,C}(t_{1}) ≤ ∂_{b,d}(t_{1}) (unter Verwendung von ν(t_{1})). Damit folgt:

∂_{b,d}(t_{1}) =^{d∉alph(u)} ∂_{b,d}(s) =^{d∈C′} ∂_{b,d,a}(t_{2}) ≤ ∂_{b,a}(t_{2}) ≤ ∂_{b,C}(t_{2}) = ∂_{b,C}(t_{1}) ≤ ∂_{b,d}(t_{1}).

□

Theorem 5.1.3 Gegeben sei ein nichtdeterministischer asynchron-zellulärer Automat A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F). Dann kann ein deterministischer asynchronzellulärer Automat Ã = ((Q̃_{a})_{a∈Σ}, (δ̃_{a})_{a∈Σ}, q̃_{0}, F̃) effektiv konstruiert werden so, daß L(A) = L(Ã). Der Automat Ã besitzt 2^{O(N^{|Σ|})} globale Zustände, wobei N die Anzahl der globalen Zustände von A ist.

Beweis: Folgt direkt aus Satz 5.1.2 zusammen mit Bemerkung 1.2.1. □

Abschließend sei an dieser Stelle angemerkt, daß die Konstruktion von Zielonka ebenfalls angewendet werden kann, wenn der gegebene asynchron-zelluläre Automat als Wortautomat angesehen wird und mittels einer gewöhnlichen Potenzautomaten-Konstruktion determinisiert wird. Unter Verwendung des minimalen Automaten kann anschließend eine Variante der Konstruktion von Zielonka [CMZ93] angewendet werden, wodurch ein einfach exponentieller Anstieg der Zustandsanzahl entsteht. Man beachte jedoch, daß in der hier vorgestellten Konstruktion nur erreichbare Zustände eingehen, im Gegensatz zum vorher beschriebenen Ansatz.

5.2 Komplementierung asynchron-zellulärer Büchi Automaten

Für die Komplement-Konstruktion für asynchron-zelluläre Büchi Automaten verwenden wir die Methode des Fortschrittsmaßes (progress measure), die von Klarlund [Kla91] eingesetzt wurde, um Büchi bzw. Streett Wortautomaten effizient zu komplementieren. Die Grundidee seiner Konstruktion besteht in der Berechnung eines Fortschrittsmaßes auf einem gerichteten, azyklischen (Berechnungs-) Graphen G = (V, E), dessen sämtliche Pfade darauf überprüft werden sollen, daß sie eine vorgegebene Bedingung stets nur endlich oft erfüllen. Das Fortschrittsmaß ist die lokale Zusicherung der global zu erfüllenden Bedingung, und die Existenz eines geeigneten Fortschrittsmaßes ist gleichbedeutend damit, daß jeder Pfad die vorgegebene Bedingung nur endlich oft bestätigt. Intuitiv quantifiziert das Fortschrittsmaß eines Knotens v ∈ V, wieweit dieser Knoten davon entfernt ist, daß alle von ihm ausgehenden Pfade die obige Eigenschaft besitzen. Unser Ausgangspunkt ist ein asynchron-zellulärer Automat A mit einer leicht modifizierten Büchi Akzeptanz-Bedingung. Diese gibt für jeden Buchstaben höchstens einen lokalen Zustand vor, der unendlich oft wiederholt werden muß. Zusätzlich spezifiziert die Akzeptanzbedingung das Alphabet, das unendlich oft wiederholt wird, d.h. die Menge alphinf(t). Formal gesehen werden wir einen Automaten A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, T ) mit T ⊆ Q × P(Σ) × P(Σ) betrachten (wobei Q = ∏_{a∈Σ} Q_{a} die Menge der globalen Zustände in A bezeichnet). Im folgenden sei A = ˙⋃_{i=1}^{k} A_{i} die Zerlegung von A in Zusammenhangskomponenten (d.h. jedes A_{i} ist als Abhängigkeitsgraph zusammenhängend, und es gilt A_{i} ×A_{j} ⊆ I für alle i ≠ j). Ein Element der Tafel T wird ein Tripel (q^{f}, A, {a_{1}, …, a_{k}}) sein, mit der Einschränkung a_{i} ∈ A_{i}, für alle 1 ≤ i ≤ k. Im folgenden verwenden wir die Bezeichnung R_{A}(t) für die Menge der Abläufe von A auf einer reellen Spur t ∈ IR(Σ, D) (durch Erweiterung der im vorigen Abschnitt angegebenen Definition eines Ablaufs). Ein Ablauf r ∈ R_{A}(t) wird mit dem Tafelelement (q^{f}, A, {a_{1}, …, a_{k}}) akzeptieren, wenn A = alphinf(t) erfüllt ist und jeder lokale Zustand q_{a}^{f} mit a ∈ Ā ∪ {a_{1}, …, a_{k}} unendlich oft wiederholt wird (bzw. einen Haltezustand darstellt), d.h.,

• A = alphinf(t) und

• Für alle a ∈ Ā ∪ {a_{1}, …, a_{k}} gilt q_{a}^{f} ∈ inf_{a}(r) mit

inf_{a}(r) := {q_{a} ∈ Q_{a} | ∀n < |t|_{a} ∃n ≤ m < |t|_{a} : r(a, m) = q_{a}}.

Man beachte, daß der Übergang von der klassischen Büchi Bedingung mit Tafel T ⊆ ∏_{a∈Σ} P(Q_{a}) zur obigen Bedingung einfach durch Verwendung der Buchstaben a_{i} (1 ≤ i ≤ k) geschieht, indem die Information über die durchlaufenen Zustände ⋃_{a∈A_{i}} T_{a} (wobei T = (T_{a})_{a∈Σ} ∈ T ) durch a_{i} gesammelt wird. Die umgekehrte Transformation ist trivial, da lediglich die Menge der Buchstaben, die unendlich oft auftreten, zusätzlich (nichtdeterministisch) überprüft werden muß. Für t ∈ IR(Σ, D), a ∈ Σ, 0 ≤ n < |t|_{a}, sei t[a, n] = ⊓{u ≤ t | |u|_{a} = n + 1} der kleinste Präfix von t, der die ersten n + 1 Vorkommen des Buchstaben a enthält (beachte max(t[a, n]) = {a}). Weiterhin sei

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

die Menge der globalen Zustände, die auf den Präfixen t[a, n] erreicht werden kann. Insbesondere für a = a_{i}, 1 ≤ i ≤ k, verwenden wir die Abkürzung U_{i}(t) für U_{a_{i}}(t). Für alle n + 1 < |t|_{a}, q, q′ ∈ U_{a}(t) mit q′ ∈ δ(q, t[a, n]^{−1} t[a, n + 1]) verwenden wir im folgenden die Notation (q, n) →^{a,t} (q′, n + 1). Schließlich werden wir durchgehend den Begriff eines Berechnungs(unter)graphen für (einen Untergraph von) (U_{a}(t), →^{a,t}) verwenden. Der nächste Satz legt die Grundlage des Komplement-Automaten von A. Es seien N := |Q| und F_{i} := {q ∈ Q | q_{a_{i}} = q_{a_{i}}^{f}}, wobei q^{f} = (q_{a}^{f})_{a∈Σ} die erste Komponente des einzigen Elements der Tafel T von A sein wird.

Satz 5.2.1 Sei A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, {(q^{f}, A, {a_{1}, …, a_{k}})}) ein asynchronzellulärer Büchi Automat mit q^{f} ∈ Q, A ⊆ Σ, a_{i} ∈ A_{i} für 1 ≤ i ≤ k. Sei t ∈ IR(Σ, D) mit alphinf(t) = A. Dann gilt t ∉ L(A) genau dann, wenn eine Familie von Berechnungs-Untergraphen (G_{i}(t))_{1≤i≤k} mit G_{i}(t) = (V_{i}(t), E_{i}(t)), und Abbildungen (Φ_{i})_{1≤i≤k}, Φ_{i} : U_{i}(t) → {0, 1, …, 2N + 1} derart existieren, daß folgende Bedingungen für alle 1 ≤ i ≤ k erfüllt sind:

1. • V_{i}(t) = {(q, n) ∈ U_{i}(t) | Φ_{i}(q, n) ≠ 2N + 1},

• E_{i}(t) ⊆ {((q, n), (q′, n + 1)) ∈ V_{i}(t)^{2} | (q, n) →^{a_{i},t} (q′, n + 1)},

• Für alle (q, n) →^{a_{i},t} (q′, n + 1) mit (q, n) ∈ V_{i}(t) gilt auch (q′, n + 1) ∈ V_{i}(t).

2. Jede Abbildung Φ_{i} : U_{i}(t) → {0, 1, …, 2N + 1} erfüllt dabei folgende Bedingungen, wobei (q, n), (q′, n + 1) ∈ U_{i}(t):

(i) Φ_{i} ist schwach monoton fallend bzgl. der Übergangsrelation →^{a_{i},t}:

(q, n) →^{a_{i},t} (q′, n + 1) ⟹ Φ_{i}(q, n) ≥ Φ_{i}(q′, n + 1)

(ii) Für (q, n) →^{a_{i},t} (q′, n+1) mit Φ_{i}(q, n) = Φ_{i}(q′, n+1) gilt entweder q′ ∉ F_{i} oder Φ_{i}(q, n) ∈ {0, 2, …, 2N} ∪ {2N + 1}.

(iii) Sei (q_{n}, n)_{n≥0} ⊆ V_{i}(t) eine unendliche Folge so, daß (q_{n}, n) →^{a_{i},t} (q_{n+1}, n+ 1), n ≥ 0. Dann gilt

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

3. Es existiert ein endliches Präfix t_{0} ≤ t von t, t_{0} ∈ IM(Σ, D), mit |t_{0}|_{a} = |t|_{a} für alle a ∉ A so, daß jeder Ablauf r ∈ R_{A}(t_{0}) eine der beiden Bedingungen erfüllt:

• Entweder gilt δ(r, t_{0})_{a} ≠ q_{a}^{f} für ein a ∈ Ā,

• oder es gilt (δ(r, ∂_{a_{i}}(t_{0})), |t_{0}|_{a_{i}} − 1) ∈ V_{i}(t) für ein 1 ≤ i ≤ k.

Bemerkung 5.2.2 Jede Abbildung Φ_{i} ist im Sinne von Klarlund ein Pseudo-Fortschrittsmaß, das bezüglich dem Wertebereich {0, 2, …, 2N} nicht stationär ist (vgl. [Kla91]). Der Wert des Fortschrittsmaßes für einen Knoten v gibt an, wieweit die in v startenden Berechnungspfade davon entfernt sind, die entsprechende Komponente des Endzustands q^{f} nur endlich oft zu wiederholen.

Bedingung (3) des Satzes ist eine Zusicherung dafür, daß die nicht in den Berechnungs-Untergraphen G_{i}(t), 1 ≤ i ≤ k, erfaßten Zustände nicht zu einem Ablauf r ∈ R_{A}(t) synchronisierbar sind. Dies bedeutet, daß jeder Ablauf r auf t entweder wegen inf_{a}(r) ≠ {q_{a}^{f}} für ein a ∉ alphinf(t) ablehnt, oder aber wegen der Existenz eines Indizes n_{i}, 1 ≤ i ≤ k, mit (δ(r, t[a_{i}, n_{i}]), n_{i}) ∈ V_{i}(t) (damit auch (δ(r, t[a_{i}, n]), n) ∈ V_{i}(t) für alle n ≥ n_{i}).

Beweis von 5.2.1: Angenommen, es existieren Berechnungsuntergraphen G_{i}(t), G_{i}(t) = (V_{i}(t), E_{i}(t)), und zugehörige Abbildungen (Φ_{i}), 1 ≤ i ≤ k so, daß die Voraussetzungen des Satzes erfüllt sind. Sei r ∈ R_{A}(t) ein A-Ablauf auf t. Mit Bemerkung 5.2.2 genügt es den Fall zu betrachten, in dem für geeignete 1 ≤ i ≤ k und n_{i} ∈ IN gilt: (δ(r, t[a_{i}, n]), n) ∈ V_{i}(t) für alle n ≥ n_{i}. Sei im folgenden q_{n} := δ(r, t[a_{i}, n]) für n ≥ n_{i}. Mit der Monotonie der Abbildung Φ_{i} können wir annehmen, daß Φ_{i}(q_{n}, n) = Φ_{i}(q_{n_{i}}, n_{i}) für alle n ≥ n_{i} gilt. Weiterhin folgt mit (2iii): Φ_{i}(q_{n_{i}}, n_{i}) ∉ {0, 2, …, 2N} ∪ {2N + 1}, und somit erfolgt über Bedingung (2ii) q_{n} ∉ F_{i} für alle n ≥ n_{i}. Damit haben wir gezeigt, daß kein Ablauf von A auf t akzeptierend ist. Für die Rückrichtung sei t ∉ L(A) mit alphinf(t) = A. Sei ω_{1} die Menge der abzählbaren Ordinalzahlen. Wir folgen dem Ansatz von Klarlund [Kla91] und definieren zunächst Fortschrittsmaße Φ̃_{i} mit Wertebereich ω_{1}. Im folgenden verwenden wir für (q, n) ∈ U_{i}(t) die Bezeichnung N_{+}(q, n) für die Menge der echten Nachfolger von (q, n) in (U_{i}(t) \ V_{i}(t), →^{a_{i},t}), d.h.,

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

wobei (q_{k}, k) →^{a_{i},t} (q_{k+1}, k + 1), ∀n ≤ k < m} .

Der Berechnungs-Untergraph G_{i}(t) = (V_{i}(t), E_{i}(t)) wird nun zusammen mit der Abbildung Φ̃_{i} : U_{i}(t) → ω_{1} mittels transfiniter Induktion definiert. Sei V_{0} = V_{i}(t) = ∅. Nehmen wir an, die Sequenz (V_{α})_{α<β} sei für α < β < ω_{1} bereits definiert, wobei die Knotenmengen V_{α} ⊆ U_{i}(t) paarweise disjunkt sind und V_{i}(t) = ∪_{α<β}V_{α} gilt. Gilt für alle (q, n) ∈ U_{i}(t) \ V_{i}(t): N_{+}(q, n) ∩ F_{i} × IN ≠ ∅, so setzen wir V_{β} := U_{i}(t) \ V_{i}(t) und V_{γ} = ∅ für alle β < γ < ω_{1}. Ansonsten wählen wir ein (q, n) ∈ U_{i}(t) \ V_{i}(t) mit N_{+}(q, n) ∩ F_{i} × IN = ∅. Sei nun V_{β} definiert durch

V_{β} := \{ \begin{matrix}\{(q, n)\} & falls N_{+}(q, n) = ∅ \\ N_{+}(q, n) & sonst, \end{matrix}

und setze abschließend V_{i}(t) = V_{i}(t) ∪ V_{β}. Damit kann Φ̃_{i} : U_{i}(t) → ω_{1} definiert werden durch Φ̃_{i}(q, n) := β genau dann, wenn (q, n) ∈ V_{β} gilt (beachte, daß die Mengen V_{α}, α < ω_{1}, paarweise disjunkt sind). Das somit definierte Fortschrittsmaß Φ̃_{i} ist offensichtlich schwach monoton fallend bezüglich der Übergangsrelation →^{a_{i},t}. Gilt für (q, n), (q′, n+1) ∈ U_{i}(t) mit (q, n) →^{a_{i},t} (q′, n + 1) und Φ̃_{i}(q, n) = Φ̃_{i}(q′, n + 1), so folgt unmittelbar aus der Konstruktion:

q′ ∉ F_{i}.  (5.1)

Aus der Konstruktion folgt außerdem die Existenz einer Ordinalzahl β_{0} < ω_{1} mit U_{i}(t) \ V_{i}(t) = V_{β_{0}} so, daß β_{0} = ⊔{α < ω_{1} | V_{α} ≠ ∅}. Es gilt nun entweder V_{β_{0}} = ∅ oder zu jedem (q_{n}, n) ∈ V_{β_{0}} existiert ein unendlicher Pfad in V_{β_{0}}, (q_{n}, n) →^{a_{i},t} (q_{n+1}, n + 1) →^{a_{i},t} ⋯, der einen Zustand aus F_{i} unendlich oft wiederholt:

|{m ≥ n | q_{m} ∈ F_{i}}| = ∞ .  (5.2)

Schließlich wird, wie in [Kla91], das Fortschrittsmaß Φ̃_{i} zu einem Pseudo-Fort-schrittsmaß Φ_{i} : U_{i}(t) → {0, 1, …, 2N + 1} abgeschwächt, wodurch ein endlicher Wertebereich entsteht. Für α < ω_{1} sei das Prädikat const(α) wahr, wenn ein unendlicher Pfad (q_{n}, n) →^{a_{i},t} (q_{n+1}, n + 1) →^{a_{i},t} ⋯ in U_{i}(t) derart existiert, daß Φ̃_{i}(q_{m}, m) = α für alle m ≥ n erfüllt ist. Wegen der durch N beschränkten Weite des Berechnungsgraphen (U_{i}(t), →^{a_{i},t}) existieren nach dem Prinzip von Dirichlet höchstens N Ordinalzahlen 0 < α_{1} < … < α_{M} < ω_{1} (M ≤ N), die const(α) = erfüllen. Mit α_{0} = 0 und α_{M+1} := ω_{1} wird Φ_{i} : U_{i}(t) → {0, 1, …, 2N + 1} definiert für (q, n) ∈ V_{i}(t) durch:

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

Für (q, n) ∈ U_{i}(t) \ V_{i}(t) sei außerdem Φ_{i}(q, n) := 2N + 1. Die Abbildung Φ_{i} erfüllt Bedingung (2iii): sonst gäbe es ein n ∈ IN und eine

Folge (q_{m}, m)_{m≥n} ⊆ U_{i}(t) mit (q_{m}, m) →^{a_{i},t} (q_{m+1}, m + 1), m ≥ n, mit Φ_{i}(q_{m}, m) =

Φ_{i}(q_{n}, n) = 2k, für alle m ≥ n und ein geeignetes k ≤ M. Mit der Monotonie von Φ̃_{i}, sowie der Tatsache, daß ω_{1} wohlgeordnet ist, gäbe es ein n′ ≥ n und ein α_{k} < α < α_{k+1} mit Φ̃_{i}(q_{n′}, n′) = Φ̃_{i}(q_{m}, m) = α, für alle m ≥ n′. Somit würde const(α) gelten und der Definition der (α_{i})_{1≤i≤M} widersprechen. Mit der Definition von Φ_{i} folgt schließlich für alle (q, n), (q′, n + 1) ∈ U_{i}(t) mit

(q, n) →^{a_{i},t} (q′, n + 1) und Φ_{i}(q, n) = Φ_{i}(q′, n + 1):

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

Es bleibt nur noch zu zeigen, daß der Zustandsraum, der nicht durch die Fortschrittsmaße (Φ_{i})_{1≤i≤k} erfaßt wird, nicht zu einem A-Ablauf von t synchronisiert werden kann (Bedingung (3)). Angenommen, für jedes endliche Präfix t_{0} ≤ t mit |t_{0}|_{a} = |t|_{a} für alle a ∈ Ā, existiert ein Ablauf r ∈ R_{A}(t_{0}) auf t_{0} so, daß zugleich δ(r, t_{0})_{a} = q_{a}^{f} für alle a ∈ Ā und (δ(r, ∂_{a_{i}}(t_{0})), |t_{0}|_{a_{i}} − 1) ∈ U_{i}(t) \ V_{i}(t) gilt. Sei t = t_{0}t_{1} ⋯ t_{k}, wobei alph(t_{i}) = A_{i} für alle 1 ≤ i ≤ k. Wir wählen t_{0} groß genug so, daß max(t_{0}) ∩ A = {a_{1}, …, a_{k}} und alph(∂_{a_{i}}(t_{0})^{−1}t_{i}) = A_{i} gelten. Wir können nun die Tatsache verwenden, daß von jedem Knoten aus U_{i}(t) \ V_{i}(t) ≠ ∅ ein Berechnungspfad ausgeht, auf dem ein Zustand aus F_{i} unendlich oft wiederholt wird (5.2). Damit existiert für jedes i ein Ablauf r_{i} auf dem zusammenhängenden Suffix t_{i}, der im globalen Zustand δ(r, ∂_{a_{i}}(t_{0})) startet so, daß q_{a_{i}}^{f} ∈ inf_{a_{i}}(r_{i}) erfüllt ist. Wir können nun einen Widerspruch herleiten, indem wir einen akzeptierenden Ablauf r′ für t wie folgt konstruieren: r′ entspricht r auf dem Präfix t_{0} bzw. r_{i} auf dem Suffix t_{i}, 1 ≤ i ≤ k. Offensichtlich gilt q_{a}^{f} ∈ inf_{a}(r′), für alle a ∈ Ā ∪ {a_{1}, …, a_{k}}, und somit würde der Widerspruch t ∈ L(A) folgen. □

Wir sind nun in der Lage, einen asynchron-zellulären Büchi Automaten B zu definieren so, daß B die Sprache L(A)^{co}∩Inf(A) erkennt. Dabei sei A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, {(q^{f}, A, {a_{1}, …, a_{k}})}). Wir folgen weiterhin der Konstruktion von Klarlund und definieren B so, daß ein geeignetes Pseudo-Fortschrittsmaß geraten wird. Zusätzlich werden wir die Berechnungs-Untergraphen (G_{i}(t))_{1≤i≤k} raten. Der Komplement-Automat basiert auf dem Potenzautomaten, der in Abschnitt 5.1 als A_{μ} mit μ = (ν, ρ) konstruiert wurde. Sei im folgenden der Potenzautomat von ((Q_{a})_{a∈Σ}(δ_{a})_{a∈Σ}, q_{0}) durch A_{μ} = ((Q̃_{a})_{a∈Σ}, (δ̃_{a})_{a∈Σ}, q̃_{0}) bezeichnet (Endzustände werden im folgenden außer acht gelassen). Weiterhin bezeichnen wir mit [2N + 1]_{p}^{Q} die Menge der partiellen Abbildungen von Q nach {0, 1, …, 2N + 1}, und mit dom(f) die Definitionsmenge einer partiellen Abbildung f ∈ [2N + 1]_{p}^{Q}. Es sei B = ((S_{a})_{a∈Σ}, (Δ_{a})_{a∈Σ}, I, T ) definiert durch:

1.

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

Weiterhin sei für alle a ∈ {a_{1}, …, a_{k}} und alle (q̃_{a}, α_{a}, A_{a}) ∈ S_{a} folgende Bedingung erfüllt:

dom(α_{a}) = {f(a) | f ∈ R, wobei q̃_{a} = (N, R) für ein N}.

(D.h., N bzw. R bezeichnen die ν- bzw. ρ-Komponente des lokalen Zustandes im Potenzautomaten.)

2. Sei a ∉ {a_{1}, …, a_{k}}. Dann gilt s′_{a} ∈ Δ_{a}((s_{b})_{b∈D(a)}) genau dann, wenn s′_{a} = δ̃_{a}((q̃_{b})_{b∈D(a)}), mit s_{b} = q̃_{b} bzw. s_{b} ∈ {q̃_{b}} × [2N + 1]_{p}^{Q} × P(Q), für alle b ∈ D(a).

Für a = a_{i}, 1 ≤ i ≤ k, seien s_{a} = (q̃_{a}, α_{a}, A_{a}) und s′_{a} = (q̃′_{a}, α′_{a}, A′_{a}). Dann gilt s′_{a} ∈ Δ_{a}((s_{b})_{b∈D(a)}) genau dann, wenn

• q̃′_{a} = δ̃((q̃_{b})_{b∈D(a)}), für q̃_{b} = s_{b}, b ∈ D(a) \ {a};

• Für alle q ∈ dom(α_{a}), q′ ∈ dom(α′_{a}) mit q →^{(a)} q′ gilt (für die Notation →^{(a)} siehe Beweis von Satz 5.1.2.):

(a) α_{a}(q) ≥ α′_{a}(q′) und

(b) Aus α_{a}(q) = α′_{a}(q′) folgt q′_{a} ≠ q_{a}^{f} oder α_{a}(q) ∈ {0, 2, …, 2N} oder α_{a}(q) = 2N + 1.

• A′_{a} = \{ \begin{matrix}dom(α′_{a}) & falls A_{a} = ∅ \\ \{q′ ∈ dom(α′_{a}) | ∃q ∈ dom(α_{a}) ∩ A_{a} mit \\ q →^{(a)} q′ und \\ α_{a}(q) = α′_{a}(q′) ∈ \{0, 2, …, 2N\}\} & sonst. \end{matrix}

3. (s^{f}, A, {a_{1}, …, a_{k}}) ∈ T genau dann, wenn für ein u ∈ IM(Σ, D) mit q̃_{a} = (ν(∂_{a}(u)), ρ(∂_{a}(u))), a ∈ Σ und Abbildungen α_{a} ∈ [2N + 1]_{p}^{Q}, a ∈ {a_{1}, …, a_{k}}, gilt:

(a) s_{a}^{f} ∈ {q̃_{a}, α_{a}, ∅), für alle a ∈ {a_{1}, …, a_{k}}, bzw. s_{a}^{f} = q̃_{a}, sonst.
(b) Sei C = Ā ∪ {a_{1}, …, a_{k}}. Dann erfüllt jedes f ∈ ρ(∂_{C}(u))
• Entweder f(a)_{a} ≠ q_{a}^{f}, für ein a ∈ Ā,
• oder α_{a}(f(a)) ≠ 2N + 1, für ein a ∈ {a_{1}, …, a_{k}}.

(c) Für alle s_{0} ∈ I, a ∈ Σ gilt: (s_{0})_{a} = (q̃_{0})_{a} bzw. (s_{0})_{a} = ((q̃_{0})_{a}, α_{a}, ∅),

für ein α_{a} ∈ [2N + 1]_{p}^{Q}.

Satz 5.2.3 Es gilt: L(B) = L(A)^{co} ∩ Inf(A).

Beweis: Wir nehmen zunächst an, daß alphinf(t) = A und t ∉ L(A) gelten. Mit Satz 5.2.1 erhalten wir Berechnungs-Untergraphen (G_{i}(t))_{1≤i≤k} und Pseudo-Fortschrittsmaße (Φ_{i})_{1≤i≤k}, die die drei Bedingungen erfüllen. Ein akzeptierender Ablauf des Automaten B auf t kann unmittelbar erklärt werden:

1. Für a ∉ {a_{1}, …, a_{k}} und n < |t|_{a}, sei r(a, n) = δ̃(q̃_{0}, t[a, n])_{a}.

2. Für a = a_{i}, 1 ≤ i ≤ k, sei r(a, n) = (q̃_{a}, α_{a}, A_{a}), wobei

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

• Mit q̃_{a} = (N, R) sei dom(α_{a}) = {f(a) ∈ Q | f ∈ R}.

• Für alle q ∈ dom(α_{a}) sei α_{a}(q) = Φ_{i}(q, n).

Schließlich ist die obige Komponente A_{a} deterministisch berechnet. Bedingung (2iii) aus Satz 5.2.1 erzwingt für a ∈ {a_{1}, …, a_{k}} die Existenz lokaler Zustände (p̃_{a}, α_{a}, ∅) ∈ inf_{a}(r), wobei p̃_{a} = (ν(∂_{a}(u)), ρ(∂_{a}(u))) für ein gewisses u ∈ IM(Σ, D) und α_{a} ∈ [2N + 1]_{p}^{Q} gilt. Wäre dies für ein a ∈ {a_{1}, …, a_{k}} nicht erfüllt, so gäbe es einen Index n_{a} ∈ IN so, daß r(a, n) = ((q̃_{n})_{a}, α_{n,a}, A_{n,a}) mit A_{n,a} ≠ ∅, für alle n ≥ n_{a}. Damit könnte ein unendlicher Untergraph von V_{i}(t) erzeugt werden, mit Knotenmenge ∪_{n≥n_{a}}A_{n,a} × {n}. Darauf läßt sich das Lemma von König anwenden, womit ein unendlicher Pfad mit konstantem Wert in {0, 2, …, 2N} und damit ein Widerspruch erzielt werden. Für a ∈ Ā gilt inf_{a}(r) = {p̃_{a}}. Die Bedingung (3) des Satzes 5.2.1 sichert nun zu, daß keine Abbildung f ∈ ρ(∂_{C}(u)) existiert so, daß f(a)_{a} = q_{a}^{f} für alle a ∈ Ā, bzw. α_{a}(f(a)) = 2N + 1, für alle a ∈ {a_{1}, …, a_{k}}. Für die Rückrichtung sei r ein akzeptierender B-Ablauf auf t, mit Tafelelement (s^{f}, A, {a_{1}, …, a_{k}}). Damit gilt zunächst alphinf(t) = A. Erneut gibt es eine kanonische Beziehung zwischen akzeptierenden Abläufen und Berechnungs-Untergraphen bzw. Pseudo-Fortschrittsmaße: für a = a_{i} und Δ(r, t[a, n])_{a} := (q̃_{a}, α_{a}, A_{a}) sei (q, n) ∈ V_{i}(t) genau dann, wenn α_{a}(q) ∈ {0, 1, …, 2N}. Für q ∈ dom(α_{a}) setze Φ_{i}(q, n) := α_{a}(q). Mit s_{a}^{f} ∈ Q̃_{a} × [2N + 1]_{p}^{Q} × {∅} ist es leicht zu sehen, daß Bedingung (2iii) aus Satz 5.2.1 erfüllt ist. Schließlich sei t_{0} ∈ IM(Σ, D) ein Präfix von t, t_{0} < t, mit Δ(r, t_{0})_{a} = s_{a}^{f} für a ∈ Ā ∪ {a_{1}, …, a_{k}} und |t_{0}|_{a} = |t|_{a} für alle a ∈ Ā. Mit dem zweiten Teil der Definition der Tafel ist auch die Synchronisations-Bedingung (3) aus Satz 5.2.1 unmittelbar erfüllt. □

Abschließend können wir das Ergebnis dieses Abschnitts im folgenden Theorem zusammenfassen:

Theorem 5.2.4 Sei A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, T ) ein (nichtdeterministischer) asynchron-zellulärer Büchi Automat mit Tafel T ⊆ (∏_{a∈Σ} Q_{a}) × P(Σ) × P(Σ) und N globalen Zuständen. Dann kann ein asynchron-zellulärer Büchi Automat B = ((S_{a})_{a∈Σ}, (Δ_{a})_{a∈Σ}, s_{0}, T′) (mit Tafel T′ ⊆ (∏_{a∈Σ} S_{a}) × P(Σ) × P(Σ)) effektiv angegeben werden so, daß L(B) = L(A)^{co} gilt. Der Komplement-Automat B hat 2^{O(N^{|Σ|})} globale Zustände (für |Σ| ≥ 2).

Abschließend wollen wir noch anmerken, daß wenn wir lediglich an einem Komplement-Automaten mit I-Diamant Eigenschaft interessiert wären, eine alternative Konstruktion existiert. Es handelt sich um die Konstruktion von Pécuchet [Péc86], die auf saturierenden Morphismen basiert und einen Automaten mit 2^{O(N^{2})} Zustände ergibt.

I-Diamant Automaten

In den bisherigen Betrachtungen haben wir uns auf Automaten mit verteilter Kontrolle konzentriert, die die nebenläufige Ausführung unabhängiger Aktionen erlauben. Wenn man hingegen den klassischen Ansatz der M-Automaten [Eil74] für das Monoid der endlichen Spuren M = IM = IM(Σ, D) verfolgt, so werden deterministische Wortautomaten A = (Q, δ, q_{0}, F) mit I-Diamant Eigenschaft betrachtet (siehe Abbildung 6.1). Mit der I-Diamant Eigenschaft wird Nebenläufig-

[figure: a; b; b; a; q_{1}; q_{2}; q_{3}; q_{4}; ∀q_{1}, q_{2}, q_{3} :; ∃q_{3} :]

Abbildung 6.1: I-Diamant Eigenschaft

keit in Form von Interleaving ausgedrückt, indem alle sequentiellen Ausführungen einer Spur dasselbe Übergangsverhalten im Automaten zeigen. Im folgenden bezeichnen wir mit [L] den Abschluß einer Wortsprache L ⊆ Σ^{∞} bzgl. dem Abhängigkeitsalphabet (Σ, D), d.h. es sei [L] = φ^{−1}φ(L), wobei φ : Σ^{∞} → IR(Σ, D) die kanonische Abbildung bezeichnet. Eine Sprache L ⊆ Σ^{∞} heißt abgeschlossen, wenn L = [L] gilt. Während die von I-Diamant Automaten erkannten Sprachen aus Σ^{∗} abgeschlossen sind, ist dies beim Übergang zu Sprachen aus Σ^{∞}, d.h. zu Muller bzw. Büchi Automaten, nicht mehr gegeben. Darin liegt ein wesentlicher Nachteil dieses Automatenmodells und damit der Grund dafür, das asynchrone Modell mit lokaler Akzeptanz für die Charakterisierung erkennbarer reeller Spursprachen dem I-Diamant Modell vorzuziehen. Mit der ersten Charakterisierung der Familie Rec(IR) durch nichtdeterministische, asynchron-zelluläre Büchi Automaten [GP92] bzw. mit dem Ergebnis des Kapitels 2 gilt aber: jede erkennbare reelle Spursprache kann mit einem nichtdeterministischen I-Diamant Automaten mit (verallgemeinerter) Büchi Bedingung, bzw. mit einem deterministischen I-Diamant Muller Automaten akzeptiert werden. Diese Eigenschaft des Automatenmodells macht natürlich die Frage nach der Abgeschlossenheit der erkannten Sprachen aus Σ^{ω} sehr interessant.

6.1 Deterministische I-Diamant Muller Automaten

In diesem Abschnitt zeigen wir, daß eine natürliche Einschränkung der I-Diamant Muller Automaten existiert, die die Familie der erkennbaren reellen Spursprachen charakterisiert. Im gesamten Abschnitt betrachten wir durchgehend deterministische Muller Automaten, daher werden wir den Zusatz “deterministisch” häufig weglassen. Mit dem nachfolgenden bekannten Beispiel von Gastin/Petit wird ersichtlich, daß die I-Diamant Eigenschaft nicht die Abgeschlossenheit der von Muller Automaten akzeptierten Sprachen zusichert.

Beispiel 6.1.1 Sei (Σ, D) = a −c −b und betrachte den Automaten A aus Abbildung 6.2. Sei q_{1} der Anfangszustand und betrachte die einelementige Tafel T = {T } mit T = {q_{1}, q_{2}, q_{3}, q_{4}}. Der Automat A ist I-Diamant, aber L(A) ist nicht abgeschlossen: es gilt nämlich (abcbac)^{ω} ∈ L(A), aber (abc)^{ω} ∉ L(A).

[figure: A :; c; q_{1}; q_{2}; q_{4}; q_{3}; a; a; b; b]
Abbildung 6.2: T = {{q_{1}, q_{2}, q_{3}, q_{4}}}

Das nächste Beispiel, das von K. Reinhardt angegeben wurde, zeigt eine weitere negative Eigenschaft von I-Diamant Muller Automaten. Damit wird gezeigt, daß der Abschluß [L(A)] der von einem I-Diamant Muller Automaten A akzeptierten Sprache im allgemeinen nicht erkennbar bleibt. Dieses Verhalten verdeutlicht einen wesentlichen Unterschied zu I-Diamant Büchi Automaten. Beim letzteren läßt sich die akzeptierte Sprache L = L(A) darstellen als endliche Vereinigung von Sprachen KN^{ω}, mit K, N = N^{+} ⊆ Σ^{∗} erkennbar und abgeschlossen. Damit kann φ(L) dargestellt werden als φ(L) = ⋃_{endlich} φ(K)φ(N)^{ω},

wobei φ(K), φ(N) ⊆ IM(Σ, D) erkennbare Spursprachen sind. Mit den Abschlußeigenschaften der Klasse Rec(IR) ist φ(L) eine erkennbare reelle Spursprache und schließlich folgt, daß [L(A)] = φ^{−1}φ(L) eine erkennbare Wortsprache ist.

Beispiel 6.1.2 Sei weiterhin (Σ, D) = a −c −b und betrachte den Automaten A aus Abbildung 6.3.

[figure: A :; a; b; a; b; b; a; c; c; 1; 2; 3; 4]

Abbildung 6.3: T = {T } mit T = {2, 3, 4}, Anfangszustand q_{0} = 3.

Es gilt L(A) ⊆ {a, b, c}^{∗}((ba)^{∗}cc)^{ω}. Offensichtlich ist L(A) nicht abgeschlossen und der Abschluß [L(A)] ist nicht erkennbar, da gilt:

[L(A)] ∩ ({a, b}^{∗}cc)^{ω} = {u_{0} cc u_{1} cc … | wobei |u_{n}|_{a} = |u_{n}|_{b}, für alle n ≥ 1}.

Aus den obigen Beispielen ist es ersichtlich, daß eine Einschränkung der Tafeln notwendig ist, um sicherzustellen, daß die akzeptierten Sprachen abgeschlossen sind. Wir geben eine solche Einschränkung für reduzierte Tafeln, die im folgenden definiert werden. Zuvor vereinbaren wir folgende Notation für einen (deterministischen) Automaten A = (Q, δ, q_{0}) und ein Wort u ∈ Σ^{ω}: mit inf(q, u) bezeichnen wir die Menge der Zustände, die auf dem Übergangspfad, der mit u beschriftet ist und in Zustand q startet, unendlich oft vorkommen. Nun heißt eine Tafel T ⊆ P(Q) reduziert, wenn für jedes Element T ∈ T ein Wort u ∈ Σ^{ω} derart existiert, daß T = inf(q_{0}, u) gilt. Für die angekündigte Einschränkung der Tafeln benötigen wir folgende

Definition 6.1.3 Sei A = (Q, δ, q_{0}, T ) ein Muller Automat.

1. Für q ∈ Q und v ∈ Σ^{∗} sei τ(q, v) = { δ(q, u) | u ist ein Präfix von v} die Menge der Zustände, die auf dem Übergangspfad vorkommen, der mit v beschriftet ist und in q startet.

2. Eine Tafel T ⊆ P(Q) heißt abgeschlossen, wenn für alle T ∈ T , q ∈ T und v ∈ Σ^{∗} mit δ(q, v) = q und T = τ(q, v) gilt:

∀w ∈ Σ^{∗} : φ(w) = φ(v) ⇒ τ(q, w) ∈ T .

Die Aussage des folgenden Satzes findet man in ähnlicher Form in [GP91], jedoch ohne eine algorithmische Behandlung des Abgeschlossenheitsproblems.

Satz 6.1.4 Sei A = (Q, δ, q_{0}, T ) ein deterministischer I-Diamant Muller Automat mit reduzierter Tafel T . Dann ist die von A akzeptierte Sprache L(A) genau dann abgeschlossen, wenn die Tafel T gemäß Definition 6.1.3 abgeschlossen ist.

Beweis: Nehmen wir zunächst an, die Sprache L(A) sei abgeschlossen und betrachten ein Element T ∈ T der Tafel. Mit der Annahme über die Reduziertheit der Tafel existieren Wörter u, v ∈ Σ^{∗} und ein Zustand q ∈ Q so, daß gilt:

δ(q_{0}, u) = q, δ(q, v) = q und τ(q, v) = T.

Sei w ∈ Σ^{∗} ein zu v äquivalentes Wort, d.h. φ(w) = φ(v). Wegen uv^{ω} ∈ L(A) zusammen mit der Abgeschlossenheit von L(A) gilt auch uw^{ω} ∈ L(A). Nun ist A deterministisch, woraus δ(q, w) = q folgt und somit auch inf(q_{0}, uw^{ω}) = τ(q, w). Damit folgt unmittelbar die Aussage τ(q, w) ∈ T . Für die Rückrichtung sei die Tafel T abgeschlossen. Es genügt nun zu zeigen, daß für alle (a, b) ∈ I gilt: ab ≡ ba (vgl. [DGP91]), wobei wir mit ≡ die syntaktische Kongruenz der Sprache L(A) bezeichnen. (Für die Definition der syntaktischen Kongruenz siehe Abschnitt 1.3.) Sei zunächst uabvw^{ω} ∈ L(A), wobei im folgenden (a, b) ∈ I gilt. Da der Automat A die I-Diamant Eigenschaft hat, folgt daraus δ(q_{0}, uabv) = δ(q_{0}, ubav) und somit direkt die Aussage ubavw^{ω} ∈ L(A). Schließlich betrachten wir ein Wort u(abv)^{ω} ∈ L(A), mit u, v ∈ Σ^{∗}. Offensichtlich existieren ganze Zahlen r, s ≥ 0 und ein q ∈ Q so, daß der Übergangspfad faktorisiert werden kann als δ(q_{0}, u(abv)^{r}) = q, δ(q, (abv)^{s}) = q und es gilt inf(q_{0}, u(abv)^{ω}) = τ(q, (abv)^{s}) ∈ T . Die Abgeschlossenheit der Tafel T erzwingt τ(q, (bav)^{s}) ∈ T und daraus folgt direkt u(bav)^{ω} ∈ L(A). □

Der letzte Satz gibt eine vollständige Charakterisierung der I-Diamant Muller Automaten, die abgeschlossene Sprachen erkennen. Um einen effizienten Algorithmus für dieses Problem angeben zu können, benötigen wir eine verfeinerte Charakterisierung der Tafeln.

Satz 6.1.5 Sei A = (Q, δ, q_{0}, T ) ein deterministischer I-Diamant Muller Automat mit reduzierter Tafel T . Es gilt: die Tafel T ist genau dann abgeschlossen, wenn die beiden nachfolgenden Bedingungen erfüllt sind:

1. Für alle T ∈ T , q ∈ Q, (a, b) ∈ I mit {q, δ(q, a), δ(q, ab)} ⊆ T gilt auch T ∪ {δ(q, b)} ∈ T .

2. Für alle T ∈ T , q ∈ Q, (a, b) ∈ I mit {q, δ(q, a), δ(q, ab)} ⊆ T mit der zusätzlichen Voraussetzung, daß ein Wort v ∈ Σ^{∗} existiert mit

δ(q, abv) = q und τ(δ(q, ab), v) = (T \ {δ(q, a)}) ∪ {δ(q, b)},

gilt auch (T \ {δ(q, a)}) ∪ {δ(q, b)} ∈ T .

Beweis: Angenommen, die Tafel T ist abgeschlossen. Es seien T ∈ T und (a, b) ∈ I so, daß {q, δ(q, a), δ(q, ab)} ⊆ T gilt. Mit der Voraussetzung, daß die Tafel T reduziert ist, existieren Wörter u, v, w ∈ Σ^{∗} mit δ(q_{0}, u) = q, δ(q, v) = q, τ(q, v) = T, δ(q, abw) = q und τ(q, abw) ⊆ T. Daraus folgt unmittelbar τ(q, vabw) = T und damit auch τ(q, vbaw) = T ∪ {δ(q, b)} ∈ T . Für die zweite Bedingung des Satzes sei v ∈ Σ^{∗} so, daß δ(q, abv) = q zusammen mit τ(δ(q, ab), v) = (T \ {δ(q, a)}) ∪ {δ(q, b)} gilt. Damit folgt τ(q, abv) = T ∪ {δ(q, b)} bzw. τ(q, bav) = (T \ {δ(q, a)}) ∪ {δ(q, b)}. Wir können nun die erste Bedingung anwenden und schließen, daß T ∪ {δ(q, b)} ∈ T ein Tafelelement ist, daher auch (T \ {δ(q, a)}) ∪ {δ(q, b)} ∈ T . Für die Rückrichtung seien die beiden Bedingungen 1. und 2. erfüllt. Wir betrachten ein Tafelelement T ∈ T , zusammen mit q ∈ T und v ∈ Σ^{∗} so, daß δ(q, v) = q und τ(q, v) = T gelten. Sei weiterhin w ∈ Σ^{∗} ein zu v äquivalentes Wort. Wir wollen zeigen, daß τ(q, w) ∈ T . Ohne Einschränkung seien v, w von der Form v = v_{1}abv_{2} und w = v_{1}bav_{2} für (a, b) ∈ I und gewisse v_{1}, v_{2} ∈ Σ^{∗}. Mit q_{1} := δ(q, v_{1}) erhalten wir τ(q_{1}, abv_{2}v_{1}) = T, zusammen mit τ(q, w) = τ(q_{1}, bav_{2}v_{1}). Abhängig davon, ob nun δ(q_{1}, a) ∈ τ(δ(q_{1}, ba), v_{2}v_{1}) gilt oder nicht, folgern wir mit einer der beiden Bedingungen, daß τ(q, w) ∈ T erfüllt ist:

• Falls δ(q_{1}, a) ∈ τ(δ(q_{1}, ba), v_{2}v_{1}), so folgt mit der ersten Bedingung τ(q, w) = {δ(q_{1}, b)} ∪ τ(δ(q_{1}, ba), v_{2}v_{1}) = T ∪ {δ(q_{1}, b)} ∈ T .

• Ansonsten wenden wir die zweite Bedingung an und erhalten abschließend erneut τ(q, w) = (T \ {δ(q_{1}, a)}) ∪ {δ(q_{1}, b)} ∈ T .

□

Im zweiten Teil dieses Abschnitts zeigen wir, daß das Abgeschlossenheitsproblem für deterministische I-Diamant Muller Automaten NL-vollständig ist (wobei NL die Komplexitätsklasse NSPACE(log(n)) bezeichnet). Wir verwenden im folgenden den Abschluß von NL unter Komplement ([Imm88, Sze88]) und die NL-Vollständigkeit des Erreichbarkeitsproblems 2-GAP in (gerichteten) Graphen mit Ausgangsgrad höchstens 2.

Bemerkung 6.1.6 Die Frage, ob zu einem gegebenem Muller Automaten A = (Q, δ, q_{0}, T ) und Abhängigkeitsalphabet (Σ, D) der Automat deterministisch ist und die I-Diamant Eigenschaft hat, kann in DSPACE(log(n)) beantwortet werden.

Satz 6.1.7 Sei (Σ, D) gegeben. Die Frage, ob die Tafel eines deterministischen, I-Diamant Muller Automaten A = (Q, δ, q_{0}, T ) reduziert ist, ist NL-vollständig.

Beweis: Es ist leicht zu sehen, daß die Frage mit nichtdeterministischen logarithmischen Platz beantwortet werden kann: für jedes T ∈ T wird q ∈ T geraten und überprüft, daß es von q_{0} erreichbar ist; anschließend wird v ∈ Σ^{O(n)} (mit |Q| = n) geraten und δ(q, v) = q und τ(q, v) = T gleichzeitig überprüft, indem die Bedingung τ(q, v) ⊆ T aufrechterhalten wird, zusammen mit einem Hochzählen der durchlaufenen Zustände aus T, gemäß ihrer Reihenfolge in der Eingabe. Im positiven Fall wird zum nächsten T′ ∈ T übergegangen. Für die Härte kann eine einfache Reduktion von 2-GAP auf das vorliegende Problem angegeben werden. □

Der obige Satz zeigt also, daß bereits die Preprocessing-Phase des Abgeschlossenheitsproblems NL-vollständig ist. Interessanterweise bleibt das Problem NLvollständig auch unter der Annahme, daß die Reduziertheit der Tafel bekannt ist.

Theorem 6.1.8 Es seien (Σ, D) und ein deterministischer I-Diamant Muller Automat A = (Q, δ, q_{0}, T ) mit reduzierter Tafel T gegeben. Die Frage, ob L(A) abgeschlossen ist, ist NL-vollständig.

Beweis: Wir zeigen zunächst, daß die beiden Bedingungen des Satzes 6.1.5 nichtdeterministisch mit logarithmischen Platz beantwortet werden können. Während dies für die erste Bedingung offensichtlich ist, genügt es für die zweite Bedingung zu überprüfen, daß für gewisse T ∈ T , {q, δ(q, a), δ(q, ab)} ⊆ T ein Wort v ∈ Σ^{O(n)} (mit |Q| = n) derart existiert, daß δ(q, abv) = q und τ(δ(q, ab), v) = (T \ {δ(q, a)}) ∪ {δ(q, b)} gelten. Dies kann analog zum Beweis von Satz 6.1.7 durchgeführt werden. Für die Härte des Problems genügt es, ein Alphabet mit 3 Buchstaben zu betrachten, (Σ, D) = a −c −b. Sei G = ({p, q, x_{1}, …, x_{n}}, E) eine Instanz von 2-GAP, wobei nach der Existenz eines Pfades von p nach q gefragt wird. Die Kanten aus E werden beliebig mit b, c beschriftet so, daß von keinem Knoten zwei Kanten mit derselben Beschriftung ausgehen. Ohne Einschränkung geht von p genau eine Kante aus (beschriftet mit b), und q hat keine ausgehende Kante, dafür eine mit c beschriftete eingehende Kante. Wir fügen zwei neue Knoten r, s und folgende zusätzliche Kanten ein: (q, b, r), (r, a, p), (q, a, s), (s, b, p), (p, c, s), (s, c, q), (q, c, x_{i}), (x_{i}, c, p) für 1 ≤ i ≤ n (siehe Abbildung 6.4). Nun gibt es eventuell Knoten x_{i}, die zwei mit c beschriftete ausgehende Kanten haben. Um den Determinismus wiederherzustellen, können 2 Kanten (x_{i}, c, y), (x_{i}, c, y′) mit y ≠ y′ durch die Einführung eines neuen Knotens x′_{i}, zusammen mit neuen Kanten (x_{i}, c, x′_{i}), (x′_{i}, b, y), (x′_{i}, c, y′) ersetzt werden. Weiterhin kann der Nichtdeterminismus, der durch Knoten q verursacht wird, behoben werden durch die Einführung neuer Knoten y_{i}, 1 ≤ i ≤ n − 1 und die Ersetzung der

[figure: q; p; s; r; x_{i}; …; …; b; a; a; b; c; c; c; c; c; b]

Abbildung 6.4: Reduktion von 2-GAP.

Kanten {(q, c, x_{i}) | 1 ≤ i ≤ n} durch die Kanten {(y_{i}, b, y_{i+1}), (y_{j}, c, x_{j}) | 1 ≤ i < n − 1, 1 ≤ j ≤ n − 1} ∪ {(q, c, y_{1}), (y_{n−1}, b, x_{n})}. Wir betrachten den entstandenen Graphen als deterministischen I-Diamant Muller Automaten mit Anfangszustand q und Tafel T = {T_{1}, T_{2}}, wobei T_{1} = Q = {r, s, p, q, x_{i}, x′_{i}, y_{j} | 1 ≤ i ≤ n, 1 ≤ j ≤ n − 1} und T_{2} = T_{1} \ {r}. Man beachte auch, daß die Tafel reduziert ist. Mit Satz 6.1.5 gilt schließlich, daß die Tafel (und damit L(A)) genau dann abgeschlossen ist, wenn kein Pfad von p nach q in G existiert. □

6.2 Nichtdeterministische I-Diamant Büchi Automaten

Wir zeigen in diesem Abschnitt, daß das Problem der Abgeschlossenheit der von einem nichtdeterministischen I-Diamant Büchi Automaten akzeptierten Sprache wesentlich schwieriger ist als für Muller Automaten. Im Büchi Fall ist es nämlich ein PSPACE-vollständiges Problem (wobei PSPACE die Klasse der im polynomiellen Platz lösbaren Probleme bezeichnet). Dies bedeutet, daß der Übergang von Büchi zu Muller Automaten einen exponentiellen Anstieg in der Größe hervorruft (wobei die Größe auch die Tafelgröße berücksichtigt). Zunächst einige Bemerkungen zum Automatenmodell. Wir wissen mit [GP92], daß die Familie der erkennbaren, abgeschlossenen ω-Wortsprachen genau charakterisierbar ist durch I-Diamant Automaten mit verallgemeinerter Büchi Akzeptanz. D.h., mit Automaten der Art A = (Q, δ, q_{0}, T ), mit T ⊆ P(Q). Ein Wort w ∈ Σ^{ω} wird von A akzeptiert, wenn ein T ∈ T und ein mit w beschrifteter Übergangspfad π derart existieren, daß inf(π) ⊇ T gilt, d.h. jeder Zustand aus T wird in π unendlich oft wiederholt. (Dabei bezeichnet für einen Übergangspfad π = (q_{0}, a_{0}, q_{1}, a_{1}, …), q_{n} ∈ Q, a_{n} ∈ Σ, inf(π) die Menge {q ∈ Q | ∃^{∞}n : q_{n} = q}.) Die nachfolgende Konstruktion von V. Diekert zeigt jedoch, daß gewöhnliche Büchi Automaten mit I-Diamant Eigenschaft genauso mächtig sind wie die verallgemeinerten I-Diamant Büchi Automaten.

Mit dem Ergebnis des Kapitels 2 können wir einen deterministischen asynchronzellulären Muller Automaten A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, T ) als Ausgangspunkt wählen. Im Laufe der Berechnung wird ein Tafelelement T = (T_{a})_{a∈Σ} geraten und anschließend überprüft, daß genau die lokalen Komponenten von T unendlich oft wiederholt werden. Sei Q = ∏_{a∈Σ} Q_{a} die Menge der globalen Zustände von A und δ : Q × Σ → Q die globale Übergangsfunktion. Ohne Einschränkung sei δ so, daß für alle q ∈ Q, a ∈ Σ, q′_{a} ∈ Q_{a} mit q′_{a} = δ_{a}((q_{b})_{b∈D(a)}) gilt: q′_{a} ≠ q_{a}. Damit gilt für ein Wort w ∈ Σ^{ω}, das mit T ∈ T akzeptiert wird: alphinf(w) = {a ∈ Σ | |T_{a}| ≥ 2}. Schließlich sei für A_{T} = {a ∈ Σ | |T_{a}| ≥ 2} die Menge lokaler Zustände S_{T} = ⋃_{a∈A_{T}} T_{a} definiert. Betrachte nun den nichtdeterministischen Büchi Automaten A′ = (Q′, δ′, q_{0}, F) mit Q′ = Q ∪ ⋃_{T ∈T} (Q×P(S_{T})×{T }) und der Übergangsrelation δ′ ⊆ Q′ ×Σ×Q′

gegeben durch

• q′ ∈ δ′(q, a), falls q′ ∈ δ(q, a) gilt.

• (q′, A, T) ∈ δ′(q, a), falls q′ ∈ δ(q, a) und A ⊆ S_{T} gelten.

• (q′, A′, T) ∈ δ′((q, A, T), a), falls q′ ∈ δ(q, a), a ∈ A_{T}, q′_{a} ∈ S_{T} und

1. Entweder A′ = ∅, falls A ∪ {q′_{a}} = S_{T},

2. oder ∅ ≠ A′ ⊆ A ∪ {q′_{a}}.

Es ist nicht schwer zu sehen, daß der Automat die I-Diamant Eigenschaft hat. Schließlich folgt mit F = ⋃_{T ∈T} {(q = (q_{a})_{a∈Σ}, ∅, T) | ∀a ∉ A_{T} : T_{a} = {q_{a}}} die

Behauptung L(A′) = φ^{−1}(L(A)).

Nun zurück zum Problem der Abgeschlossenheit für I-Diamant Büchi Automaten. Der folgende Satz gibt für ein Abhängigkeitsalphabet (Σ, D) eine Charakterisierung derjenigen Automaten, die eine abgeschlossenen Sprache erkennen. Analog zu Muller Automaten betrachten wir nur reduzierte Endzustandsmengen F, d.h. für jeden Zustand f ∈ F existiert ein Übergangspfad π mit f ∈ inf(π). Weiterhin vereinbaren wir folgende Notation: für A = (Q, δ, q_{0}, F) bedeutet q′ ∈ δ_{F} (q, u) für u ∈ Σ^{∗}, daß ein mit u beschrifteter Pfad von q nach q′ existiert, der durch einen Zustand aus F führt.

Satz 6.2.1 Sei A = (Q, δ, q_{0}, F) ein nichtdeterministischer I-Diamant Büchi Automat. Dann gilt: L(A) ist abgeschlossen genau dann, wenn für alle q, q′, s ∈ Q, x, y ∈ Σ^{∗} und (a, b) ∈ I mit

q ∈ δ(q_{0}, x), q′ ∈ δ(q, a) ∩ F, s ∈ δ(q′, b) und q ∈ δ(s, y)

positive ganze Zahlen p ≤ n, m ≤ 2n (mit n = |Q|) und ein Zustand q′′ ∈ Q derart existieren, daß gilt:

q′′ ∈ δ(q_{0}, x(bay)^{p}) und q′′ ∈ δ_{F} (q′′, (bay)^{m}).

Beweis: Nehmen wir an, es gilt L(A) = [L(A)] und betrachten wir q, q′, s ∈ Q, x, y ∈ Σ^{∗} so, daß die Voraussetzungen des Satzes erfüllt sind. Es gilt x(aby)^{ω} ∈ L(A) und damit auch x(bay)^{ω} ∈ L(A). Ein akzeptierender Pfad für x(bay)^{ω} kann nun ohne weiteres wie im Satz angegeben faktorisiert werden. Umgekehrt sei ≡_{L} die syntaktische Kongruenz von L = L(A). Mit [DGP] genügt es zu zeigen, daß ab ≡_{L} ba für alle (a, b) ∈ I gilt. Zunächst gilt offensichtlich xabyz^{ω} ∈ L genau dann, wenn xbayz^{ω} ∈ L. Betrachte nun x(aby)^{ω} ∈ L. Damit existieren k, l ≤ |Q| und ein Zustand q ∈ Q mit q ∈ δ(q_{0}, x(aby)^{k}) und q ∈ δ_{F} (q, (aby)^{l}). Es genügt, den Fall zu betrachten, in dem q′ ∈ δ(q, a) ∩ F gilt, wobei q ∈ δ(q′, by(aby)^{l−1}) (ansonsten kann direkt die I-Diamant Eigenschaft angewendet werden). Schließlich folgt mit y′ = y(bay)^{l−1} die Existenz eines Zustands q′′ ∈ Q und Indizes p, m mit q′′ ∈ δ(q_{0}, x(bay)^{k}(bay′)^{p}) und q′′ ∈ δ_{F} (q′′, (bay′)^{m}), und dies ergibt x(bay)^{ω} ∈ L. □

Bemerkung 6.2.2 Es genügt, die obige Eigenschaft für alle Wörter x, y ∈ Σ^{∗} mit beschränkter Länge |x| ≤ 2^{n} bzw. |y| ≤ 2^{2n^{2}} zu überprüfen (mit n = |Q|).

Satz 6.2.3 Gegeben sei ein Abhängigkeitsalphabet (Σ, D) und ein nichtdeterministischer I-Diamant Büchi Automat A = (Q, δ, q_{0}, F). Das Problem, ob L(A) abgeschlossen ist, liegt in PSPACE.

Beweis: Wir zeigen, daß die Negation der Charakterisierung des Satzes 6.2.1 in PSPACE überprüft werden kann. Eine nichtdeterministische Turing Maschine M rät zuerst q, q′, s ∈ Q, (a, b) ∈ I und überprüft q′ ∈ δ(q, a) ∩ F zusammen mit s ∈ δ(q′, b). Anschließend simuliert M den Potenzautomaten von A und rät on-line ein Wort x ∈ Σ^{∗} mit |x| ≤ 2^{n}. Dies kann mit O(n) Platz durchgeführt werden. Sei R_{1} ⊆ Q die erreichte Zustandsmenge. Die Turing Maschine M überprüft q ∈ R_{1} und rät Zustandsmengen R_{2}, …, R_{3n} ⊆ Q. Darauf wird erneut der Potenzautomat von A simuliert, und zwar rät M on-line ein Wort y mit |y| ≤ 2^{2n^{2}} und überprüft gleichzeitig, daß Δ(R_{i}, bay) = R_{i+1} für alle i gilt (wobei Δ die Übergangsfunktion des Potenzautomaten ist). Genauer, sei R_{i} = {q_{1i}, …, q_{n_{i},i}}. Für alle i und alle 1 ≤ j ≤ n_{i} generiert M schrittweise die Menge S_{ji} ⊆ Q der Folgezustände von q_{ji} bezüglich dem gleichzeitig geratenen Wort bay. Wenn ein Endzustand durchlaufen wird, so markiert M die Folgezustände. Gleichzeitig simuliert M den Potenzautomaten auf y ausgehend von s und verfolgt die Zustandsmenge S ⊆ Q. Nach dieser Phase überprüft M, daß q ∈ S und R_{i+1} = ⋃_{j=1}^{n_{i}} S_{ji} für alle i gilt. Schließlich überprüft M für alle q′′ ∈ Q und p ≤ n, m ≤ 2n mit q′′ ∈ R_{p} ∩ R_{p+m}, ob ein Pfad von q′′ nach q′′ (durch die Zustandsmengen R_{i}) durch die Endzustandsmenge F führt (anhand der Markierungen), und lehnt ab, falls dies der Fall ist. □

Theorem 6.2.4 Gegeben sei ein Abhängigkeitsalphabet (Σ, D) und ein nichtdeterministischer I-Diamant Büchi Automat A = (Q, δ, q_{0}, F). Das Problem, ob L(A) abgeschlossen ist, ist PSPACE-hart.

Beweis: Wir reduzieren im folgenden das Totalitäts-Problem “L(A) =^{?} Σ^{∗}”

[MS72] für nichtdeterministische endliche Automaten auf das vorliegende Problem. Sei A′ = (Q′, Γ, δ′, s, F′) ein endlicher Automat über dem Alphabet Γ. Es seien nun a, b ∉ Γ und betrachte das Alphabet Σ = Γ ∪ {a, b} mit der Unabhängigkeitsrelation I = {(a, b)}. Sei A = (Q, Σ, δ, q_{0}, F) ein nichtdeterministischer Büchi Automat mit Zustandsmenge Q = Q′ ∪ {q_{0}, 1, …, 7}, Endzustände F = {2, 7} und Übergangsrelation δ gegeben durch die folgende Abbildung (mit c ∈ Γ beliebig):

[figure: c; c; c; q_{0}; c; 1; 2; 4; 3; 6; f; ∀ f ∈ F′; ⋯; 7; 5; c; s; b; a; a; b; a; b; b; a]

Abbildung 6.5: Reduktion vom Totalitätsproblem.

Offensichtlich gilt w ∈ L(A) genau dann, wenn x ∈ Σ^{∗}, (y_{n})_{n≥1} ⊆ Σ^{∗} derart existieren, daß w = xy_{1}y_{2} … gilt, mit

1. entweder x ∈ Γ^{+}, y_{n} ∈ (ab+ba)Γ^{+} und y_{n} ∈ abΓ^{+} für unendlich viele n ≥ 1,

2. oder x ∈ Γ L(A′), y_{n} ∈ (ab + ba) ΓL(A′) und y_{n} ∈ baΓL(A′) für unendlich viele n ≥ 1.

Somit ist L(A) abgeschlossen genau dann, wenn L(A′) = Γ^{∗} gilt. □

Abschließende Bemerkungen und Ausblick

In der vorliegenden Arbeit haben wir wesentliche Aspekte der automatentheoretischen Charakterisierung erkennbarer reeller Spursprachen untersucht. Wir haben das Theorem von McNaughton auf reelle Spuren erweitert, indem wir die Äquivalenz zwischen Erkennbarkeit und Akzeptanz durch deterministische asynchron-zelluläre Muller Automaten gezeigt haben. Wir haben zunächst deterministische Spursprachen definiert und gezeigt, daß die Klasse erkennbarer reeller Spursprachen mit dem Booleschen Abschluß der Klasse deterministischer Sprachen übereinstimmt. Die Problematik einer geeigneten Charakterisierung deterministischer reeller Spursprachen zeigt hingegen, daß Fragen bezüglich der Definition von asynchronzellulären Büchi Automaten und/oder deterministischer Sprachen offen bleiben. In diesem Zusammenhang sollte hinzugefügt werden, daß ein alternativer Weg für die Untersuchung deterministischer Sprachen existiert, nämlich die topologische Charakterisierung. In der Theorie der unendlichen Wörter entsprechen die deterministischen Sprachen der G_{δ} Stufe in der Borel Hierarchie. In Zusammenarbeit mit P. Gastin (Univ. Paris 6) und A. Petit (Univ. Paris Sud) wurde dieser Aspekt für reelle Spursprachen untersucht. Es stellte sich heraus, daß eine analoge Charakterisierung, d.h. als Durchschnitt abzählbar vieler offener Mengen existiert, und zwar bezüglich der Metrik, die zum Monoid komplexer Spuren C(Σ, D) als Vervollständigung von IM(Σ, D) führt [Die93]. Dieses Ergebnis spricht daher eher für die Definition deterministischer Spursprachen. Wir haben weiterhin die Familie sternfreier reeller Spursprachen untersucht und gezeigt, daß klassische Resultate wie die Äquivalenz zur Aperiodizität von ω-Wörter auf reelle Spuren übertragen werden können. In diesem Bereich gibt es verschiedene weitere Fragen, deren Untersuchung vielversprechend zu sein scheint. Ein Beispiel wären die lokal testbaren Sprachen, für deren Definition es einen nicht sehr zufriedenstellenden Ansatz in [GRS91] für Sprachen endlicher Spuren gegeben hat. Eine partielle Lösung dieses Problems könnte z.B. darin bestehen, nicht nur die Faktoren u einer bestimmten Länge in der gegebenen Spur t = xuy zu betrachten, sondern sie zu Tripeln (u, D(alph(x)), D(alph(y))) zu erweitern. Ein solcher Ansatz würde direkt zu einer Kongruenzrelation führen.

Die in dieser Arbeit entwickelte Potenzautomaten-Konstruktion für asynchron-- zelluläre Automaten löst ein interessantes Problem in der Theorie endlicher Spuren, das Problem der direkten Determinisierung. Wir verwenden im entscheidenden Maße die Zeitmarkierungsfunktion der Zielonka-Konstruktion. Dies führt natürlich zur Frage der Notwendigkeit der Zeitmarkierung innerhalb einer solchen Konstruktion. Wir vermuten allerdings, daß unsere Konstruktion bezüglich der Größe des Potenzautomaten optimal ist. Im direkten Zusammenhang stellt sich natürlich auch die Frage nach der Größe des Komplement-Automaten. Im Fall der ω-Wortsprachen ist beispielsweise durch ein Beispiel von Max Michel [Mic88] die untere Schranke 2^{O(n log n)} für die Größe des Komplement-Automaten bekannt. Für asynchron-zelluläre Automaten kann durchaus erwartet werden, daß sowohl bei der Determinisierung als auch bei der Komplementierung von Büchi Automaten die Größe des Alphabets eine Rolle spielt.

Literaturverzeichnis

[Arn85] A. Arnold. A syntactic congruence for rational ω-languages. Theoretical Computer Science, 39:333–335, 1985.

[BD87] E. Best and R. Devillers. Sequential and concurrent behaviour in Petri net theory. Theoretical Computer Science, 55:87–136, 1987.

[Ber79] J. Berstel. Transductions and context-free languages. Teubner Studienbücher, Stuttgart, 1979.

[BMP90] P. Bonizzoni, G. Mauri, and G. Pighizzini. About infinite traces. In V. Diekert, ed., Proceedings of the ASMICS workshop Free Partially Commutative Monoids, Kochel am See, Oktober 1989, Report TUM-I9002, Technical University of Munich, pages 1–10, 1990.

[Büc60] J.R. Büchi. On a decision method in restricted second order arithmetic. In E. Nagel et al., eds., Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, pages 1–11. Stanford Univ. Press, Stanford, CA, 1960.

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

[CMZ90] R. Cori, Y. Métivier, and W. Zielonka. Applications of trace approximation to asynchronous automata and message passing with bounded time-stamps in asynchronous networks. Technical report, Univ. Bordeaux, 1990.

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

[CP85] R. Cori and D. Perrin. Automates et commutations partielles. R.A.I.R.O. — Informatique Théorique et Applications, 19:21–32, 1985.

[DGP] V. Diekert, P. Gastin, and A. Petit. Rational and recognizable complex trace languages. Information and Computation. To appear in.

[DGP91] V. Diekert, P. Gastin, and A. Petit. Recognizable complex trace languages. In A. Tarlecki, ed., Proceedings of the 16th Symposium on Mathematical Foundations of Computer Science (MFCS’91), Kazimierz Dolny (Poland) 1991, number 520 in Lecture Notes in Computer Science, pages 131–140, Berlin-Heidelberg-New York, 1991. Springer.

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

[Die93] V. Diekert. On the concatenation of infinite traces. Theoretical Computer Science, 113:35–54, 1993. Special issue STACS 91.

[DM93] V. Diekert and A. Muscholl. Deterministic asynchronous automata for infinite traces. In P. Enjalbert et al., eds., Proceedings of the 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS’93), Würzburg 1993, number 665 in Lecture Notes in Computer Science, pages 617–628, Berlin-Heidelberg-New York, 1993. Springer.

[Eil74] S. Eilenberg. Automata, Languages and Machines, volume A. Academic Press, New York and London, 1974.

[EM93] W. Ebinger and A. Muscholl. Logical definability on infinite traces. In A. Lingas et al., eds., Proceedings of the 20th International Colloquium on Automata, Languages and Programming (ICALP’93), Lund (Sweden) 1993, number 700 in Lecture Notes in Computer Science, pages 335–346, Berlin-Heidelberg-New York, 1993. Springer.

[FR85] M. P. Flé and G. Roucairol. Fair serializability of iterated transactions using fifo-nets. In G. Rozenberg, ed., Advances in Petri Nets, number 188 in Lecture Notes in Computer Science, pages 154–168. Springer, Berlin-Heidelberg-New York, 1985.

[Gas91] P. Gastin. Recognizable and rational trace languages of finite and infinite traces. In Choffrut C. et al., eds., 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.

[GP91] P. Gastin and A. Petit. Büchi (asynchronous) automata for infinite traces. Tech. rep., LRI, Université Paris-Sud, 1991.

[GP92] P. Gastin and A. Petit. Asynchronous automata for infinite traces. In W. Kuich, ed., 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.

[GPZ91] P. Gastin, A. Petit, and W. Zielonka. A Kleene theorem for infinite trace languages. In J. Leach Albert et al., eds., Proceedings of the 18th International Colloquium on Automata, Languages and Programming (ICALP’91), Madrid (Spain) 1991, number 510 in Lecture Notes in Computer Science, pages 254–266, Berlin-Heidelberg-New York, 1991. Springer.

[GR93] P. Gastin and B. Rozoy. The poset of infinitary traces. Theoretical Computer Science, 120:101–121, 1993.

[GRS91] G. Guaiana, A. Restivo, and S. Salemi. On aperiodic trace languages. In Choffrut C. et al., eds., 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 76–88, Berlin-Heidelberg-New York, 1991. Springer.

[Imm88] N. Immerman. Nondeterministic space is closed under complement. SIAM Journal on Computing, 17(5):935–938, 1988.

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

[KMS94] N. Klarlund, M. Mukund, and M. Sohoni. Determinizing asynchronous automata. In Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP’94), Jerusalem (Israel) 1994, Lecture Notes in Computer Science. Springer, 1994.

[Kwi89] M. Kwiatkowska. Event fairness and non-interleaving concurrency. Formal aspects of computing, 1(3):213–228, 1989.

[Kwi90] M. Kwiatkowska. A metric for traces. Information Processing Letters, 35:129–135, 1990.

[Lev44] F. W. Levi. On semigroups. Bull. Calcutta Math. Soc., 36:141–146, 1944.

[LL90] L. Lamport and N. Lynch. Distributed computing: models and methods. In Jan van Leeuwen, ed., Handbook of Theoretical Computer Science, volume B, pages 1157–1200. Elsevier, Amsterdam, 1990.

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

[Maz85] A. Mazurkiewicz. Semantics of concurrent systems: a modular fixed point approach. In G. Rozenberg, ed., Advances in Petri nets, number 188 in Lecture Notes in Computer Science, pages 353–375, Berlin-Heidelberg-New York, 1985. Springer.

[McN66] R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.

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

[MS72] A. Meyer and L. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In Proc. of the 13th Annual IEEE Symposium on Switching and Automata Theory, pages 125–129, 1972.

[Mus94] A. Muscholl. On the complementation of Büchi asynchronous cellular automata. In Proceedings of the 21st International Colloquium on Automata, Languages and Programming (ICALP’94), Jerusalem (Israel) 1994, Lecture Notes in Computer Science. Springer, 1994.

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

[Per] D. Perrin. Recent results on automata and infinite words. In M.P. Chytil et al., eds., Proceeding of the 11th Symposium on Mathematical Foundations of Computer Science (MFCS’84), Praha (CSFR) 1984.

[PP93] D. Perrin and J.-E. Pin. Mots Infinis. Tech. Rep. LITP 93.40, Université Paris 7, 1993. Book to appear.

[Saf88] S. Safra. On the complexity of ω-automata. In Proc. of the 29th Symposium on Foundations of Computer Science, 1988.

[Sch65] M. P. Schützenberger. On a factorization of free monoids. Proc. A.M.S., 16:21–24, 1965.

[Sch73] M. P. Schützenberger. Sur les r’elations rationelles fonctionelles. In M. Nivat, ed., Automata, languages and programming, pages 103–114. North-Holland, 1973.

[Sze88] R. Szelepcsényi. The method of forced enumeration for nondeterministic automata. Acta Informatica, 26:279–284, 1988.

[Tho90] W. Thomas. Automata on infinite objects. In Jan van Leeuwen, ed., Handbook of Theoretical Computer Science, chapter 4, pages 133–191. Elsevier Science Publishers B. V., 1990.

[Tho90b] W. Thomas. On logical definability of trace languages. In V. Diekert, editor, Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Kochel am See, Bavaria, FRG (1989), Report TUM-I9002, Technical University of Munich, pages 172–182, 1990.

[TZ90] W. Thomas and W. Zielonka. Logical definability of trace languages. Manuscript, 1990.

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

[Zie89] W. Zielonka. Safe executions of recognizable trace languages by asynchronous automata. In A. R. Mayer et al., eds., Proceedings Symposium on Logical Foundations of Computer Science, Logic at Botik ’89, Pereslavl-Zalessky (USSR) 1989, number 363 in Lecture Notes in Computer Science, pages 278–289, Berlin-Heidelberg-New York, 1989. Springer.

Index

alph(t) 10 alph(s) 24 alphinf(t) 10 alphinf(w) 10 AP(IR) 44 AP(Σ^{∞}) 44 AP(Σ^{∗}) 44 D(a) 10 D(A) 10 δ(r, u) 50 δ_{F} (q, u) 68 ∂_{a}, ∂_{A} 15 DRec(IR) 23, 26 E(S) 24 E_{s} 30 ≡_{L} 12, 18 η 18 φ 10 I(a) 10 I(A) 10 Inf(A), IR_{A} 20 inf_{a}(r) 54 inf(q, u) 63

[L] 64 max(t) 10 IM_{s} 23 ν 50 ω-Iteration 10 \overrightarrow{L} 26 IP_{s} 24 Q_{A}, q_{A}, q_{D(a)} 14 R 30 IR(Σ, D) 10 c−Rat(IR) 20 R_{L} 12 Rec(M) 11 Rec(IR) 18 R_{A}(t) 50, 54 ρ 50 SF(IM) 43 SF(IR) 43 SF(Σ^{∞}) 44 SF(Σ^{∗}) 44 Σ^{ω} 10 Σ^{∞} 10 Synt(L) 12 t[a, n] 54 τ(q, v) 63 U_{a}(t) 54 U_{i}(t) 54 X_{s}, P_{s} 44 ⊓ 10 ⊔Y 10 ∩ 10 ≤_{R} 30

→^{a,t} 54

abgeschlossene Sprache 61 abgeschlossene Tafel 64 Abhängigkeitsalphabet 9 Abhängigkeitsgraph 9 Abhängigkeitsrelation D 9 Ablauf 50 aperiodisch 44 asynchrone Abbildung 15 asynchroner Automat 13 asynchron-zellulärer Automat 14

Büchi-Akzeptanz 19

c-rationale Ausdrücke 20

D-Shuffle 45 deterministische reelle Spursprachen,

DRec(IR) 26

erkennbare reelle Spursprachen, Rec(IR)

18 erkennender Homomorphismus 11, 17

Faktorisierung 17 Fortschrittsmaß 56

gerichtete Menge 26 globaler Übergang 14

Halbordnung ≤ 30

I-Diamant Eigenschaft 12 I-Diamant 61 idempotente Elemente, E(S) 24

konjugiert 24

Levi Lemma 26 Logik 1. Stufe 43

M-Automat 11 Methode des Fortschrittsmaßes 49 minimaler Automat 12 monadische Logik 2. Stufe 21 Monoid endlicher Spuren, IM(Σ, D) 9 Monoid (un)endlicher Abhängigkeits-

graphen, G(Σ, D) 9 Muller-Akzeptanz 19

Petri-Netze (1–sicher, beschriftet) 13 Präfix-Ordnung ≤ 10 ∂_{a}-, ∂_{A}-Präfixe 15 Pseudo-Fortschrittsmaß 55

Ramsey-Argument 17 reduzierte Tafel 63

sternfreie Sprache 43

syntaktische Kongruenz 12, 17

syntaktisches Monoid 12 syntaktischer Morphismus 12

Theorem von McNaughton 23

Unabhängigkeitsrelation I 9

verallgemeinerte Büchi-Akzeptanz 40

Zeitmarkierung (time stamping) 50 Zielonka-Konstruktion 15 Anca Muscholl

Brühlbachweg 5 70565 Stuttgart

\underline{Lebenslauf}

12.1.1967  geboren in Bukarest, Rumänien
1973-1981  allgemeine Schule, Bukarest
1981-1984  Gymnasium N. Balcescu, Bukarest
1984-1986  Klenze-Gymnasium, München
1985, 1986  Bundessiegerin im Bundeswettbewerb Mathematik
1986  Abitur
1986 / 1988  Aufnahme in die Studienstiftung des Deutschen

Volkes

1986-1991  Studium der Informatik an der Technischen

Universität München

1991  Diplom in Informatik
seit 1991  wissenschaftliche Mitarbeiterin am Institut für

Informatik der Universität Stuttgart, Abteilung Theoretische Informatik

Stuttgart, April 1994