A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems

M. Hague, C. -H. L. Ong

We present an extension of an algorithm for computing directly the denotation of a mu-calculus formula X over the configuration graph of a pushdown system to allow backwards modali…