Algorithmic improvements for graph games

07/25/2012
Speaker(s) : Krishnendu Chatterjee (IST Austria)
 We consider two classical algorithms related to graph games and verification of probabilistic systems : Büchi games and Maximal End-Component (MEC) decomposition. In Büchi games, the first player aims at finding a strategy for reaching infinitely often a predefined set of vertices of the graph. Maximal End-Component decomposition, often used in probabilistic games, consists in finding a strongly connected component, which is also a trap for the second player's moves. We propose new algorithms which break the long standing best known bounds of O(nm), where n and m are respectively the number of vertices and edges of the underlying graph. Our algorithms are in O(n^2) for both problems, with another one in O(m^{1.5}) for MEC decomposition.