Gra parzystości

Gry parzystości – gry pomiędzy dwoma graczami, toczone na skierowanym grafie etykietowanym $(V,E),$ gdzie $V$ to zbiór wierzchołków grafu, a $E$ to zbiór jego krawędzi.

Potencjalnie zbiór $V$ może być nieskończony. Gracze są z angielskiego nazywani Odd i Even. Każdy wierzchołek $v\in V$ jest wierzchołkiem jednego z graczy, to znaczy to ten gracz wykonuje z niego ruch. Dana jest funkcja $rank:V\to \mathbb {N} ,$ która każdemu wierzchołkowi przypisuje nieujemną liczbę całkowitą zwaną rankiem. Zakłada się, że obraz funkcji $rank$ jest skończony. Gra polega na tym, że gracze wykonują ruchy (zgodne z krawędziami ze zbioru $E$) na grafie gry, w danym momencie rusza się ten, który jest właścicielem danego wierzchołka. Jeśli w pewnym momencie któryś z graczy nie może wykonać ruchu, to przegrywa, natomiast jeśli gra toczy się w nieskończoność, to przyglądamy się liczbie $\limsup rank(v),$ czyli największemu rankowi, który pojawia się na wybranej ścieżce nieskończenie wiele razy. Jeśli liczba ta jest parzysta, to wygrywa gracz Even, a jeśli nieparzysta, to gracz Odd.

Własności

1. Gry parzystości są grami zdeterminowanymi, to znaczy dla każdej pozycji w grze istnieje gracz, który z tej pozycji ma strategię wygrywającą.

Rozwiązywanie gier

Poprzez rozwiązanie gry parzystości rozumiemy odpowiedzenie dla każdej pozycji który gracz posiada z tej pozycji strategię wygrywającą (wiemy, że taki istnieje dzięki determinacji gier parzystości) oraz wskazanie tej strategii. Dla gier parzystości wystarczy umieć wskazywać który gracz posiada strategię wygrywającą, a już umiemy wskazywać tę strategię.

Dotychczas nie jest znany wielomianowy algorytm rozwiązywania gier parzystości, najlepsze znane dziś algorytmy są podwykładnicze, jak na przykład.

Wiadomo natomiast, że dla gier parzystości z ograniczoną z góry liczbą ranków istnieją algorytmy wielomianowe rozwiązujące te gry, najlepsze osiągają złożoność czasową rzędu $n^{\frac {d}{2}},$ gdzie $d$ to ograniczenie na ilość różnych ranków.

Zastosowania

Najpoważniejszym powodem, dla którego interesujemy się grami parzystości, jest ich bliskie powiązanie z rachunkiem Mi. Rachunek Mi jest obecnie jednym z najlepszych formalizmów do automatycznej weryfikacji systemów za pomocą metody model checking. Potocznie mówiąc, gry parzystości są przydatne do automatycznego weryfikowania poprawności programów. Automatyczne weryfikowanie programów jest bardzo istotne, gdyż programista nie jest nigdy w stanie w stu procentach zapewnić poprawności napisanego kodu. Dlatego informatyka intensywnie pracuje nad tym problemem.