No Cover Image

Book chapter 732 views

On the complexity of parity games

Faron Moller Orcid Logo

Visions of Computer Science, Pages: 237 - 247

Swansea University Author: Faron Moller Orcid Logo

Abstract

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...

Full description

Published in: Visions of Computer Science
Published: British Computer Society 2008
URI: https://cronfa.swan.ac.uk/Record/cronfa13714
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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.
Item Description: 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.
Keywords: parity games, model checking, bounded arithmetic, complexity
College: Faculty of Science and Engineering
Start Page: 237
End Page: 247