Abstract
We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Andersen H.R. (1994) Model checking and boolean graphs. TCS, 126(1): 3–30
Areces, C. (2000). Logic engineering. The case of description and hybrid logics. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands.
Areces C., Blackburn P., Marx M. (2000) The computational complexity of hybrid temporal logics. Logic Journal of the IGPL, 8(5): 653–679
Areces, C., & ten Cate, B. (2006). Hybrid logics. In P. Blackburn, F. Wolter, & J. van Benthem (Eds.), Handbook of modal logics. Elsevier.
Bhat, G., & Cleaveland, R. (1996). Efficient local model-checking for fragments of the modal μ-calculus. In T. Margaria & B. Steffen (Eds.), Proceedings of the 2nd international workshop on tools and algorithms for construction and analysis of systems, TACAS’96, LNCS (Vol. 1055, pp. 107–126). Springer.
Bidoit N., Cerrito S., Thion V. (2004) A first step towards modeling semistructured data in hybrid multimodal logic. Journal of Applied Non-Classical Logics, 14(4): 447–475
Blackburn P. (1993) Modal logic and attribute value structures. In: Rijke M.(eds) Diamonds and defaults, synthese language library.. Kluwer Academic Publishers, Dordrecht, pp 19–65
Blackburn P., Tzakova M. (1998) Hybridizing concept languages. Annals of Math and AI, 24(1–4): 23–49
Bull R. (1970) An approach to tense logic. Theoria, 36: 282–300
Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J. (1992) Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2): 142–170
Cleaveland R. (1990) Tableau-based model checking in the propositional μ-calculus. Acta Informatica, 27(8): 725–748
Cleaveland, R., & Steffen, B. (1992). A linear-time model-checking algorithm for the alternation-free modal μ-calculus. In Proceedings of the 3rd international conference on computer aided verification, CAV’91, LNCS (Vol. 575, pp. 48–58). Springer.
Emerson E.A., Clarke E.M. (1982) Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3): 241–266
Emerson, E. A., & Lei, C. L. (1986). Efficient model checking in fragments of the propositional μ-calculus. In Symposium on Logic in Computer Science (pp. 267–278). IEEE, Washington, D.C., USA.
Franceschet, M., & de Rijke, M. (2003). Model checking for hybrid logics. In Proceedings of the 3rd international workshop methods for modalities, M4M-3.
Franceschet M., de Rijke M. (2006) Model checking hybrid logics (with an application to semistructured data). Journal of Applied Logic, 4(3): 279–304
Goranko V. (1996) Hierarchies of modal and temporal logics with reference pointers. Journal of Logic, Language, and Information, 5(1): 1–24
Jurdziński, M. (2000). Small progress measures for solving parity games. In H. Reichel & S. Tison (Eds.), Proceedings of the 17th annual symposium on theoretical aspects of computer science, STACS’00, LNCS (Vol. 1770, pp. 290–301). Springer.
Kozen D., Tiuryn J. (1990) Logics of programs. In: Leeuwen J.(eds) Handbook of theoretical computer science, vol B: Formal models and semantics, chap 14.. Elsevier and MIT Press, New York, pp 789–840
Passy S., Tinchev T. (1991) An essay in combinatory dynamic logic. Information and Computation, 93(2): 263–332
Queille, J. P., & Sifakis, J. (1982). Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th symposium on programming, LNCS (Vol. 137, pp. 337–371). Springer.
Stevens, P., & Stirling, C. (1998). Practical model-checking using games. In B. Steffen (Ed.), Proceedings of the 4th international conference on tools and algorithms for the construction and analysis of systems, TACAS’98, LNCS (Vol. 1384, pp. 85–101). Springer.
Stirling, C. (1995). Local model checking games. In Proceedings of the 6th conference on concurrency theory, CONCUR’95, LNCS (Vol. 962, pp. 1–11). Springer.
Stirling C., Walker D. (1991) Local model checking in the modal μ-calculus. Theoretical Computer Science, 89(1): 161–177
Tarski A. (1955) A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 5: 285–309
ten Cate, B. (2005). Model theory for extended modal languages. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands.
Vergauwen, B., & Lewi, J. (1993). A linear local model checking algorithm for CTL. In Lecture Notes in Computer Science (Vol. 715, pp. 447–461).
Vöge, J., & Jurdziński, M. (2000). A discrete strategy improvement algorithm for solving parity games. In Proceedings of the 12th international conference on computer aided verification, CAV’00, LNCS (Vol. 1855, pp. 202–215). Springer.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Lange, M. Model Checking for Hybrid Logic. J of Log Lang and Inf 18, 465–491 (2009). https://doi.org/10.1007/s10849-009-9088-7
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10849-009-9088-7