Fabio Mogavero

Date: 17:00, Wednesday, February 1, 2017
Speaker: Fabio Mogavero
Venue: IST Austria

Mondi 2

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.
Posted in RiSE Seminar