Paper Info
Title
Solving µ-Calculus Parity Games by Symbolic Planning
Abstract
This paper applies symbolic planning to solve parity games equivalent to μ-calculus model checking problems. Compared to explicit algorithms, state sets are compacted during the analysis. Given that diam(G)\mbox{\it diam}(G) is the diameter of the parity game graph G with node set V, for the alternation-free model checking problem with at most one fixpoint operator, the algorithm computes at most O(diam(G))O(\mbox{\it diam}(G)) partitioned images. For d alternating fixpoint operators, O(d ·diam(G) ·(\frac|</font >V|</font >+(d-</font >1)d-</font >1)d-</font >1)O(d \cdot \mbox{\it diam}(G) \cdot (\frac{|V|+(d-1)}{d-1})^{d-1}) partitioned images are required in the worst case. Practical models and properties stem from data-flow analysis, with problems transformed to parity game graphs, which are then compiled to a general game playing planner input.
Year
DOI
Venue
2008
10.1007/978-3-642-00431-5_2
MoChArt
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
26
4
Name
Order
Citations
PageRank
Marco Bakera1384.64
Stefan Edelkamp21557125.46
Peter Kissmann318113.93
Clemens D. Renner4232.25