Abstract
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.
Original language | English |
---|---|
Title of host publication | HyLo |
Publication status | Published - 10 Jul 2010 |
Event | HyLo - Edinburgh, Scotland Duration: 1 Jan 1824 → … |
Conference
Conference | HyLo |
---|---|
City | Edinburgh, Scotland |
Period | 1/01/24 → … |
Keywords
- satisfiability
- modal logic
- complexity
- hybrid logic