Complexity of Hybrid Logics over Transitive Frames

TL;DR

This paper investigates the computational complexity of various hybrid logics over transitive frames, revealing decidability boundaries and complexity bounds, and contrasting these with known results over other frame classes.

Contribution

It establishes new complexity results for hybrid logics over transitive frames, including NEXPTIME-completeness and upper bounds, and contrasts decidability with transitive trees and linear frames.

Findings

Satisfiability over transitive frames with downarrow is NEXPTIME-complete.

Adding @ operator or past modality causes undecidability over transitive frames.

Upper bounds of 2EXPTIME and EXPTIME are established for hybrid Until/Since over transitive frames and trees.

Abstract

This paper 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 (Areces, Blackburn, Marx 1999). 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.