Spiele auf Graphen

Aus Wikiludia
Wechseln zu: Navigation, Suche

Inhaltsverzeichnis

Einleitung

Wozu werden Spiele auf Graphen gebraucht?

In der Informatik werden Systeme häufig als Graphen modelliert.

Zustand = Knoten

Zustandsübergang = Kante

Reaktive Systeme reagieren auf Eingaben aus der Umgebung (Benutzereingaben, Messungen, etc.). In manchen Zuständen kann das System selbst entscheiden welcher der nächste Zustandsübergang sein soll \Rightarrow Spieler 1 (System) entscheidet. In manchen Zuständen ist der nächste Zustandsübergang von den Eingaben abhängig \Rightarrow Spieler 2 entscheidet.

Wichtige Begriffe

Als erstes werden folgende Begriffe definiert:

Graph: Ein Graph G\!\, besteht aus einer Menge V\!\, von Knoten, und einer Menge E\!\, von Kanten.

Pfad: Ein Pfad im Graphen G=(V,E)\!\, ist eine Folge von Kanten der Form (q_n, q_{n+1})_{n\in \mathbb{N}}.

Endknoten (= Senke): Ein Endknoten ist der letzte Knoten, der keinen Nachfolger mehr hat.

Spiele auf Graphen

Definition

Ein Spiel auf Graphen G=(V,E)\!\, ist ein Tupel S=(N,G,v_0 \in V,P,(u_i ) ), mit:

  • N\!\, - Menge der Spieler
  • v_0\!\, - Anfangsknoten
  • P:V \rightarrow N - Spielerfunktion
  • u_i\!\,, für i \in N - Nutzenfunktion von Spieler i\!\,


Das Spiel fängt in v_0\!\, zu einem Endknoten, oder ein unendlicher Pfad, der in v_0\!\, beginnt.

  • Sei Z\!\, die Menge aller endlichen Pfade von v_0\!\, zu einem Endknoten
  • Sei Y\!\, die Menge aller unendlichen Pfade von v_0\!\,.

W=Z \cup U ist die Menge aller Spielverläufe. Daraus folgt, dass u_i\!\,, für jedes i \in N, eine Funktion von W\!\, auf \mathbb{R} ist.


Sei G=(V,E)\!\, ein gerichteter Graph. Wir können die Pfade in G\!\, folgendermaßen betrachten:

V^*\!\,=Menge aller Pfade (v_0 v_1 v_2 \dots v_n) von v\!\, zu einem Endknoten, mit:

  • v_0=v\!\,
  • v_n\!\, ein Endknoten
  • (v_j,v_{j+1}) \in E  \forall 0  \leq j < n.

V^w\!\,= Menge aller unendlichen Pfade (v_0 v_1 v_2 \dots) von v\!\,, mit:

  • v_0=v\!\,
  • (v_j,v_{j+1})\in E  \forall 0 \leq j.

Gewinnbedingungen

Definition

In Gewinner-Verlierer-Spiele gibt es manchmal Gewinnbedingungen.

Eine Gewinnbedingung auf G=(V,E)\!\, mit Anfangsknoten v_0\!\, ist eine Teilmenge aller Pfade von v_0\!\, zu einem Endknoten und aller unendlichen Pfade von v_0\!\,.

Die Gewinnbedingung des ersten Spielers ist eine Menge aller Pfade wo er gewinnt.


Was für Gewinnbedingungen werden gebraucht?

Diese Frage lässt sich nicht eindeutig beantworten.

Die Umgebung kann das System nie dazu zwingen, ein Fehlerzustand einzunehmen. (Safety condition)

Das System kann immer wieder einen gewissen Zustand erreichen.(Liveness condition)

Model Checking ist eine große Unterdisziplin in der Informatik. Die beschäftigt sich damit, festzustellen ob Systeme solche Eigenschaften haben.

Viele wichtige Probleme in Model Checking lassen sich als Spiele beschreiben.


Einschränkung der Gewinnbedingung

Da nicht alle Gewinnbedingungen zu determinierten Spielen führen, werden diese eingeschränkt.

Definition

