Satisfiability of a Spatial Logic with Tree Variables

Abstract : 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.
Type de document :
Communication dans un congrès
16th EACSL Annual Conference on Computer Science and Logic, Sep 2007, Lausanne, Switzerland. Springer Berlin / Heidelberg, 4646, pp.130-145, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74915-8_13〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00148462
Contributeur : Emmanuel Filiot <>
Soumis le : jeudi 12 juin 2008 - 16:05:23
Dernière modification le : lundi 13 février 2017 - 18:00:08
Document(s) archivé(s) le : mardi 21 septembre 2010 - 17:04:51

Fichier

tql-csl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Emmanuel Filiot, Jean-Marc Talbot, Sophie Tison. Satisfiability of a Spatial Logic with Tree Variables. 16th EACSL Annual Conference on Computer Science and Logic, Sep 2007, Lausanne, Switzerland. Springer Berlin / Heidelberg, 4646, pp.130-145, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74915-8_13〉. 〈inria-00148462v2〉

Partager

Métriques

Consultations de la notice

304

Téléchargements de fichiers

123