Abstract
We present an ExpTime decision procedure for the full μ- Calculus (including converse programs) extended with nominals and a universal program, thus devising a new, highly expressive ExpTime 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. The contribution of the paper is two-fold: we extend the family of ExpTime logics, and we present a technique to reason in the presence of nominals.
Part of this work was carried out while the second author was visiting Rice University on a DAAD Grant.
Work partially supported by NSF grants CCR-9700061 and CCR-9988322
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
C. Areces, P. Blackburn, and M. Marx. The computational complexity of hybrid temporal logics. Logic Journal of the IGPL, 8(5), 2000.
F. Baader and B. Hollunder. A terminological knowledge representation system with complete inference algorithm. In Proc. of PDK-91, vol. 567 of LNAI. Springer-Verlag, 1991.
G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal μ-calculus. In Proc. of TACAS, vol. 1055 of LNCS. Springer-Verlag, 1996.
P. Blackburn. Nominal tense logic. Notre Dame Journal of Formal Logic, 34, 1993.
D. Calvanese, G. De Giacomo, and M. Lenzerini. Reasoning in expressive description logics with fixpoints based on automata on infinite trees. In Proc. of IJCAI’99, 1999.
D. Calvanese, G. De Giacomo, M. Lenzerini, D. Nardi, and R. Rosati. Description logic framework for information integration. In Proc. of KR-98, 1998.
D. Calvanese, M. Lenzerini, and D. Nardi. Description logics for conceptual data modeling. In Logics for Databases and Information Systems. Kluwer Academic Publisher, 1998.
E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Proc. of CAV’94, vol. 818 of LNCS, pages 415–427. Springer-Verlag, 1994.
G. De Giacomo and M. Lenzerini. Boosting the correspondence between description logics and propositional dynamic logics. In Proc. of AAAI-94, 1994.
G. De Giacomo and M. Lenzerini. Concept language with number restrictions and fixpoints, and its relationship with μ-calculus. In Proc. of ECAI-94, 1994.
G. De Giacomo and M. Lenzerini. Tbox and Abox reasoning in expressive description logics. In Proc. of KR-96. Morgan Kaufmann, 1996.
F. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages. In Proc. of KR-91. Morgan Kaufmann, 1991.
F. M. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages. Information and Computation, 134, 1997.
E. A. Emerson and C. S. Jutla. Tree automata, μ-calculus, and determinacy. In Proc. of FOCS-91. IEEE, 1991.
E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model checking for fragments of the μ-calculus. In Proc. of CAV’93, vol. 697 of LNCS. Springer-Verlag, 1993.
D. Fensel, I. Horrocks, F. van Harmelen, S. Decker, M. Erdmann, and M. Klein. OIL in a nutshell. In Proc. EKAW-2000, vol. 1937 of LNAI, 2000. Springer-Verlag.
K. Fine. In so many possible worlds. Notre Dame J. of Formal Logics, 13, 1972.
E. Franconi and U. Sattler. A data warehouse conceptual data model for multidimensional aggregation: a preliminary report. AI✻IA Notizie, 1, 1999.
V. Haarslev and R. Möller. Expressive abox reasoning with number restrictions, role hierarchies, and transitively closed roles. In Proc. of KR-00, 2000.
Gerard J. Holzmann. The spin model checker. IEEE Trans. on Software Engineering, 23(5), 1997.
I. Horrocks. Using an Expressive Description Logic: FaCT or Fiction? In Proc. Of KR-98, 1998.
I. Horrocks, U. Sattler, and S. Tobies. Practical reasoning for very expressive description logics. Logic Journal of the IGPL, 8(3), May 2000.
D. Kozen. Results on the propositional μ-calculus. In Proc. of ICALP’82, vol. 140 of LNCS. Springer-Verlag, 1982.
O. Kupferman and M. Y. Vardi. μ-calculus synthesis. In Proc. MFCS’00, LNCS. Springer-Verlag, 2000.
O. Kupferman and M.Y. Vardi. Weak alternating automata and tree automata emptiness. In Proc. of STOC-98, 1998.
H. Levesque and R. J. Brachman. Expressiveness and tractability in knowledge representation and reasoning. Computational Intelligence, 3, 1987.
D. E. Muller and P. E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54(1-2), 1987.
B. Nebel. Reasoning and Revision in Hybrid Representation Systems. LNAI. Springer-Verlag, 1990.
P. F. Patel-Schneider and I. Horrocks. DLP and FaCT. In Proc. TABLEAUX-99, vol. 1397 of LNAI. Springer-Verlag, 1999.
A. Prior. Past, Present and Future. Oxford University Press, 1967.
A. Rector and I. Horrocks. Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions. In Proc. of the AAAI Spring Symposium on Ontological Engineering. AAAI Press, 1997.
K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. of IJCAI-91, 1991.
K. Schild. Terminological cycles and the propositional μ-calculus. In Proc. Of KR-94, 1994. Morgan Kaufmann.
M. Schmidt-Schauβ and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48(1), 1991.
R. S. Streett and E. A. Emerson. An automata theoretic decision procedure for the propositional μ-calculus. Information and Computation, 81(3), 1989.
W. Thomas. Languages, automata, and logic. In Handbook of Formal Language Theory, vol 1. Springer-Verlag, 1997.
S. Tobies. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. of Artificial Intelligence Research, 12, 2000.
S. Tobies. PSPACE reasoning for graded modal logics. J. of Logic and Computation, 2001. To appear.
M. Y. Vardi. What makes modal logic so robustly decidable? In Descriptive Complexity and Finite Models, American Mathematical Society, 1997.
M. Y. Vardi. Reasoning about the past with two-way automata. In Proc. Of ICALP’98, vol. 1443 of LNCS, 1998. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Heidelberg
About this paper
Cite this paper
Sattler, U., Vardi, M.Y. (2001). The Hybrid μ-Calculus. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_7
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive