Static analysis of parity games: alternating reachability under parity
File(s)
Published version
Author(s)
Huth, Michael
Kuo, Jim Huan-Pu
Type
Report
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.
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-01-01
Citation
Departmental Technical Report: 15/4, 2015, pp.1-18
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
18
Journal / Book Title
Departmental Technical Report: 15/4
Copyright Statement
© 2015 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
15/4