An efficient translation from a modal μ-calculus over finite tress with converse to tree automata

Louis Jachiet 1 Pierre Genevès 1 Nabil Layaïda 1
1 TYREX - Types and Reasoning for the Web
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We present a direct translation from a sub-logic of µ-calculus to non-deterministic binary automata of finite trees. The logic is an alternation-free modal µ-calculus, restricted to finite trees and where formulae are cycle-free. This logic is expressive enough to encode significant fragments of query languages (such as Regular XPath). The size of the generated automaton (the number of transitions) is bounded by 2^n where n is the size of a Fischer-Ladner closure of the formula. This is an improvement over previous translations in 2^{n^2} . We have implemented our translation. In practice, our prototype effectively decides static analysis problems that were beyond reach, such as the XPath containment problem with DTDs of significant size.
Type de document :
Pré-publication, Document de travail
2016
Domaine :
Liste complète des métadonnées


https://hal.inria.fr/hal-01117830
Contributeur : Tyrex Equipe <>
Soumis le : vendredi 9 décembre 2016 - 11:00:10
Dernière modification le : jeudi 18 mai 2017 - 11:22:39
Document(s) archivé(s) le : lundi 20 mars 2017 - 20:52:56

Fichier

aaai17 (1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01117830, version 2

Collections

Citation

Louis Jachiet, Pierre Genevès, Nabil Layaïda. An efficient translation from a modal μ-calculus over finite tress with converse to tree automata. 2016. <hal-01117830v2>

Partager

Métriques

Consultations de
la notice

132

Téléchargements du document

50