A saturation method for the modal mu-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 configuratio...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2011
|