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, PS pace , NE xp T ime , and even (...) N2E xp T ime . Our analysis includes the versions of all these languages without atomic propositions, and also complete frames. (shrink)

We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We present (...) a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms. (shrink)

Head-driven phrase structure grammar (HPSG) is one of the most prominent theories employed in deep parsing of natural language. Many linguistic theories are arguably best formalized in extensions of modal or dynamic logic (Keller, Feature logics, infinitary descriptions and grammar, 1993; Kracht, Linguistics Philos 18:401–458, 1995; Moss and Tiede, In: Blackburn, van Benthem, and Wolther (eds.) Handbook of modal logic, 2006), and HPSG seems to be no exception. Adequate extensions of dynamic logic have not been studied in detail, however; the (...) most important aspect is the reference to sets of substructures. In this paper, an adequate extension is identified, and some important results are established: Satisfiability is highly undecidable, and model checking is shown to be in EXPTIME and PSPACE-hard. A fragment with polynomial time model checking procedures is identified; it is shown to cover considerable fragments of HPSG. (shrink)

Graphs are among the most frequently used structures in Computer Science. Some of the properties that must be checked in many applications are connectivity, acyclicity and the Eulerian and Hamiltonian properties. In this work, we analyze how we can express these four properties with modal logics. This involves two issues: whether each of the modal languages under consideration has enough expressive power to describe these properties and how complex it is to use these logics to actually test whether a given (...) graph has some desired property. First, we show that these properties are not definable in a basic modal logic or in any bisimulation-invariant extension of it, like the modal μ-calculus. We then show that it is possible to express some of the above properties in a basic hybrid logic. Unfortunately, the Hamiltonian and Eulerian properties still cannot be efficiently checked. In a second attempt, we propose an extension of CTL* with nominals and show that the Hamiltonian property can be more efficiently checked in this logic than in the previous one. In a third attempt, we extend the basic hybrid logic with the ↓ operator and show that we can check the Hamiltonian property with optimal complexity in this logic. Finally, we tackle the Eulerian property in two different ways. First, we develop a generic method to express edge-related properties in hybrid logics and use it to express the Eulerian property. Second, we express a necessary and sufficient condition for the Eulerian property to hold using a graded modal logic. (shrink)

We prove that every first-order formula that is invariant under quasi-injective bisimulations is equivalent to a formula of the hybrid logic . Our proof uses a variation of the usual unravelling technique. We also briefly survey related results, and show in a standard way that it is undecidable whether a first-order formula is invariant under quasi-injective bisimulations.