A Road-map on Complexity for Hybrid Logics

C. Areces, P. Blackburn, and M. Marx. A Road-map on Complexity for Hybrid Logics. In J. Flum and M. Rodr\'iguez-Artalejo, editors, Computer Science Logic, number 1683 in LNCS, pp. 307–321, Springer, Madrid, Spain, 1999. Proceedings of the 8th Annual Conference of the EACSL, Madrid, September 1999.

Download

[pdf] 

Abstract

Hybrid languages are extended modal languages which can refer to (or even quantify over) states. Such languages are better behaved proof theoretically than ordinary modal languages for they internalize the apparatus of labeled deduction. Moreover, they arise naturally in a variety of applications, including description logic and temporal reason- ing. Thus it would be useful to have a map of their complexity-theoretic properties, and this paper provides one. Our work falls into two parts. We first examine the basic hybrid lan- guage and its multi-modal and tense logical cousins. We show that the basic hybrid language (and indeed, multi-modal hybrid languages) are no more complex than ordinary uni-modal logic: all have pspace-complete K-satisfiability problems. We then show that adding even one nominal to tense logic raises complexity from pspace to exptime. In the second part we turn to stronger hybrid languages in which it is possible to bind nom- inals. We prove a general expressivity result showing that even the weak form of binding offered by the \downarrow operator easily leads to undecidability.

BibTeX

@InCollection{Areces1999b,
  author =       "C. Areces and P. Blackburn and M. Marx",
  booktitle =    "Computer Science Logic",
  title =        "A Road-map on Complexity for Hybrid Logics",
  year =         "1999",
  abstract =     "Hybrid languages are extended modal languages which
                 can refer to (or even quantify over) states. Such
                 languages are better behaved proof theoretically than
                 ordinary modal languages for they internalize the
                 apparatus of labeled deduction. Moreover, they arise
                 naturally in a variety of applications, including
                 description logic and temporal reason- ing. Thus it
                 would be useful to have a map of their
                 complexity-theoretic properties, and this paper
                 provides one. Our work falls into two parts. We first
                 examine the basic hybrid lan- guage and its multi-modal
                 and tense logical cousins. We show that the basic
                 hybrid language (and indeed, multi-modal hybrid
                 languages) are no more complex than ordinary uni-modal
                 logic: all have pspace-complete K-satisfiability
                 problems. We then show that adding even one nominal to
                 tense logic raises complexity from pspace to exptime.
                 In the second part we turn to stronger hybrid languages
                 in which it is possible to bind nom- inals. We prove a
                 general expressivity result showing that even the weak
                 form of binding offered by the \downarrow operator
                 easily leads to undecidability.",
  address =      "Madrid, Spain",
  editor =       "J. Flum and M. Rodr{\'i}guez-Artalejo",
  note =         "Proceedings of the 8th Annual Conference of the EACSL,
                 Madrid, September 1999.",
  number =       "1683",
  pages =        "307--321",
  publisher =    "Springer",
  series =       "LNCS",
  ISBN =         "978-3-540-66536-6",
}