Output details
11 - Computer Science and Informatics
University of Oxford
Article title
A saturation method for the modal μ-calculus over pushdown systems
Type
D - Journal article
Title of journal
Information and Computation
Article number
-
Volume number
209
Issue number
5
First page of article
799
ISSN of journal
0890-5401
Year of publication
2011
Number of additional authors
1
Additional information
<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.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
2
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
