The computational complexity of hybrid temporal logics.

*(English)*Zbl 0959.03011Summary: 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: becausc 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 S. Passy and T. Tinchev [Inf. Comput. 93, 263-332 (1991; Zbl 0732.03021)] and G. De Giacomo [Decidability of class-based knowledge representation formalisms. Ph. D. thesis, Univ. di Roma “La Sapienza” (1995)]. 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.

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 S. Passy and T. Tinchev [Inf. Comput. 93, 263-332 (1991; Zbl 0732.03021)] and G. De Giacomo [Decidability of class-based knowledge representation formalisms. Ph. D. thesis, Univ. di Roma “La Sapienza” (1995)]. 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.