The Computational Complexity of Hybrid Temporal Logics

C. Areces, P. Blackburn, and M. Marx. The Computational Complexity of Hybrid Temporal Logics. Logic Journal of the IGPL, 8(5):653–679, 2000.

Download

[pdf] 

Abstract

In their simplest form, hybrid languages are propositional modal languages which can refer to states. They were introduced by Arthur Prior, the inventor of tense logic, and played an important role in his work: because they make reference to specific times possible, they remove the most serious obstacle to developing modal approaches to temporal representation and reasoning. However very little is known about the computational complexity of hybrid temporal logics. In this paper we analyze the complexity of the satisfiability problem of a number of hybrid temporal logics: the basic hybrid language over transitive frames; nominal tense logic over transitive frames, strict total orders, and transitive trees; nominal Until logic; and referential interval logic. We discuss the effects of including nominals, the @ operator, the somewhere modality E, and the difference operator D. Adding nominals to tense logic leads for several frame–classes to an increase in complexity of the satisfiability problem from pspace to exptime. On transitive trees, however, the satisfiability problem for this language can be decided in pspace. Along the way we make a detour through hybrid propositional dynamic logic: we establish upper bounds for a number of temporal logics by generalizing results due to Passy and Tinchev [PT91] and De Giacomo [De 95]. We conclude with some remarks on the relevance of our results to description logic, and draw attention to the utility of the spypoint technique for proving upper and lower bounds.

BibTeX

@Article{Areces2000c,
  author =       "C. Areces and P. Blackburn and M. Marx",
  journal =      "Logic Journal of the IGPL",
  title =        "The Computational Complexity of Hybrid Temporal
                 Logics",
  year =         "2000",
  abstract =     "In their simplest form, hybrid languages are
                 propositional modal languages which can refer to
                 states. They were introduced by Arthur Prior, the
                 inventor of tense logic, and played an important role
                 in his work: because they make reference to specific
                 times possible, they remove the most serious obstacle
                 to developing modal approaches to temporal
                 representation and reasoning. However very little is
                 known about the computational complexity of hybrid
                 temporal logics. In this paper we analyze the
                 complexity of the satisfiability problem of a number of
                 hybrid temporal logics: the basic hybrid language over
                 transitive frames; nominal tense logic over transitive
                 frames, strict total orders, and transitive trees;
                 nominal Until logic; and referential interval logic. We
                 discuss the effects of including nominals, the @
                 operator, the somewhere modality E, and the difference
                 operator D. Adding nominals to tense logic leads for
                 several frame–classes to an increase in complexity of
                 the satisfiability problem from pspace to exptime. On
                 transitive trees, however, the satisfiability problem
                 for this language can be decided in pspace. Along the
                 way we make a detour through hybrid propositional
                 dynamic logic: we establish upper bounds for a number
                 of temporal logics by generalizing results due to Passy
                 and Tinchev [PT91] and De Giacomo [De 95]. We conclude
                 with some remarks on the relevance of our results to
                 description logic, and draw attention to the utility of
                 the spypoint technique for proving upper and lower
                 bounds.",
  number =       "5",
  pages =        "653--679",
  volume =       "8",
}