Polynomial-time under-approximation of winning regions in parity games
File(s)
Published version
Author(s)
Antonik, Adam
Carhlton, Nathaniel
Huth, Michael
Type
Report
Abstract
We propose a pattern for designing algorithms that run in polynomial time by construction and underapproximate
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 pre-processors for
algorithms whose worst-case running time is exponential.
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 pre-processors for
algorithms whose worst-case running time is exponential.
Date Issued
2006-01-01
Citation
Departmental Technical Report: 06/12, 2006, pp.1-23
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
23
Journal / Book Title
Departmental Technical Report: 06/12
Copyright Statement
© 2006 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
06/12