Polynomial-Time Under-Approximation of Winning Regions in Parity Games

File Description SizeFormat 
under-approximation-parity-game.pdfAccepted version690.16 kBAdobe PDFDownload
Title: Polynomial-Time Under-Approximation of Winning Regions in Parity Games
Author(s): Antonik, A
Charlton, N
Huth, M
Item Type: Journal Article
Abstract: We propose a pattern for designing algorithms that run in polynomial time by construction and under-approximate the winning regions of both players in parity games. This approximation is achieved by the interaction of finitely many aspects governed by a common ranking function, where the choice of aspects and ranking function instantiates the design pattern. Each aspect attempts to improve the under-approximation of winning regions or decrease the rank function by simplifying the structure of the parity game. Our design pattern is incremental as aspects may operate on the residual game of yet undecided nodes. We present several aspects and one higher-order transformation of our algorithms - based on efficient, static analyses - and illustrate the benefit of their interaction as well as their relative precision within pattern instantiations. Instantiations of our design pattern can be applied for local model checking and as preprocessors for algorithms whose worst-case running time is exponential. This design pattern and its aspects have already been implemented in [H. Wang. Framework for Under-Approximating Solutions of Parity Games in Polynomial Time. MEng Thesis, Department of Computing, Imperial College London, 78 pages, June 2007]. © 2008 Elsevier B.V. All rights reserved.
Publication Date: 2-Jan-2009
Citation: Electronic Notes in Theoretical Computer Science Vol.( 225 ) No.( ) pp 115 - 139
URI: http://hdl.handle.net/10044/1/5753
Publisher Link: http://dx.doi.org/10.1016/j.entcs.2008.12.070
DOI: 10.1016/j.entcs.2008.12.070
ISSN: 1571-0661
Publisher: Elsevier
Start Page: 115
End Page: 139
Copyright Statement: © 2008 Elsevier B.V. All rights reserved. NOTICE: this is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, VOL: 225, (2009) DOI:10.1016/j.entcs.2008.12.070
Volume: 225
Appears in Collections:Computing
Quantitative Analysis and Decision Science



Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons