The Complexity of Hybrid Logics over Equivalence Relations

by    Martin Mundhenk, Thomas Schneider

Preprint series: 07-02, Reports on Computer Science

The paper is published: Proceedings of the workshop

03B45 Modal logic {For knowledge and belief see 03B42; for temporal logic see 03B44; for provability logic see also 03F45}

Abstract: This paper examines and classifies the computational complexity of model checking and satisfiability for hybrid logics over frames with equivalence relations. The considered languages contain all possible combinations of the downarrow binder, the existential binder, the satisfaction operator, and the global modality, ranging from the minimal hybrid language to very expressive languages. For model checking, we separate polynomial-time solvable from PSPACE-complete cases, and for satisfiability, we exhibit cases complete for NP, PSPACE, NEXPTIME, and even N2EXPTIME. Our analysis includes the versions without atomic propositions of all these languages.

Keywords: Computational Complexity, Downarrow Operator, Hybrid Logic, Modal Logic

Upload: 2007-05-14

Update: 2007 -05 -14

The author(s) agree, that this abstract may be stored as full text and distributed as such by abstracting services.