A Linear Time Special Case for MC Games

• Autorzy: Poranen T. , Nummenmaa J.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

model checking; MC games; parity games

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2002
• Tom: Vol. 50, nr 3,4
• Strony: 315--324
• Opis fizyczny: bibliogr. 21 poz.

Twórcy

autor

Poranen T.

autor

Nummenmaa J.

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