Output details
11 - Computer Science and Informatics
University of Oxford
A saturation method for the modal μ-calculus over pushdown systems
<11>
We give the first extension of the saturation method---the implementation technique of choice for pushdown reachability checkers---to the mu-calculus. Starting from an initial automaton representing a configuration set, we perform a series of automaton manipulations which directly compute the denotation of a mu-formula by recursion over its syntax. Simple, direct and in contrast to previous solutions, our algorithm avoids an immediate exponential explosion, which is key to an efficient implementation. Extending results published in CONCUR09 and SPIN10, we show experimentally that our direct algorithm is more efficient than via a reduction to parity games.