On the Complexity of Hybrid Logics with Binders
Hybrid logic refers to a group of logics lying between modal and first-order logic in which one can refer to individual states of the Kripke structure. In particular, the hybrid logic HL(@, ↓ ) is an appealing extension of modal logic that allows one to refer to a state by means of the given names and to dynamically create new names for a state.
Unfortunately, as for the richer first-order logic, satisfiability for the hybrid logic HL(@, ↓ ) is undecidable and model checking for HL(@, ↓ ) is PSpace-complete. We carefully analyze these results and we isolate large fragments of HL(@, ↓ ) for which satisfiability is decidable and model checking is below PSpace.
KeywordsModel Check Modal Logic Kripke Structure Hybrid Logic Model Check Problem
Unable to display preview. Download preview PDF.
- 7.ten Cate, B.: Model theory for extended modal languages. PhD thesis, University of Amsterdam, ILLC Dissertation Series DS-2005-01 (2005)Google Scholar
- 8.Franceschet, M., de Rijke, M.: Model checking for hybrid logics (with an application to semistructured data). Journal of Applied Logics (2005) (to appear)Google Scholar
- 12.Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Guez-Artalejo, M.R. (eds.) Proceedings of the 8th Annual Conference of the EACSL, Madrid (1999)Google Scholar
- 13.Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of the International Workshop on Description Logics (2002)Google Scholar
- 16.ten Cate, B., Franceschet, M.: Guarded fragments with constants. Journal of Logic, Language, and Information (2005) (to appear)Google Scholar
- 18.ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. Technical Report PP-2005-02, ILLC, University of Amsterdam (2005)Google Scholar
- 19.Vardi, M.Y.: On the complexity of bounded-variable queries. In: Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pp. 266–276 (1995)Google Scholar
- 20.ten Cate, B., Franceschet, M.: Guarded fragments with constants. Technical Report PP-2004-32, ILLC, University of Amsterdam (2004)Google Scholar