Igre parnosti

Opis projektnog zadatka:

Igre parnosti (engl. parity games) od iznimne su važnosti u teoriji automata na beskonačnim riječima, te predstavljaju osnovu za modeliranje nekih problema iz područja računalne verifikacije (primjerice model checking mu-racuna). Također su i od velikog značaja za teoriju računske složenosti, budući problem njihovog rješavanja predstavlja jedan od rijetkih problema za kojeg je poznato da se nalazi u presjeku klasa NP i Co-NP, a da još uvijek nije poznato postoji li za njega i algoritam polinomijalne složenosti. Cilj ovog projektnog zadatka jest implementirati neke od glavnih algoritama za rješavanje igara parnosti. Implementacija algoritama treba biti napravljena u jeziku C++ ili C#.

Prvi korak sastoji se od implementacije elementarnog algoritma eksponencijalne složenosti i njegovog recentnog subeksponencijalnog poboljšanja. Oba algoritma opisana su u M. Jurdzinski, M. Paterson, U. Zwick: A Deterministic Subexponential Algorithm for Solving Parity Games, SODA 2006.

U drugom koraku potrebno je implementirati tzv. strategy improvement algoritam, do danas još uvijek smatran najefikasnijim praktičnim algoritmom za rješavanje igara parnosti. Sam algoritam je opisan u J. Vöge, M. Jurdzinski: A Discrete Strategy Improvement Algorithm for Solving Parity Games, CAV 2000, dok se njegov pojednostavljeni prikaz i osnovne ideje za implementaciju mogu naći u D. Schmitz, J. Vöge: Implementation of a Strategy Improvement Algorithm for Finite-State Parity Games, CIAA 2000.

Ukoliko u izradi projektnog zadatka sudjeluju dva studenta, potrebno je još implementirati i algoritam baziran na tzv. mjerama napretka. Algoritam je originalno opisan u M. Jurdzinski: Small Progress Measures for Solving Parity Games, STACS 2000, dok se nešto raspisaniji opis može naći u H. Klauck: Algorithms for Parity Games, In: Automata, Logics, and Infinite Games, LNCS 2500, Springer, 2002, 107-129.


Projektni zadatak sastavio: Matko Botinčan.