The Complexity of Satisfiability for Fragments of Hybrid Logic---Part II
Arne Meier, M. Mundhenk, Thomas Schneider, Michael E. Thomas, Felix Weiß · Research Explorer (The University of Manchester) · 2010
Hybrid logic is an expressive specification language, but has anundecidable satisfiability problem in general. In this paper, we restrictthe set of Boolean operators to monotone operators (for instance conjunction and disjunction)and the underlying frames to commonly used acyclic frames, namely transitive trees, total transitivetrees, linear orders, and the natural numbers. We show that, under these restrictions,satisfiability is decidable for 16 fragments arising from different combinationsof modal and hybrid operators. More precisely, we categorise these fragments to bePSPACE-complete, NP-complete or tractable, where the latter cases are contained indetLOGCFL or complete for NC1.