Parity games are two-player infinite-duration games on numerically labeled

graphs, playing a crucial role in various fields of theoretical computer

science. Finding efficient algorithms to solve these games in practice is widely

acknowledged as a core problem in formal verification, as it leads, indeed, to

efficient solutions of the model-checking and satisfiability problems for

expressive temporal logics, e.g., the modal µCalculus. This problem has also an

intriguing status from a complexity theoretic viewpoint, since it belongs to the

class UPTime ∩ CoUPTime, and still open is the question whether it can be solved

in polynomial time. The solution of a parity game can be reduced to the problem

of identifying sets of positions of the game, called dominions, in each of which

a player can force a win by remaining in the set forever. In this talk, we

describe a novel technique to compute dominions, based on the idea of promoting

positions to higher priorities during the search for winning regions. The

proposed approaches have nice computational properties, exhibiting the best

space complexity among the currently known solutions. Experimental results on

both random games and benchmark families show that the technique is also very

effective in practice.

The talk is based on joint works with Massimo Benerecetti and Daniele Dell’Erba

of the Università degli Studi di Napoli Federico II.