The Complexity of Satisfiability for Fragments of Hybrid Logic-Part I

The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments including negation. For the monotone fragments, we are able to distinguish the easy from the hard cases, depending on the allowed set of operators.

• Publication year

  2009

• Venue

  International Symposium on Mathematical Foundations of Computer Science

• Publication date

  2009-06-08

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1016/j.jal.2010.08.001arXiv 0906.1489
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The Complexity of Satisfiability for Fragments of Hybrid Logic---Part II

  2010cited by this paper
• Terminological Cycles in a Description Logic with Existential Restrictions

  2009cited by this paper
• Model Checking CTL is Almost Always Inherently Sequential

  2009cited by this paper
• Branching-Time Logics Repeatedly Referring to States

  2009cited by this paper
• The Complexity of Hybrid Logics over Equivalence Relations

  2009cited by this paper
• The Complexity of Satisfiability for Fragments of CTL and CTL*

  2008cited by this paper
• The tractability of model checking for LTL: The good, the bad, and the ugly fragments

  2008cited by this paper
• Complexity of hybrid logics over transitive frames

  2008cited by this paper
• Complexity and succinctness issues for linear-time hybrid logics

  2008cited by this paper
• Hybrid Branching-Time Logics

  2007cited by this paper
• DL-Lite in the Light of First-Order Logic

  2007cited by this paper
• Polynomial Size Log Depth Circuits: Between NC1 and AC1

  2007cited by this paper
• The complexity of hybrid logics over restricted frame classes

  2007cited by this paper
• The Complexity of Generalized Satisfiability for Linear Temporal Logic

  2007cited by this paper
• Bounded-Variable Fragments of Hybrid Logics

  2007cited by this paper
• Generalized modal satisfiability

  2006influential reference
• Model checking hybrid logics (with an application to semistructured data)

  2006cited by this paper
• On the Complexity of Hybrid Logics with Binders

  2005cited by this paper
• I Computational Complexity

  2005cited by this paper
• Pushing the EL Envelope

  2005cited by this paper
• DL-Lite: Tractable Description Logics for Ontologies

  2005cited by this paper
• SIGACT news complexity theory column 48

  2005cited by this paper
• Hybrid logics on linear structures: expressivity and complexity

  2003cited by this paper
• Past is for free: on the complexity of verifying linear temporal properties with past

  2002cited by this paper
• Representation, Reasoning, and Relational Structures: a Hybrid Logic Manifesto

  2000cited by this paper
• The Computational Complexity of Hybrid Temporal Logics

  2000influential reference
• The Complexity of Poor Man's Logic

  1999cited by this paper
• Hybrid logic is the bounded fragment of first order logic.

  1999cited by this paper
• A Road-Map on Complexity for Hybrid Logics

  1999cited by this paper
• Introduction to Circuit Complexity

  1999cited by this paper
• Gap-Languages and Log-Time Complexity Classes

  1997cited by this paper
• Theories of computability

  1997cited by this paper
• Hierarchies of modal and temporal logics with reference pointers

  1996cited by this paper
• Counting quantifiers, successor relations, and logarithmic space

  1995cited by this paper
• Hybrid languages

  1995cited by this paper
• The Complexity of Existential Quantification in Concept Languages

  1992cited by this paper
• Half-order modal logic: how to prove real-time properties

  1990cited by this paper
• Satisfiability problems for propositional calculi

  1979cited by this paper
• The complexity of satisfiability problems

  1978cited by this paper
• The Computational Complexity of Provability in Systems of Modal Propositional Logic

  1977cited by this paper
• The two-valued iterative systems of mathematical logic

  1942influential reference
• Review: Emil L. Post, The Two-valued Iterative Systems of Mathematical Logic

  1941cited by this paper

• Modal Fragments

  2026cites this paper
• When Symmetry Yields NP-Hardness: Affine ML-SAT on S5 Frames

  2025cites this paper
• Ontology-Based AI Design Patterns and Constraints in Cancer Registry Data Validation

  2023cites this paper
• Model checking for hybrid branching-time logics

  2020cites this paper
• Parameterized complexity of abduction in Schaefer's framework

  2020cites this paper
• Parameterised Complexity of Abduction in Schaefer's Framework

  2019cites this paper
• Hybrid Branching-Time Logics

  2019cites this paper
• Parameterized complexity of decision problems in non-classical logics

  2018cites this paper
• Parametrised Complexity of Satisfiability in Temporal Logic

  2017cites this paper
• Model Checking for the Full Hybrid Computation Tree Logic

  2016cites this paper
• Applications of finite model theory : optimisation problems, hybrid modal logics and games

  2013cites this paper
• The expressibility of fragments of Hybrid Graph Logic on finite digraphs

  2013cites this paper
• Generalized Satisability for the Description LogicALC

  2013cites this paper
• Via della Vasca Navale , 79 00146 Roma , Italy Tableaux for multi-modal hybrid logic with binders , transitive relations and relation hierarchies

  2012cites this paper
• The Complexity of Monotone Hybrid Logics over Linear Frames and the Natural Numbers

  2012influential citation
• On the Complexity of Modal Logic Variants and their Fragments

  2011cites this paper
• THE EXPRESSIVE POWER OF MEMORY LOGICS

  2011cites this paper
• Generalized Satisfiability for the Description Logic ALC - (Extended Abstract)

  2011cites this paper
• Generalized Satisfiability for the Description Logic ALC

  2011cites this paper
• On the Complexity of Modal Logic Variants and their Fragments

  2011cites this paper
• The Complexity of Satisfiability for Fragments of Hybrid Logic---Part II

  2010influential citation
• On the applicability of Post's lattice

  2010cites this paper
• The Complexity of Satisfiability for Sub-Boolean Fragments of ALC

  2010cites this paper
• Islands of Tractability for Relational Constraints: Towards Dichotomy Results for the Description Logic EL

  2010cites this paper