Eine Nutzenfunktion u_i\!\, in einem Spiel auf G=(V,E)\!\, ist ohne Erinnerung auf endlichen Pfaden, wenn für jeden Endknoten v \in V\!\, gilt, dass u_i (wv)=u_i (w'v)\!\,für alle wv,w'v \in W\!\,.

Für einen unendlichen Pfad \pi=v_0,v_1,\dots \in V^w\!\, wird inf (\pi)={v \in V | v = v_i}\!\, für unendlich viele i definiert.

Nebenbedingung: Wenn inf(w\pi)=inf(\pi')\!\, für zwei unendliche Pfade in V^w\!\,, dann gilt inf(\pi)=inf(\pi')\!\,.

Eine Nutzenfunktion u_i\!\, in einem Spiel auf G=(V,E)\!\, ist ohne Erinnerung auf unendlichen Pfade, wenn u_i (\pi)=u_i (\pi')\!\, für alle unendliche Pfade \pi,\pi'\in W mit inf(\pi)=inf(\pi')\!\,.

Eine Nutzenfunktion ist ohne Erinnerung, wenn sie für endliche und unendliche Pfade in W\!\, ohne Erinnerung ist. Solche Nutzenfunktionen werden weiter benutzt.


Positionelle Strategien

Sei S\!\, ein Spiel auf G=(V,E)\!\, mit Anfangsknoten v_0\!\,.

Definition Eine Strategie für Spieler i\!\, in S\!\,, ist ein Funktion f_i\!\, die jedem Pfad wv\!\, in G\!\,, der mit v_0\!\, anfängt und mit v \in P^{(-1)} (i) endet, einen Knoten u\!\, zuordnet, mit (v,u)\in E.

Wenn v\!\, auf zwei verschiedene Wege erreicht wird, kann Strategie f_i\!\, also auch verschiedene Fortsetzungen wählen.

Eine Strategie f_i\!\, für Spieler i\!\, in S\!\, ist positional, wenn f_i (wv)=f_i (w'v)\!\, für alle w,w'\!\, und alle v \in P^(-1) (i).

Immer, wenn v\!\, erreicht wird, wählt f_i\!\, also dieselbe Fortsetzung. Der bisherige Spielverlauf spielt für die Wahl keine Rolle.


Finite Gewinnbedingungen

Definition Ein Gewinner-Verlierer-Spiel auf G=(V,E)\!\, hat eine finite Gewinnbedingung, wenn entweder Spieler 1 alle unendlichen Spielverläufe gewinnt oder Spieler 2 alle unendlichen Spielverläufe gewinnt.

Satz

Alle Gewinner-Verlierer-Spiele auf Graphen mit finiten Gewinnbedingungen sind determiniert. Der Gewinner hat eine erinnerungslose Gewinnstrategie.

Beweis

Schritt 1: Attraktoren werden definiert.

Sei S\!\, ein Spiel mit 2 Spielern auf G=(V,E)\!\,. Sei V_1=P^{(-1)} (1)\!\, und V_2=P^{(-1)} (2)\!\,. Sei U \subset V\!\,. Der i-te-Attraktor von U\!\, ist die Menge aller Knoten, von denen Spieler i den Spielverlauf in 0 oder mehr Schritte zu einem Knoten in U\!\, zwingen kann. U\!\, selbst ist Teilmenge von dem i-ten-Attraktor von U\!\,. Für den i-ten Attraktor von U\!\, wird attr_i (U)\!\, geschrieben.


Tatsache: Wenn Spieler 1 den Spielverlauf zu einem Knoten in attr_i (U)\!\, zwingen kann, kann er ihn auch zu einem Knoten in U\!\, zwingen.


Schritt 2:Beschreibung eines Algorithmus, der für jeden Knoten v\!\, berechnet, wer gewinnen würde, falls das Spiel in v\!\, anfangen würde.

Sei S\!\, ein Gewinner-Verlierer-Spiel auf G=(V,E)\!\, mit finiter Gewinnbedingung. Angenommen, Spieler 2 gewinnt alle unendlichen Spielverläufe. (Die Situation, wenn Spieler 1 die unendlichen Verläufe gewinnt ist analog.)

Spieler 1 kann nur gewinnen, indem er einen Endknoten erreicht, in der er gewinnt.

Sei U\!\, die Menge aller Endknoten wo Spieler 1 gewinnt. Berechnet werden attr_1 (U)\!\,, und eine positionelle Strategie, die Spieler 1 in den Knoten in attr_1 (U)\!\, verwenden kann.

Eine positionelle Strategie für Spieler i\!\, kann als eine ausgehende Kante aus jedem Knoten in P^{(-1)} (i)\!\, gesehen werden.

Algorithmus:

  • U \leftarrow alle Endknoten v\!\, wo Spieler 1 gewinnt
  • Y\leftarrow U
  • f_1 \leftarrow \emptyset
  • neue \leftarrow \emptyset
  • foreach v \in \frac{V}{Y}
  • if P(v)=1\!\,
  • if \exists u:u \in Y oder (v,u)\in E
  • neue \leftarrowneue \cup{v}\!\,
  • f_1 \leftarrow f_1 \cup {(v,u)}
  • else
  • if \forall u:(v,u)\in E \leftarrow u \in Y
  • neue \leftarrowneue \cup {v}
  • Y \leftarrow Y \cupneue
  • until neue \leftarrow \emptyset
  • return Y,f_1\!\,


Schritt 3:Beweis, dass der Algorithmus korrekt ist, und dass der Gewinner eine erinnerungslose Gewinnstrategie hat.

Als erstes wird bewiesen, dass wenn der Spielverlauf v \in Y erreicht hat, und Spieler 1 die (partielle) Strategie f_1\!\, spielt, wird der Spielverlauf in einem Knoten in U\!\, enden.

Angenommen, v\!\, wurde in Y\!\, in Iteration n\!\, von der While-Schleife eingefügt.

Induktionsanfang: n=0,v \in U\!\,.

Induktionsschritt: Wenn P(v)=1\!\, ist f_1 (v)=u\!\,, mit (v,u) \in E\!\, und u \in Y\!\, wurde in Iteration n-1\!\, hineingefügt. Laut Induktionsannahme endet der Spielverlauf in U\!\,.

Wenn P(v)=2\!\, ist u \in Y\!\, für alle u\!\, mit (v,u) \in E. Alle sind in Iterationen <n\!\, eingefügt worden. Nach v\!\, erreicht der Spielverlauf also einen Knoten u\!\, von dem er, laut Induktionsannahme, nach U\!\, weitergeht. Daraus folgt: wenn v_0\in Y(=attr_1 (U)), gewinnt Spieler 1 mit jeder positionellen Strategie, die f_1\!\, als Teilstrategie hat.

Was passiert wenn v_0 \in \frac{V}{Y}?

Sei f_2\!\, eine positionelle Strategie die für keinen Knoten außerhalb von Y\!\, einen Nachfolger in Y\!\, wählt. Wenn das Spiel in v_0\!\, anfängt, und der 2. Spieler die Strategie f_2\!\, spielt, wird nie ein Knoten in Y\!\, erreicht. Alle Endknoten in denen Spieler 1 gewinnt, gehören zu Y\!\,. Spieler 2 gewinnt alle unendlichen Spielverläufe. Also ist f_2\!\, eine Gewinnstrategie für Spieler 2.



Beispiele

Paritätsspiele

Paritätsspiele werden auf Graphen gespielt, die mit einer Paritätsfunktion \ c:V \rightarrow {1,...,k} versehen sind. Wir nehmen an dass der Graph G keine Senken hat. Sei \ \pi=v_1,v_2,v_3,... ein unendlicher Spielverlauf. Spieler 1 gewinnt, wenn \ \max(c(v)|v \in f(\pi)) gerade ist. Spieler 2 gewinnt, wenn \ \max(c(v)|v \in f(\pi)) ungerade ist.

Paritätsspiele sind also Gewinner-Verlierener-Spiele mit erinnerungslosen Gewinnbedingungen. Die Gewinnbedingungen sind nicht finit. Büchi-Spiele sind ein Spezialfall von Paritätsspielen.

Satz

(Emerson, Jutla 1988, Mostowski 1988). Paritätsspiele sind deterministisch. Der Gewinner hat eine erinnerungslose Gewinnstrategie.

Anwendungen

Model Checking: Wir wollen wissen, ob ein System eine gewisse Eigenschaft hat. Das System wird oft als so-genannte Kripke-Struktur modelliert. Die Eigenschaft wird in einer temporalen Logik ausgedrückt.

Häufig verwendete Logiken: LTL, CTL, CTL*, \ \mu - Kalkül. Tatsächlich kann alles, was in LTL, CTL, CTL* ausgedrückt werden kann, auch in dem \ \mu - Kalkül ausgedrückt werden.

Herauszufinden, ob eine Kripke-Struktur eine Formel in dem \ \mu- Kalkül erfüllt, ist polonomialzeit-äquivalent mit dem Berechnen des Gewinners in einem Paritätsspiel.


Muller Spiele

Ein Muller Spiel besthet aus einem Graphen \ G=(V,E), eine Spielerfunktion \ P, einen Anfangsknoten \ v_0 \in V und eine Menge \ F=(F_1,F_2,...,F_k) von teilmengen von \ V. Wir nehmen an, dass es keine Senken im \ G gibt. Spieler 1 gewinnt einen unendlichen Spielverlauf \ \pi=v_0 v_1 v_2... wenn \ \inf(\pi)=F_i für ein \ i \in (1,...,k) Spieler 2 gewinnt, wenn er kein \ i \in (1,...,k) gibt mit \ \inf(\pi)=F_i.

Muller Spiele sind Gewinner-Verlierer-Spiele. Die Gewinnbedingungen sind nicht finit. Paritätsspiele sind Muller – Spiele. Muller-Spiele sind determiniert, da die Gewinnbedingungen Borel-Mengen sind.


Der Gewinner in einem Muller-Spiel hat nicht notwendigerweise eine erinnerungslose Gewinnstrategie.


Beispiel

Muller-Spiele2.JPG

\ F=((v_1,v_2,v_3 ),(v_1,v_3 ))

Spieler 1 muss abwechselnd links und rechst gehen, um zu gewinnen. Wann hat der Gewinner in einem Muller-Spiel eine erinnerungslose Gewinnstrategie?


Der Satz von McNaughton

Definition. Die Gewinnmenge \ F=(F_1,F_2,...,F_k) hat ein Split, wenn es \ Q,R \subseteq V gibt, mit Entweder \ Q \sqcap R \in F aber \ Q \notin F und \ R \notin F , Oder \ Q \sqcap R \notin F aber \ Q \in F und \ R \in F .


Satz(McNaughton, 1993)

Wenn F kein Split hat, dann hat der Gewinner eine erinnerungslose Gewinnstrategie.

Wir werden diesen Satz mit Induktion auf \ |V| beweisen. Lemma. Wenn \ F kein Split hat, und \ V \in F , dann gibt es \ v \in V mit \ R \in F für jede Menge \ R mit \ v \in R.

Wir können annehmen, dass \ V \in F . Wenn nicht, tauchen wir die Rollen der Spieler, und setzen \ F=P(V)\setminus F


Induktionsanfang: Wenn \ |V|=1 genügt eine erinnerungslose Strategie offenbar.


Induktionsannahme: Sei \ n \ge 2 . In alle Muller-Spiele auf Graphen mit weniger als \ n Knoten, und eine Gewinnstrategie \ F ohne Split gibt es, für jeden möglichen Anfangsknoten, ein Spieler der einen erinnerungslosen Gewinnstrategie hat.


Induktionsschritt: Sei \ S ein Muller-Spiel auf \ G=(V,E) mit \ |V|=n und gewinnmenge \ F=(F_1,F_2,...,F_k) ohne Split. Wir nehmen an, dass \ V \in F (siehe oben). Laut dem Lemma von oben gibt es \ v \in V mit \ (R \sqcap V|v \in R) \sqcap F .

Sei \ V^'=V \setminus attr_1(v)  die Menge der Knoten, von denen Spieler 2 \ v für immer vermeiden kann. Dies entspricht ein Erreichbarkeitsspiel, und Spieler 2 kann eine erinnerungslose Strategie verwenden.


Lemma. Nehmen wir an, dass \ G=(V,E) keine Senken hat. Sei \ X \subseteq V . Das Komplement von \ attr_i(X), für \ i \in (1,2) hat keine Senken. Wir definieren jetzt ein Teilspiel \ S^' auf \ G^'=(V^',E^') ,der Teilgraph von \ G der durch \ V^' induziert wird. Die entsprechende Gewinnmenge \ F^' ist \ F \cup P(V^'). Da \ v \notin V^' haben wir \ |V| < n. Da \ F kein Split hat, hat auch \ F^' keins.

Also gibt es, laut Induktionsannahmen, für jeden Knoten Da \ v^' \in G^' ein Spieler, der eine erinnerungslose Gewinnstrategie von \ v^' \in S^' hat. Seien \ W_1^',W_2^' die Teilmenge von \ V^' von denen Spieler 1 bzw. Spieler 2 so eine Strategie hat.

Muller-Spiele1.JPG

Die Gewinnstrategie von Spieler 2 für den Knoten in \ W_2 funktioniert auch im ursprünglichen Spiel \ S, da Spieler 1 keine Kanten hat, die aus \ V^' hinaus führen.

Für Spieler 1 ist das anders.


Fall 1: Spieler 2 kann von \ v aus den Spielverlauf nicht in einem Schritt in \ W_2^' hineinzwingen. Dann hat Spieler 1 von allen Knoten in \ V \setminus W_2 eine erinnerungslose Gewinnstrategie: In Knoten in \ W_1^' Spielt er wie in \ S^'. In Knoten in \ attr_1(v) \setminus v Spielt er die (erinnerungslose) Attraktorstrategie. In \ v Spielt verwendet er (wenn er am Zug ist) eine Kante, die nicht in \ W_2^' hineinführt.

Also gewinnt Spieler 1 von allen Knoten in \ V \setminus W_2 und Spieler 2 von allen Knoten in \ W_2^'.


Fall2:Spieler 2 kann von \ v aus den Spielverlauf in einem Schritt in \ W_2^' hineinzwingen. Dann hat Spieler 2 eine erinnerungslose Gewinnstrategie von allen Knoten in \ attr_2(W_2^'). Sei \ Q=V \setminus attr_2(W_2^'). Sei \ S^Q das Teilspiel induziert (wie oben) von \ Q .

Wir haben \ w \in Q, und deshalb \ |Q| < n. Die Induktionsannahme kann also für \ S^Q eine erinnerungslose Gewinnstrategie haben. Spieler 2 hat keine Kanten von \ Q in \ V \setminus Q . Deshalb gewinnt die Strategie von Spieler 1 für die Kanten in \ W_1^Q auch in \ S. Also gewinnt Spieler 1 von \ W_1^Q und Spieler 2 von \ V \setminus W_1^Q.



Satz

Der Gewinner in einem Muller–Spiel hat immer eine Gewinnstrategie mit endlichem Speicher.

Beweisidee:

• Wir definieren LAR. (Latest Appearance Record)

• Wir reduzieren Muller-Spieler auf Paritätsspiele.

• Wir zeigen, dass der erinnerungslosen Gewinnstrategie im Paritätsspiele eine Gewinnstrategie mit endlichem Speicher im Muller-Spiel entspricht.


Sei V={A,B,C,D,E}

Knoten LAR

A ----- A B C D E

C ----- C A B D E

E ----- E C A B D

A ----- A E C B D

A ----- A E C B D

E ----- E A C B D

A ----- A E C B D


Intuition. Der aktuelle Knoten Wird zur ersten Stelle in der Liste geholt. Die alte Position des aktuellen Knoten wird markiert.

Diese Struktur wurde zum ersten Mal von McNaughton definiert, in 1965. Er hat sie „order vector“ genannt.

Die Name „Latest appearance record“ hat sie von Gurevich und Harrington in 1985 bekommen. Sie speichert die Knoten nach der Ordnung, in welcher sie zuletzt besucht wurden. Notation. Statt eines Strichs unter der markierten Position zu Zeichnen schreiben wir \ ((v_1,v_2,...,v_n ),i). D.h. ((A,B,C,D,E),2) statt ABCDE.


Idee:

Die Knoten von \ G^' sind die LARs von \ G.

\ (v,u) \in E^' wenn diese Kante eine korrekte LAR-Aktualisierung für \ G ist.


Die Reduktion Anfangsknoten. Sei \ V=(1,2,3,...,n, mit Anfangsknoten 1. Der Anfangsknoten in \ G^' ist dann \ ((1,2,3,...,n),1). Kanten. Wenn \ (i_1,i_m ) \in E, gibt es in \ E^' eine Kante von


\ ((i_1,i_2,...,i_{m-1},i_m,i_{m+1},...,i_n ),h)

Zu

\ ((i_m,i_1,i_2,...,i_{m-1},i_{m+1},...,i_n ),m)


Prioritäten. Wir definieren \ c:V1^' \rightarrow (1,2,...,2n):


\ c((i_1,i_2,...,i_h,...,i_n ),h)=\begin{cases} 2h, & (i_1,...,i_h) \in F \\ 2h - 1, & (i_1,...,i_h) \notin F  \end{cases}


Korrektheit der Reduktion:

Zu jedem unendlichen Pfad \ \pi in \ G korrespondiert genau ein unendlicher Pfad \ \pi^' in \ G^'.

Sei \ \pi ein unendlicher Pfad in \ G mit \ |\inf(\pi)=t|. Dann gibt es eine Zahl \ p, so dass für alle Knoten \ ((i_1,...,i_n),h) die nach mehr als \ p schritte auf \ \pi^' auftreten gilt, dass \ h \le t.

Ab diesen Punkt \ p auf \ \pi^' gilt für jeden Knoten \ ((i_1,...,i_n),h), dass \ ((i_1,...,i_t)= \inf(\pi)

Sei \ |\inf(\pi)=t|. Dann gibt es auf \ \pi^' unenlich viele Knoten \ ((i_1,...,i_n),h) mit \ h=t. Nehmen wir an, Pfad \ \pi in \ G ist gut für Spieler 1. D.h. \ \inf(\pi) \in F. Auf \ \pi^' werden Knoten \ ((i_1,...,i_n),h) mit \ h=| \inf(\pi)| und \ ((i_1,...,i_h)= \inf(\pi) unendlich oft besucht. Knoten mit \ h \ge |\inf(\pi)| werden nur endlich oft besucht.

Da \ \inf(\pi) \in F ist \ 2h die grösste Priorität die unendlich oft auf \ \pi^' vorkommt. Also gewinnt Spieler 1 \ \pi^'.

Nehmen wir jetzt an, Pfad \ \pi in \ G. ist gut für Spieler 2. D.h. \ \inf(\pi) \notin F. Auf \ \pi^' werden Knoten \ ((i_1,...,i_n),h) mit mit \ h=| \inf(\pi)| und ((i_1,...,i_h)= \inf(\pi)</math> unendlich oft besucht. Knoten mit \ h \ge |\inf(\pi)| werden nur endlich oft besucht.

Da \ \inf(\pi) \notin F ist \ 2h-1 die grösste Priorität die unendlich oft auf \ \pi^' vorkommt. Also gewinnt Spieler 2 \ \pi^'.


Strategien. Sei \ f_i:V^*V_i \rightarrow V eine Gewinnstrategie für Spieler \ i in \ S. Dann können wir eine Gewinnstrategie \ f_i^' für Spieler \ i in \ S^' folgendermaßen definieren:

Sei \ \pi^' ein endlicher Pfad in \ G^' der in \ ((i_1,...,i_n),h) endet, und sei \ \pi der entsprechende Pfad in \ G. Der Pfad \ \pi endet also in \ i_1. Sei \ f_i(\pi)=i_m. Dann setzen wir


\ f_i^'(\pi^')=((i_m,i_1,i_2,...,i_{m-1},i_{m+1},...,i_n ),m)



Beispiel

Muller-Spiele2.JPG

F=((A,C),(A,B,C)). Sei A der Anfangsknoten. Spieler 1 kann gewinnen, indem er abwechselnd links und rechts geht.


Knoten LAR

A ----- ABC

B ----- BAC

C ----- CBA

B ----- BCA

A ----- ABC

B ----- BAC

Büchi-Spiele

Definition

Ein Büchi-Spiel auf dem Graphen G=(V,E)\!\, (ohne Endknoten) mit Zielmenge F \subseteq V\!\,, ist ein Gewinner-Verlierer-Spiel in dem Spieler 1 gewinnt, wenn F\!\, unendlich oft eintritt. Ansonsten gewinnt der 2. Spieler.

Bemerkung: Diese Gewinnbedingung ist nicht endlich.

Sei attr_i^+(X)\!\, die Menge der Knoten von denen Spieler i\!\, den Verlauf ein oder mehrere Schritte zu einem Knoten in X\!\, zwingen kann.

Büchi-Spiel auf G=(V,E) mit Zielmenge F - Algorithmus

  • F^' \leftarrow F
  • U \leftarrow attr_1^* (F)
  •  while F^'\neq(F^'\cap U)
  • F^' \leftarrow F^'\cap U
  • U \leftarrow attr_1^+ (F^')
  • return U\!\,

Der Algorithmus berechnet die Menge U\!\, der Knoten, von denen Spieler 1 eine Gewinnstrategie hat. Wenn der Anfangsknoten zu U\!\, gehört, dann gewinnt der 1. Spieler. Sonst gewinnt Spieler 2.

Spieler 1 hat eine erinnerungslose Strategie, um von den Knoten in U\!\, immer wieder zu einem Knoten in U \cap F\!\, zurückzukehren.

Korrektheit des Algorithmus:

Lemma:

Wenn der Anfangsknoten v_0\!\, nicht zu U\!\, gehört, hat Spieler 2 eine erinnerungslose Gewinnstrategie.

Beweis:

Wir zeigen, dass Spieler 2 eine erinnerungslose Strategie f_2\!\, hat, die von allen Knoten in  \frac{V}{U} gewinnt.

Jeder dieser Knoten ist in einem Durchlauf von der While\!\,-Schleife aussortiert worden (das, was vor dem ersten Durchlauf passiert, zählen wir als Durchlauf 0).

Sei U_i\!\, die Menge der Knoten die nach Durchlauf i\!\, von der Schleife zu U\!\, gehörten, und F_i\!\, die Knoten die nach Durchlauf i\!\, zu F\!\, gehörten.

Sei R_i \frac{V}{U_i}.

Induktionsanfang

Betrachte v \in R_0\!\,.

  • Wenn P(v)=1\!\, gilt u \in \frac{R_0}{F} für alle u\!\, mit (v,u)\in E\!\,.
  • Wenn P(v)=2\!\, gibt es ein u \in \frac{R_0}{F} mit (v,u)\in E\!\,.

Also hat Spieler 2 in den Knoten von R_0\!\, eine erinnerungslose Strategie, die garantiert, dass R_0\!\, nie mehr verlassen wird und dass F\!\, höchstens einmal besucht wird.

Induktionsschritt:

Nehmen wir an,  v \in \frac {R_i}{R_{(i-1)}}.

Laut Induktionsannahmen hat Spieler 2 eine gewinnende Teilstrategie für den Knoten in R_{(i-1)}\!\,.

Knoten v\!\, gehört nicht zu attr_1^+ (F_i)\!\,.

  • Wenn P(v)=1\!\, gilt  u\in \frac{R_i}{F} für alle u\!\, mit (v,u)\in E\!\,.
  • Wenn P(v)=2\!\, gibt es ein u \in \frac{R_i}{F} mit (v,u)\in E\!\,.

Wir nehmen die entsprechenden Kanten in f_2\!\, auf.

Wenn der Spielverlauf einen Knoten in  \frac {R_i}{R_{(i-1)}} erreicht, und Spieler 2 seine Teilstrategie f_2\!\, folgt, bleibt er entweder für immer in  \frac{R_i}{(F_i \cap R_{(i-1)})} oder er geht in R_{(i-1)}\!\, hinein nach einer endlichen Anzahl von Schritten. In beiden Fällen gewinnt Spieler 2.

Satz:

Der Büchi-Algorithmus kann so implementiert werden, dass die Laufzeit O(\mid V \mid ^2) ist.

Literatur

Ralf Küsters: Memoryless Determinacy of Parity Games.

Rene Mazala: Infinite Games.

E. Grädel, W. Thomas und T. Wilke (Eds.): Automata, Logics and Infinite Games: A guide to Current Research.

Meine Werkzeuge