Book chapter 732 views
On the complexity of parity games
Visions of Computer Science, Pages: 237 - 247
Swansea University Author: Faron Moller
Parity games underlie the model checking problem for the modal mu-calculus, the complexity of which remains unresolved after decades of intensive research. In this paper we explore the possibility of employing Bounded Arithmetic to resolve this question, motivated by the fact that problems which are...
|Published in:||Visions of Computer Science|
British Computer Society
No Tags, Be the first to tag this record!
Parity games underlie the model checking problem for the modal mu-calculus, the complexity of which remains unresolved after decades of intensive research. In this paper we explore the possibility of employing Bounded Arithmetic to resolve this question, motivated by the fact that problems which are both NP and co-NP (such as the problem of solving parity games), and where the equivalence between their NP and co-NP description can be formulated and proved within a certain fragment of Bounded Arithmetic, necessarily admit a polynomial-time solution. While the problem remains unresolved by this paper, we do proposed a novel approach, and provide a demonstration that the problem of solving parity games lies in the class PLS of Polynomial Local Search problems. This result is based on a new proof of memoryless determinacy which can be formalised in Bounded Arithmetic. The approach we propose may offer a route to a polynomial-time solution. Alternatively, there may be scope in devising a reduction between the problem and some other problem which is hard with respect to PLS, thus making the discovery of a polynomial-time solution unlikely according to current wisdom.
The Visions of Computer Science Conference was an international conference with stringent refereeing criteria ensuring that only work recognised as internationally-excellent was accepted. The programme for the conference featured no fewer than seven Turing Award winners.The paper in question represents great originality in applying bounded arithmetic to a problem that has undergone intensive international study and attack since the early 1980s. As such, it clearly makes important contributions to the field at an international standard, contributing knowledge, ideas and techniques likely to have a lasting influence.
parity games, model checking, bounded arithmetic, complexity
Faculty of Science and Engineering