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

作者：Hague M^*; Ong C H L

来源：Information and Computation, 2011, 209(5): 799-821.

DOI：10.1016/j.ic.2010.12.004

• Modal mu-calculus
• Pushdown systems
• Parity games
• Winning regions
• Global model checking
• Saturation methods

We present an algorithm for computing directly the denotation of a modal mu-calculus formula chi over the configuration graph of a pushdown system. Our method gives the first extension of the saturation technique to the full modal mu-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.

• 出版日期2011-5