Hybrid Logics on Linear Structures: Expressivity and Complexity

We investigate expressivity and complexity of hybrid logics on linear structures. Hybrid logics are an enrichment of modal logics with certain first-order features which are algorithmically well behaved. Therefore, they are well suited for the specification of certain properties of computational systems. We show that hybrid logics are more expressive than usual modal and temporal logics on linear structures, and exhibit a hierarchy of hybrid languages. We determine the complexities of the satisfiability problem for these languages and define an existential fragment of hybrid logic for which satisfiability is still NP-complete. Finally, we examine the linear time model checking problem for hybrid logics and its complexity.

Authors

• Massimo Franceschet
• Maarten de Rijke
• Bernd-Holger Schlingloff

Keywords

• Logic
• Mechanical factors
• Mathematical model
• Linear Structure
• Hybrid Logics
• Linear Model
• Model Checking
• Temporal Logic
• First-order Features
• Modal Logic
• General Structure
• State Model
• Hybrid Model
• Path Model
• First-order Logic
• Non-deterministic Polynomial-time
• NP-complete Problem
• Temporal Operators
• Propositional Logic
• Formula Means