An ACO-approach to Parity Games

Parity games are a notion of two player-games underlying among others
a solution to the model checking problem for the modal
mu-calculus. Various algorithms exist to decide if for a given parity
game a player has a winning strategy. 

Ant Colony Optimization (ACO) [2] is a computational approximation
paradigm inspired by food foraging by ants. Several algorithmically
challenging problems, like the travelling salesman problem, have quite
satisfactory solutions based on ACO.

In the proposed thesis work a solution with ACO for parity games will
be constructed and compared to other approaches like Zielonka's
recursive algorithm [3].

[1] E.A. Emerson, C.S. Jutla, A.P. Sistla, On model-checking fragments
of mu-calculus, Proc. CAV 1993, LNCS 697, 1993, pages 385-396

[2] M. Dorigo, M. Birattari, T. Stuetzle, Ant Colony Optimization:
Artificial ants as a computational intelligence technique, IEEE
Computational Intelligence Magazine, November 2006, pages 28-39

[3] W. Zielonka, Infinite games and finitely coloured graphs with
applications to automata on infinite trees, Theoretical Computer
Science 200, 1998, pages 135--183