No Cover Image

Book chapter 1243 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
first_indexed 2013-07-23T12:10:45Z
last_indexed 2018-02-09T04:44:35Z
id cronfa13714
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T15:18:42.4861737</datestamp><bib-version>v2</bib-version><id>13714</id><entry>2012-12-16</entry><title>On the complexity of parity games</title><swanseaauthors><author><sid>bf25e0b52fe7c11c473cc48d306073f7</sid><ORCID>0000-0001-9535-8053</ORCID><firstname>Faron</firstname><surname>Moller</surname><name>Faron Moller</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-12-16</date><deptcode>MACS</deptcode><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.</abstract><type>Book chapter</type><journal>Visions of Computer Science</journal><volume></volume><journalNumber></journalNumber><paginationStart>237</paginationStart><paginationEnd>247</paginationEnd><publisher>British Computer Society</publisher><placeOfPublication/><issnPrint/><issnElectronic/><keywords>parity games, model checking, bounded arithmetic, complexity</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2008</publishedYear><publishedDate>2008-12-31</publishedDate><doi/><url/><notes>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.</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T15:18:42.4861737</lastEdited><Created>2012-12-16T20:24:06.3539912</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Faron</firstname><surname>Moller</surname><orcid>0000-0001-9535-8053</orcid><order>1</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T15:18:42.4861737 v2 13714 2012-12-16 On the complexity of parity games bf25e0b52fe7c11c473cc48d306073f7 0000-0001-9535-8053 Faron Moller Faron Moller true false 2012-12-16 MACS 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. Book chapter Visions of Computer Science 237 247 British Computer Society parity games, model checking, bounded arithmetic, complexity 31 12 2008 2008-12-31 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. COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2013-10-17T15:18:42.4861737 2012-12-16T20:24:06.3539912 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Faron Moller 0000-0001-9535-8053 1
title On the complexity of parity games
spellingShingle On the complexity of parity games
Faron Moller
title_short On the complexity of parity games
title_full On the complexity of parity games
title_fullStr On the complexity of parity games
title_full_unstemmed On the complexity of parity games
title_sort On the complexity of parity games
author_id_str_mv bf25e0b52fe7c11c473cc48d306073f7
author_id_fullname_str_mv bf25e0b52fe7c11c473cc48d306073f7_***_Faron Moller
author Faron Moller
author2 Faron Moller
format Book chapter
container_title Visions of Computer Science
container_start_page 237
publishDate 2008
institution Swansea University
publisher British Computer Society
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2008-12-31T06:25:30Z
_version_ 1821385666858057728
score 11.048171

Similar Items