A Linear Time Special Case for MC Games

Article type: Research Article

Authors: Poranen, Timo | Nummenmaa, Jyrki

Affiliations: Dept. of Computer and Information Sciences, P.O. Box 607, FIN-33014 University of Tampere, Tampere, Finland

Abstract: MC games are infinite duration two-player games played on graphs. Deciding the winner in MC games is equivalent to the the modal mu-calculus model checking. In this article we provide a linear time algorithm for a class of MC games. We show that, if all cycles in each strongly connected component of the game graph have at least one common vertex, the winner can be found in linear time. Our results hold also for parity games, which are equivalent to MC games.

Keywords: model checking, MC games, parity games

Journal: Fundamenta Informaticae, vol. 50, no. 3-4, pp. 315-324, 2002