Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userComplexity of Hybrid Logics over Transitive Frames
114
0
0.0
(
0
)
Added by
Thomas Schneider
Publication date
2008
fields
Informatics Engineering
and research's language is
English
Authors
Martin Mundhenk
Ask ChatGPT about the research
No Arabic abstract
This paper examines the complexity of hybrid logics over transitive frames, transitive trees, and linear frames. We show that satisfiability over transitive frames for the hybrid language extended with the downarrow operator is NEXPTIME-complete. This is in contrast to undecidability of satisfiability over arbitrary frames for this language (Areces, Blackburn, Marx 1999). It is also shown that adding the @ operator or the past modality leads to undecidability over transitive frames. This is again in contrast to the case of transitive trees and linear frames, where we show these languages to be nonelementarily decidable. Moreover, we establish 2EXPTIME and EXPTIME upper bounds for satisfiability over transitive frames and transitive trees, respectively, for the hybrid Until/Since language. An EXPTIME lower bound is shown to hold for the modal Until language over both frame classes.
rate research
Read More
In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Goedel translation from S4 into Intuitionistic Logic, the PSPACE- completeness of M-imply is drawn. The sub-formula principle for a deductive system for a logic L states that whenever F1,...,Fk proves A, there is a proof in which each formula occurrence is either a sub-formula of A or of some of Fi. In this work we extend Statman result and show that any propositional (possibly modal) structural logic satisfying a particular formulation of the sub-formula principle is in PSPACE. If the logic includes the minimal purely implicational logic then it is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME. We also show how our technique can be used to prove that any finitely many-valued logic has the set of its tautologies in PSPACE.
We tackle the issue of representing infinite sets of real- valued vectors. This paper introduces an operator for combining integer and real sets. Using this operator, we decompose three well-known logics extending Presburger with reals. Our decomposition splits a logic into two parts : one integer, and one decimal (i.e. on the interval [0,1]). We also give a basis for an implementation of our representation.
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control locations). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking over deterministic one-counter automata is PSPACE-complete with infinite and finite accepting runs. By constrast, we prove that model checking freeze LTL in which the until operator is restricted to the eventually operator over nondeterministic one-counter automata is undecidable even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for first-order logic with data equality tests restricted to two variables. This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for the two logics are decidable. Our results pave the way for model-checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines.
We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the logic is complete; in addition, has the finite model property, and again ADF. This argument can be iterated, and as an application we obtain the finite model property for PDL-like expansions of logics that ADF.
We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamps theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal alpha and a formula, we can decide in PSPACE whether the formula has a model over alpha. In order to show these results, we introduce a class of simple ordinal automata, as expressive as Buchi ordinal automata. The PSPACE upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
