Book chapter 1185 views
On the complexity of parity games
Visions of Computer Science, Pages: 237 - 247
Swansea University Author:
Faron Moller
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...
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!
|
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>SCS</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>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</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 SCS 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 Computer Science COLLEGE CODE SCS 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-31T03:15:40Z |
_version_ |
1763750277936054272 |
score |
11.024221 |