Mundhenk, Schneider, Schwentick, Weber:
Complexity of Hybrid Logics over Transitive Frames.

4th Workshop on Methods for Modalities, 2005.

This paper examines the complexity of hybrid logics over transitive frames and transitive trees. We show that satisfiability over transitive frames for the hybrid language extended with downarrow is decidable, presenting a NEXPTIME decision procedure for this problem. This is in contrast to undecidability of satisfiability over arbitrary frames for this language [Areces, Blackburn, Marx 1999]. We also show that adding @ or the past modality leads to undecidability over transitive frames, but not over transitive trees, where the richest language is nonelementarily decidable. Moreover, we establish 2EXPTIME and EXPTIME upper bounds for satisfiability over transitive frames and transitive trees, respectively, for the hybrid Until/Since-language. An EXPTIME lower bound is shown to hold for the modal Until-language over both frame classes.