A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems
Formal Languages and Automata Theory
2010-07-01 v1 Logic in Computer Science
Abstract
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 modalities. Our method gives the first extension of the saturation technique to the full mu-calculus with backwards modalities.
Cite
@article{arxiv.1006.5906,
title = {A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems},
author = {M. Hague and C. -H. L. Ong},
journal= {arXiv preprint arXiv:1006.5906},
year = {2010}
}