Citations of:
The computational complexity of hybrid temporal logics
Logic Journal of the IGPL 8 (5):653679 (2000)
Add citations
You must login to add citations.


We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2variable fragment of firstorder logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into firstorder logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) 









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 polynomialtime solvable from PSPACEcomplete cases, and for satisfiability, we exhibit cases complete for NP, PS pace , NE xp T ime , and even (...) 



The paper studies the logic TL(NBox+wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Boxw (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+wC), so we prove that TL(NBox+wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced (...) 

This is an extended version of the lectures given during the 12thConference on Applications of Logic in Philosophy and in the Foundationsof Mathematics in Szklarska Poręba. It contains a surveyof modal hybrid logic, one of the branches of contemporary modal logic. Inthe ﬁrst part a variety of hybrid languages and logics is presented with adiscussion of expressivity matters. The second part is devoted to thoroughexposition of proof methods for hybrid logics. The main point is to showthat application of hybrid logics (...) 

In a previous work we introduced the algorithm \SQEMA\ for computing firstorder equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) 

We study hybrid logics in topological semantics. We prove that hybrid logics of separation axioms are complete with respect to certain classes of finite topological models. This characterisation allows us to obtain several further results. We prove that aforementioned logics are decidable and PSPACEcomplete, the logics of T 1 and T 2 coincide, the logic of T 1 is complete with respect to two concrete structures: the Cantor space and the rational numbers. 

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 (...) 

We prove ExpTimemembership of the satisfiability problem for loosely ∀guarded firstorder formulas with a bounded number of variables and an unbounded number of constants. Guarded fragments with constants are interesting by themselves and because of their connection to hybrid logic. 

Hybrid languages are expansions of propositional modal languages which can refer to worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work has focussed on a more constrained system called $\mathscr{H}$. We show in detail that $\mathscr{H}$ is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations and a syntactic characterization. The key result to emerge is that $\mathscr{H}$ corresponds to the fragment of firstorder logic which is invariant for generated (...) 

We investigate the expressive power of memory logics. These are modal logics extended with the possibility to store (or remove) the current node of evaluation in (or from) a memory, and to perform membership tests on the current memory. From this perspective, the hybrid logic (↓), for example, can be thought of as a particular case of a memory logic where the memory is an indexed list of elements of the domain. 



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 (...) 





We propose a logic for reasoning about metric spaces with the induced topologies. It combines the 'qualitative' interior and closure operators with 'quantitative' operators 'somewhere in the sphere of radius r.' including or excluding the boundary. We supply the logic with both the intended metric space semantics and a natural relational semantics, and show that the latter (i) provides finite partial representations of (in general) infinite metric models and (ii) reduces the standard '∈definitions' of closure and interior to simple constraints (...) 