Catálogo de publicaciones - libros

We compare the expressive power of a class of well-structured transition systems that includes relational automata, Petri nets, lossy channel systems, and constrained multiset rewriting systems. For each one of these models we study the class of languages generated by labelled transition systems describing their semantics. We consider here two types of accepting conditions: coverability and reachability of a given configuration. In both cases we obtain a strict hierarchy in which constrained multiset rewriting systems is the the most expressive model.

The operation → is a fundamental operation over finitary languages leading to -languages. Since the set of infinite words over a finite alphabet can be equipped with the usual Cantor topology, the question of the topological complexity of -powers of finitary languages naturally arises and has been posed by Niwinski [Niw90], Simonnet [Sim92] and Staiger [Sta97a] . It has been recently proved that for each integer  ≥ 1, there exist some -powers of context free languages which are -complete Borel sets,[Fin01], that there exists a context free language such that is analytic but not Borel,[Fin03] , and that there exists a finitary language such that is a Borel set of infinite rank, [Fin04]. But it was still unknown which could be the possible infinite Borel ranks of -powers.

We fill this gap here, proving the following very surprising result which shows that -powers exhibit a great topological complexity: for each non-null countable ordinal , there exist some -complete -powers, and some -complete -powers.

We investigate in this paper the spatial logic TQL for querying semi-structured data, represented as unranked ordered trees over an infinite alphabet. This logic consists of usual Boolean connectives, spatial connectives (derived from the constructors of a tree algebra), tree variables and a fixpoint operator for recursion. Motivated by XML-oriented tasks, we investigate the guarded TQL fragment. We prove that for closed formulas this fragment is MSO-complete. In presence of tree variables, this fragment is strictly more expressive than MSO as it allows for tree (dis)equality tests, i.e. testing whether two subtrees are isomorphic or not. We devise a new class of tree automata, called TAGED, which extends tree automata with global equality and disequality constraints. We show that the satisfiability problem for guarded TQL formulas reduces to emptiness of TAGED. Then, we focus on bounded TQL formulas: intuitively, a formula is bounded if for any tree, the number of its positions where a subtree is captured by a variable is bounded. We prove this fragment to correspond with a subclass of TAGED, called bounded TAGED, for which we prove emptiness to be decidable. This implies the decidability of the bounded guarded TQL fragment. Finally, we compare bounded TAGED to a fragment of MSO extended with subtree isomorphism tests.

We define regular expressions for unranked trees (actually, ordered sequences of unranked trees, called forests). These are compared to existing regular expressions for trees. On the negative side, our expressions have complementation, and do not define all regular languages. On the positive side, our expressions do not use variables, and have a syntax very similar to that of regular expressions for word languages.

We examine the expressive power of these expressions, especially from a logical point of view. The class of languages defined corresponds to a form of chain logic [5,6]. Furthermore, the star-free expressions coincide with first-order logic. Finally, we show that a concatenation hierarchy inside the expressions corresponds to the quantifier prefix hierarchy for first-order logic, generalizing a result of Thomas.

We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.

This paper considers logical formulas built on the single binary connector of implication and a finite number of variables. When the number of variables becomes large, we prove the following quantitative results: . It follows that .

Establishing local consistency is one of the main algorithmic techniques in temporal and spatial reasoning. In this area, one of the central questions for the various proposed temporal and spatial constraint languages is whether local consistency implies global consistency. Showing that a constraint language has this “local-to-global” property implies polynomial-time tractability of the constraint language, and has further pleasant algorithmic consequences.

In the present paper, we study the “local-to-global” property by making use of a recently established connection of this property with universal algebra. Specifically, the connection shows that this property is equivalent to the presence of a so-called quasi near-unanimity polymorphism of the constraint language. We obtain new algorithmic results and give very concise proofs of previously known theorems. Our results concern well-known and heavily studied formalisms such as the point algebra and its extensions, Allen’s interval algebra, and the spatial reasoning language RCC-5.

We study the enumeration complexity of the natural extension of acyclic conjunctive queries with disequalities. In this language, a number of -complete problems can be expressed. We first improve a previous result of Papadimitriou and Yannakakis by proving that such queries can be computed in time where is the structure, is the result set of the query and is a simple exponential in the size of the formula . A consequence of our method is that, in the general case, tuples of such queries can be enumerated with a linear delay between two tuples.

We then introduce a large subclass of acyclic formulas called and prove that the tuples of a query can be enumerated with a linear time precomputation and a constant delay between consecutive solutions. Moreover, under the hypothesis that the multiplication of two × boolean matrices cannot be done in time (), this leads to the following dichotomy for acyclic queries: either such a query is in or it cannot be enumerated with linear precomputation and constant delay. Furthermore we prove that testing whether an acyclic formula is in can be performed in polynomial time.

Finally, the notion of free-connex treewidth of a structure is defined. We show that for each query of free-connex treewidth bounded by some constant , enumeration of results can be done with precomputation steps and constant delay.

We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. One of our main results is completeness of the resulting calculus under some finiteness assumptions.

Calculi with explicit substitutions (ES) are widely used in different areas of computer science. Complex systems with ES were developed these last 15 years to capture the good computational behaviour of the original systems (with meta-level substitutions) they were implementing.

In this paper we first survey previous work in the domain by pointing out the motivations and challenges that guided the development of such calculi. Then we use very simple technology to establish a general theory of explicit substitutions for the lambda-calculus which enjoys fundamental properties such as simulation of one-step beta-reduction, confluence on metaterms, preservation of beta-strong normalisation, strong normalisation of typed terms and full composition. The calculus also admits a natural translation into Linear Logic’s proof-nets.