Abstract
In this paper, we introduce decidable multimodal logics to describe and reason about navigation across object structures. The starting point of these navigation logics is the modelling of object structures as Kripke models that contain a family of deterministic accessibility relations; one for each pointer attribute. These pointer attributes are used in the logics both as first-order terms in equalities and as modal operators. To handle the ambiguities of pointer attributes the logics also cover a mechanism to bind logical variables to objects that are reachable by a pointer. The main result of this paper is a tableau construction for deciding the validity of formulas in the navigation logics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Areces, P. Blackburn, and M. Marx. A road-map on the complexity of hybrid logics. In J. Flum and M. Rodrýguez-Artalejo, editors, Computer Science Logic, Proceedings of CSL’99, volume 1683 of Lecture Notes in Computer Science, pages 307–321. Springer-Verlag, Heidelberg, 1999.
P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4:251–272, 1995.
P. Blackburn and J. Seligman. What are hybrid languages? In M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, editors, Advances in Modal Logic’96. CSLI Publications, Stanford, California, 1997.
F.S. de Boer. A WP-calculus for OO. In Proceedings of Foundations of Software Science and Computation Structures (FOSSACS’99), volume 1578 of Lecture Notes in Computer Science, pages 135–149, 1999.
R.M. van Eijk, F.S. de Boer, W. van der Hoek, and J.-J.Ch. Meyer. Modal logic with bounded quantification over worlds. Journal of Logic and Computation, 2001. To appear.
M. Fitting and R.L. Mendelsohn. First-Order Modal Logic. Kluwer Academic Publishers, Dordrecht, The Netherlands, 1998.
A. Hamie, J. Howse, and S. Kent. Navigation expressions in object-oriented modelling. In Fundamental Approaches to Software Engineering, Proceedings of FASE’98, volume 1382 of Lecture Notes in Computer Science, pages 123–137. Springer-Verlag, Heidelberg, 1998.
D. Harel. First-Order Dynamic Logic, volume 68 of Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 1979.
G.E. Hughes and M.J. Cresswell. An Introduction to Modal Logic. Methuen and Co. Ltd, London, 1968.
J. Rumbauch, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, Reading, Massachusetts, 1999.
M. Tzakova. Tableau calculi for hybrid logics. In N.V. Murray, editor, Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of TABLEAUX’99, volume 1617 of Lecture Notes in Artificial Intelligence, pages 278–292. Springer-Verlag, Heidelberg, 1999.
M.Y. Vardi. Why is modal logic so robustly decidable? In N. Immerman and P. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 149–184. AMS, 1997.
J.B. Warmer and A.G. Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading, Massachusetts, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Boer, F.S., van Eijk, R.M. (2001). Decidable Navigation Logics for Object Structures. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_23
Download citation
DOI: https://doi.org/10.1007/3-540-44802-0_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42554-0
Online ISBN: 978-3-540-44802-0
eBook Packages: Springer Book Archive