Résumé de rapport du LIF

Téléchargement / Download : pdf 284k , ps.gz 276k , bibtex

Abstract

We describe multitree automata and a related logic on multitrees. Multitrees are extensions of trees with both associative and associative-commutative symbols that may bear arbitrary numbers of sons. An originality of our approach is that transitions of an automaton are restricted using Presburger's constraints. The benefit of this extension is that we generalize, all together, automata with equality and disequalities constraints as well as counting constraints. This new class of automata appears very general as it may encompass hedge automata, a simple yet effective model for XML schemata, feature tree automata, automata with constraints between brothers and automata with arithmetical constraints. Moreover, the class of recognizable languages enjoys all the typical good properties of traditional regular languages: closure under boolean operations and composition by associative and associative-commutative operators, determinisation, decidability of the test for emptiness, ...

We apply our automata to query languages for XML-like documents and to automated inductive theorem proving based on rewriting, obtaining each time new results. Using a classical connection between logic and automata, we design a decidable logic for (multi)trees that can be used as a foundation for querying XML-like document. This proposition has the same flavour as a query language for semi-structured recently proposed by Cardelli and Ghelli. The same tree logic is used to yield decidable cases of inductive reducibility modulo associativity-commutativity, a key property in inductive theorem proving based on rewriting.

Keywords

Tree automata, constraints, modal logic, query languages, automated theorem proving.

Résumé

Nous décrivons des automates pour multiarbres et une logique correspondante sur les multiarbres et ses applications. Les multiarbres sont des extensions des arbres avec des symboles associatifs-commutatifs et associatifs. Une originalité de l'approche est l'utilisation de contraintes de Presburger sur les transitions des automates. Ceci permet de généraliser les contraintes d'égalité et les contraintes arithmétiques. Cette classe généralise les hedge automata qui sont un modèle des schémas pour XML, les feature-tree automata et les automates à contraintes entre frères. Les langages reconnus possèdent toutes les bonnes propriétés des langages réguliers: cloture par les opérations ensemblistes et aussi par composition associative-commutative, et le vide est décidable.

Nous appliquons cette classes aux langages de requête pour XML et aux preuves par induction en démonstration automatique. En faisant le lien usuel entre logique et automates (pour des multiarbres) nous obtenons une logique décidable qui peut être utilisée comme langage de requête pour des documents XML. Cette logique est similaire à celle proposée par Cardelli et Ghelli. La même logique est utilisée pour donner des cas décidables de la propriété de réductibilité inductive modulo AC, une propriété clef pour la preuve de théorèmes inductifs utilisant la réécriture.

Mots clés

Automates d'arbres, constraintes, logique modale, langage de requêtes, démonstration automatique.

Bibtex

@TECHREPORT{08-2002,
    AUTHOR	= {Denis Lugiez and Silvano Dal Zilio},
    TITLE	= {{Multitrees Automata, Presburger's Constraints and Tree Logics}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {08-2002},
    MONTH	= {June},
    YEAR	= {2002},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/08-2002.html},
}