A saturation method for the modal μ-calculus over pushdown systems

We present an algorithm for computing directly the denotation of a μ-calculus formula χ over the configuration graph of a pushdown system. Our method gives the first extension of the saturation technique to the full μ-calculus. Finite word automata are used to represent sets of pushdown configurations. Starting from an initial automaton, we perform a series of automaton manipulations which compute the denotation by recursion over the structure of the formula. We introduce notions of under-approximation (soundness) and over-approximation (completeness) that apply to automaton transitions rather than runs. Our algorithm is relatively simple and direct, and avoids an immediate exponential blow up. Finally, we show experimentally that the direct algorithm is more efficient than via a reduction to parity games.