We define memory-efficient certificates for μ-calculus model checking problems based on the well-known correspondence between μ-calculus model checking and winning certain parity games. Winning strategies can be independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning strategies are computed by fixpoint iteration following the naive semantics of μ-calculus. We instrument the usual fixpoint iteration of μ-calculus model checking so that it produces evidence in the form of a winning strategy; for a formula φ with fixed alternation depth, these winning strategies can be computed in polynomial time in |S| and in space O(|S|2|φ|2), where |S| is the size of the state space and |φ| the length of the formula φ. On the technical level our work yields a new, simpler, and immediate constructive proof of the correspondence between μ-calculus and parity games. A prototypical implementation of a μ-calculus model checker generating these certificates has been developed.
CITATION STYLE
Hofmann, M., Neukirchen, C., & Rueß, H. (2016). Certification for μ-calculus with winning strategies. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9641, pp. 111–128). Springer Verlag. https://doi.org/10.1007/978-3-319-32582-8_8
Mendeley helps you to discover research relevant for your work.