The Hybrid mu-Calculus

Ulrike SattlerUlrike Sattler, M. Y. VardiM. Y. Vardi

Datei:SattlerVardi-IJCAR.ps.gz

Download

Ulrike Sattler, M. Y. Vardi
The Hybrid mu-Calculus
In R. Goré and A. Leitsch and T. Nipkow, eds., Proceedings of the International Joint Conference on Automated Reasoning, volume 2083 of LNAI, 76-91, 2001. Springer

Details
Bibtex

KurzfassungAbstract
In the last years, several decision procedures for ExpTime-complete modal/description/dynamic logics were implemented and proved to behave well in practice. Due to its high expressive power, the full mu-calculus (including converse programs) is one of the ``queens of ExpTime modal/description/dynamic logics. However, it lacks two features important in many applications: nominals to refer to named individuals, and a universal program for the internalisation of general axioms. We present an ExpTime decision procedure for the full mu-Calculus extended with nominals and a universal program, thus creating a new, more expressive ``queen logic. The decision procedure is based on tree automata, and makes explicit the problems caused by nominals and how to overcome them. Roughly speaking, we show how to reason in a logic lacking the tree model property using techniques for logics with the tree model property. Hence the contribution of the paper is two-fold: we extend the choice of ExpTime logics an implementer can choose from, and we present a technique to reason in the presence of nominals.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ SattlerVardi-IJCAR,
  author = {U. {Sattler} and M. Y. {Vardi}},
  booktitle = {Proceedings of the International Joint Conference on Automated Reasoning},
  editor = {R. {Gor{\'e}} and A. {Leitsch} and T. {Nipkow}},
  pages = {76--91},
  publisher = {Springer Verlag},
  series = {LNAI},
  title = {The Hybrid mu-Calculus},
  volume = {2083},
  year = {2001},
}