Catálogo de publicaciones - libros

Let ${\cal A}$ be a partial algebra on a finite signature. We say that ${\cal A}$ has decidable query evaluation problem if there exists an algorithm that given a first order formula $\phi(\bar{x})$ and a tuple $\bar{a}$ from the domain of ${\cal A}$ decides whether or not $\phi(\bar{a})$ holds in ${\cal A}$ . Denote by $E({\cal A})$ the total algebra freely generated by ${\cal A}$ . We prove that if ${\cal A}$ has a decidable query evaluation problem then so does $E({\cal A})$ . In particular, the first order theory of $E({\cal A})$ is decidable. In addition, if ${\cal A}$ has elimination of quantifiers then so does $E({\cal A})$ extended by finitely many definable selector functions and tester predicates. Our proof is a refinement of the quantifier elimination procedure for free term algebras. As an application we show that any finitely presented term algebra has a decidable query evaluation problem. This extends the known result that the word problem for finitely presented term algebras is decidable.

We study the problem of the satisfiability of guarded formulas in models in which some distinguished binary symbols are interpreted as equivalence relations or as transitive relations. We sharpen the undecidability result for the two-variable guarded fragment with transitive relations by reducing the number of transitive relations to two. We prove that the satisfiability problem for the two-variable guarded fragment with two equivalence relations is 2EXPTIME-complete. We consider the guarded fragment with equivalence relations in guards and show that this variant is easily reducible to the variant with transitive relations in guards. However, in the case of two variables, the version with equivalence relations is easier: NEXPTIME-complete. Finally we show that the decidability results for the guarded fragment with either equivalence relations or transitive relations in guards cannot be generalized to the loosely guarded fragment.

We show that the modular decomposition of a countable graph can be defined from this graph, given with an enumeration of its set of vertices, by formulas of Monadic Second-Order logic. A second main result is the definition of a representation of modular decompositions by a low degree relational structures, also constructible by Monadic Second-Order formulas.

Hybrid logic refers to a group of logics lying between modal and first-order logic in which one can refer to individual states of the Kripke structure. In particular, the hybrid logic HL(@, ↓ ) is an appealing extension of modal logic that allows one to refer to a state by means of the given names and to dynamically create new names for a state. Unfortunately, as for the richer first-order logic, satisfiability for the hybrid logic HL(@, ↓ ) is undecidable and model checking for HL(@, ↓ ) is PSpace -complete. We carefully analyze these results and we isolate large fragments of HL(@, ↓ ) for which satisfiability is decidable and model checking is below PSpace .

We study the complexity of model-checking for the fixpoint extension of Hintikka and Sandu’s independence-friendly logic. We show that this logic captures ExpTime ; and by embedding PFP, we show that its combined complexity is ExpSpace -hard, and moreover the logic includes second order logic (on finite structures).

In this paper we study the properties of systems of bounded arithmetic capturing small complexity classes and state conditions sufficient for such systems to capture the corresponding complexity class tightly. Our class of systems of bounded arithmetic is the class of second-order systems with comprehension axiom for a syntactically restricted class of formulas Φ ⊂ Σ $_{\rm 1}^{B}$ based on a logic in the descriptive complexity setting. This work generalizes the results of [8] and [9]. We show that if the system 1) extends V _0 (second-order version of I Δ_0), 2) Δ_1-defines all functions with bitgraphs from Φ, and 3) proves witnessing for all theorems from Φ, then the class of Σ $_{\rm 1}^{B}$ -definable functions of the resulting system is exactly the class expressed by Φ in the descriptive complexity setting, provably in this system.

In [1] Bradfield found a link between finite differences formed by Σ $^{\rm 0}_{\rm 2}$ sets and the mu-arithmetic introduced by Lubarski [7]. We extend this approach into the transfinite: in allowing countable disjunctions we show that this kind of extended mu-calculus matches neatly to the transfinite difference hierarchy of Σ $^{\rm 0}_{\rm 2}$ sets. The difference hierarchy is intimately related to parity games. When passing to infinitely many priorities, it might not longer be true that there is a positional winning strategy. However, if such games are derived from the difference hierarchy, this property still holds true.

We propose a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. Our procedure checks whether a program execution of length n ends in an error (e.g. a NULL dereference) by testing if the weakest precondition of the error condition together with the initial condition of the program (e.g. program variable x points to a circular list) is satisfiable. We express error conditions as formulas in the 2-variable fragment of the Bernays-Schönfinkel class with equality. We show that this fragment is closed under computing weakest preconditions. We express the initial conditions by unary relations which are defined by monadic Datalog programs. Our main contribution is a small model theorem for the 2-variable fragment of the Bernays-Schönfinkel class extended with least fixed points expressible by certain monadic Datalog programs. The decidability of this extension of first-order logic gives us a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. In contrast to SAT-based bounded model checking, we do not bound the size of the heap a priori, but allow for pointer structures of arbitrary size. Thus, we are doing bounded model checking of infinite state transition systems.

In its many guises and variations, propositional dynamic logic (PDL) plays an important role in various areas of computer science such as databases, artificial intelligence, and computer linguistics. One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse. Although ICPDL has several interesting applications, its computational properties have never been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the monadic second order logic of infinite trees. Our result has applications in information logic, description logic, and epistemic logic. In particular, we solve a long-standing open problem in information logic. Another virtue of our approach is that it provides a decidability proof that is more transparent than existing ones for PDL with intersection (but without converse).

It has been proved by Niwiński and Walukiewicz that a deterministic tree language is either Π $_{\rm 1}^{\rm 1}$ -complete or it is on the level Π $_{\rm 3}^{\rm 0}$ of the Borel hierarchy, and that it can be decided effectively which of the two takes place. In this paper we show how to decide if the language recognized by a given deterministic tree automaton is on the Π $_{\rm 2}^{\rm 0}$ , the Σ $^{\rm 0}_{\rm 2}$ , or the Σ $^{\rm 0}_{\rm 3}$ level. Together with the previous results it gives a procedure calculating the exact position of a deterministic tree language in the topological hierarchy.