Complexity of hybrid logics over transitive frames

Martin Mundhenk, Thomas Schneider, Thomas Schwentick, Volker Weber

    Research output: Contribution to journalArticlepeer-review

    32 Downloads (Pure)


    This article examines the complexity of hybrid logics over transitive frames, transitive trees, and linear frames. We show that satisfiability over transitive frames for the hybrid language extended with the downarrow operator ← is NEXPTIME-complete. This is in contrast to undecidability over arbitrary frames (Areces et al. (1999) [2]). We also show that adding the @ operator or the past modality leads to undecidability over transitive frames. This is again in contrast to the case of transitive trees and linear frames, where we show these languages to be nonelementarily decidable. Furthermore, we establish 2EXPTIME and EXPTIME upper bounds for satisfiability over transitive frames and transitive trees, respectively, for the hybrid Until/Since language and complement them with an EXPTIME lower bound for the modal Until language. © 2010 Elsevier B.V.
    Original languageEnglish
    Pages (from-to)422-440
    Number of pages18
    JournalJournal of Applied Logic
    Issue number4
    Publication statusPublished - Dec 2010


    • Complexity
    • Decidability
    • Hybrid logic
    • Satisfiability


    Dive into the research topics of 'Complexity of hybrid logics over transitive frames'. Together they form a unique fingerprint.

    Cite this