No Cover Image

Conference Paper/Proceeding/Abstract 1154 views

On the complexity of parity games

Arnold Beckmann Orcid Logo, Faron Moller

Visions of Computer Science — BCS International Academic Conference, Pages: 237 - 247

Swansea University Author: Arnold Beckmann Orcid Logo

Abstract

Parity games underlie the model checking problem for the modal μ-calculus, the complexity of which remains unresolved after more than two decades of intensive research. The community is split into those who believe this problem - which is known to be both in NP and coNP - has a polynomial-time solut...

Full description

Published in: Visions of Computer Science — BCS International Academic Conference
Published: BCS 2008
URI: https://cronfa.swan.ac.uk/Record/cronfa56
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:49:25Z
last_indexed 2018-02-09T04:27:22Z
id cronfa56
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T11:44:52.4948899</datestamp><bib-version>v2</bib-version><id>56</id><entry>2011-10-01</entry><title>On the complexity of parity games</title><swanseaauthors><author><sid>1439ebd690110a50a797b7ec78cca600</sid><ORCID>0000-0001-7958-5790</ORCID><firstname>Arnold</firstname><surname>Beckmann</surname><name>Arnold Beckmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2011-10-01</date><deptcode>SCS</deptcode><abstract>Parity games underlie the model checking problem for the modal &#x3BC;-calculus, the complexity of which remains unresolved after more than two decades of intensive research. The community is split into those who believe this problem - which is known to be both in NP and coNP - has a polynomial-time solution (without the assumption that P=NP) and those who believe that it does not. (A third, pessimistic, faction believes that the answer to this question will remain unknown in their lifetime.)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 coNP, and where the equivalence between their NP and coNP 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 another approach, and at the very least provide a modest refinement to the complexity of parity games (and in turn the &#x3BC;-calculus model checking problem): that they lie in the class 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>Conference Paper/Proceeding/Abstract</type><journal>Visions of Computer Science &#x2014; BCS International Academic Conference</journal><volume></volume><journalNumber></journalNumber><paginationStart>237</paginationStart><paginationEnd>247</paginationEnd><publisher>BCS</publisher><placeOfPublication/><issnPrint/><issnElectronic/><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2008</publishedYear><publishedDate>2008-12-31</publishedDate><doi/><url/><notes>&lt;p&gt;In Visions of Computer Science, Proc. BCS International Academic Research Conference, London, UK&lt;/p&gt;</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T11:44:52.4948899</lastEdited><Created>2011-10-01T00:00:00.0000000</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>Arnold</firstname><surname>Beckmann</surname><orcid>0000-0001-7958-5790</orcid><order>1</order></author><author><firstname>Faron</firstname><surname>Moller</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T11:44:52.4948899 v2 56 2011-10-01 On the complexity of parity games 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2011-10-01 SCS Parity games underlie the model checking problem for the modal μ-calculus, the complexity of which remains unresolved after more than two decades of intensive research. The community is split into those who believe this problem - which is known to be both in NP and coNP - has a polynomial-time solution (without the assumption that P=NP) and those who believe that it does not. (A third, pessimistic, faction believes that the answer to this question will remain unknown in their lifetime.)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 coNP, and where the equivalence between their NP and coNP 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 another approach, and at the very least provide a modest refinement to the complexity of parity games (and in turn the μ-calculus model checking problem): that they lie in the class 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. Conference Paper/Proceeding/Abstract Visions of Computer Science — BCS International Academic Conference 237 247 BCS 31 12 2008 2008-12-31 <p>In Visions of Computer Science, Proc. BCS International Academic Research Conference, London, UK</p> COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2013-10-17T11:44:52.4948899 2011-10-01T00:00:00.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Arnold Beckmann 0000-0001-7958-5790 1 Faron Moller 2
title On the complexity of parity games
spellingShingle On the complexity of parity games
Arnold Beckmann
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 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 Arnold Beckmann
Faron Moller
format Conference Paper/Proceeding/Abstract
container_title Visions of Computer Science — BCS International Academic Conference
container_start_page 237
publishDate 2008
institution Swansea University
publisher BCS
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 μ-calculus, the complexity of which remains unresolved after more than two decades of intensive research. The community is split into those who believe this problem - which is known to be both in NP and coNP - has a polynomial-time solution (without the assumption that P=NP) and those who believe that it does not. (A third, pessimistic, faction believes that the answer to this question will remain unknown in their lifetime.)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 coNP, and where the equivalence between their NP and coNP 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 another approach, and at the very least provide a modest refinement to the complexity of parity games (and in turn the μ-calculus model checking problem): that they lie in the class 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:03:15Z
_version_ 1763749496255152128
score 11.03559

Similar Items