Complexity of Hybrid Logics over Transitive Frames

M Mundhenk, T Schneider, T Schwentick, V Weber

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Abstract

    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 of satisfiability over arbitrary frames for this language [2]. It is also shown 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. 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.
    Original languageEnglish
    Title of host publicationProc. 4th Int. Workshop Methods for Modalities (M4M)
    PublisherHumboldt-Universität zu Berlin
    Pages62-78
    Number of pages17
    Volume194
    Publication statusPublished - 2005
    Event4th Int. Workshop Methods for Modalities (M4M) -
    Duration: 1 Jan 1824 → …

    Publication series

    NameInformatik-Berichte

    Conference

    Conference4th Int. Workshop Methods for Modalities (M4M)
    Period1/01/24 → …

    Fingerprint

    Dive into the research topics of 'Complexity of Hybrid Logics over Transitive Frames'. Together they form a unique fingerprint.

    Cite this