Imperial College London
Portrait Picture

ProfessorMichaelHuth

Faculty of Engineering, Department of Computing

Head of the Department of Computing
 
 
 
//

Contact

 

m.huth Website

 
 
//

Location

 

Huxley 566Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Huth:2015:10.1007/978-3-319-27810-0_8,
author = {Huth, MRA and Huth and Piterman and Kuo, J},
doi = {10.1007/978-3-319-27810-0_8},
pages = {159--177},
publisher = {Springer},
title = {Static Analysis of Parity Games: Alternating Reachability Under Parity},
url = {http://dx.doi.org/10.1007/978-3-319-27810-0_8},
year = {2015}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - It is well understood that solving parity games is equivalent,up to polynomial time, to model checking of the modal mu-calculus. Itis a long-standing open problem whether solving parity games (or modelchecking modal mu-calculus formulas) can be done in polynomial time.A recent approach to studying this problem has been the design of partialsolvers, algorithms that run in polynomial time and that may only solveparts of a parity game. Although it was shown that such partial solverscan completely solve many practical benchmarks, the design of such partialsolvers was somewhat ad hoc, limiting a deeper understanding ofthe potential of that approach. We here mean to provide such robustfoundations for deeper analysis through a new form of game, alternatingreachability under parity. We prove the determinacy of these games anduse this determinacy to define, for each player, a monotone fixed pointover an ordered domain of height linear in the size of the parity gamesuch that all nodes in its greatest fixed point are won by said player inthe parity game. We show, through theoretical and experimental work,that such greatest fixed points and their computation leads to partialsolvers that run in polynomial time. These partial solvers are based onestablished principles of static analysis and are more effective than partialsolvers studied in extant work.
AU  - Huth,MRA
AU  - Huth
AU  - Piterman
AU  - Kuo,J
DO  - 10.1007/978-3-319-27810-0_8
EP  - 177
PB  - Springer
PY  - 2015///
SN  - 0302-9743
SP  - 159
TI  - Static Analysis of Parity Games: Alternating Reachability Under Parity
UR  - http://dx.doi.org/10.1007/978-3-319-27810-0_8
UR  - http://hdl.handle.net/10044/1/28804
ER  -
Download