Static Analysis of Parity Games: Alternating Reachability Under Parity
File(s)
Accepted version
Author(s)
Huth, MRA
Huth
Piterman
Kuo, J
Type
Conference Paper
Abstract
It is well understood that solving parity games is equivalent,
up to polynomial time, to model checking of the modal mu-calculus. It
is a long-standing open problem whether solving parity games (or model
checking modal mu-calculus formulas) can be done in polynomial time.
A recent approach to studying this problem has been the design of partial
solvers, algorithms that run in polynomial time and that may only solve
parts of a parity game. Although it was shown that such partial solvers
can completely solve many practical benchmarks, the design of such partial
solvers was somewhat ad hoc, limiting a deeper understanding of
the potential of that approach. We here mean to provide such robust
foundations for deeper analysis through a new form of game, alternating
reachability under parity. We prove the determinacy of these games and
use this determinacy to define, for each player, a monotone fixed point
over an ordered domain of height linear in the size of the parity game
such that all nodes in its greatest fixed point are won by said player in
the parity game. We show, through theoretical and experimental work,
that such greatest fixed points and their computation leads to partial
solvers that run in polynomial time. These partial solvers are based on
established principles of static analysis and are more effective than partial
solvers studied in extant work.
up to polynomial time, to model checking of the modal mu-calculus. It
is a long-standing open problem whether solving parity games (or model
checking modal mu-calculus formulas) can be done in polynomial time.
A recent approach to studying this problem has been the design of partial
solvers, algorithms that run in polynomial time and that may only solve
parts of a parity game. Although it was shown that such partial solvers
can completely solve many practical benchmarks, the design of such partial
solvers was somewhat ad hoc, limiting a deeper understanding of
the potential of that approach. We here mean to provide such robust
foundations for deeper analysis through a new form of game, alternating
reachability under parity. We prove the determinacy of these games and
use this determinacy to define, for each player, a monotone fixed point
over an ordered domain of height linear in the size of the parity game
such that all nodes in its greatest fixed point are won by said player in
the parity game. We show, through theoretical and experimental work,
that such greatest fixed points and their computation leads to partial
solvers that run in polynomial time. These partial solvers are based on
established principles of static analysis and are more effective than partial
solvers studied in extant work.
Date Issued
2015-12-25
Date Acceptance
2015-11-15
Citation
Semantics, Logics, and Calculi, 2015, 9560, pp.159-177
ISBN
978-3-319-27809-4
ISSN
0302-9743
Publisher
Springer
Start Page
159
End Page
177
Journal / Book Title
Semantics, Logics, and Calculi
Volume
9560
Copyright Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-27810-0_8
Source
Semantics, Logics, and Calculi Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Subjects
Artificial Intelligence & Image Processing
08 Information And Computing Sciences
Publication Status
Published
Start Date
2016-01-08
Coverage Spatial
Denmark