×

Clique-width and parity games. (English) Zbl 1179.68090

Duparc, Jacques (ed.) et al., Computer science logic. 21st international workshop, CSL 2007, 16th annual conference of the EACSL, Lausanne, Switzerland, September 11–15, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74914-1/pbk). Lecture Notes in Computer Science 4646, 54-68 (2007).
Summary: The question of the exact complexity of solving parity games is one of the major open problems in system verification, as it is equivalent to the problem of model-checking the modal \(\mu \)-calculus. The known upper bound is \(\text{NP}\cap \text{co-NP}\), but no polynomial algorithm is known. It was shown that on tree-like graphs (of bounded tree-width and DAG-width) a polynomial-time algorithm does exist. Here we present a polynomial-time algorithm for parity games on graphs of bounded clique-width (class of graphs containing e.g. complete bipartite graphs and cliques), thus completing the picture. This also extends the tree-width result, as graphs of bounded tree-width are a subclass of graphs of bounded clique-width. The algorithm works in a different way to the tree-width case and relies heavily on an interesting structural property of parity games.
For the entire collection see [Zbl 1122.68006].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q25 Analysis of algorithms and problem complexity
91A43 Games involving graphs
Full Text: DOI