An efficient translation from a modal μ-calculus 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
Submitted. 2016
Domaine :
Liste complète des métadonnées
Contributeur : Tyrex Equipe <>
Soumis le : vendredi 9 décembre 2016 - 11:00:10
Dernière modification le : mardi 13 décembre 2016 - 16:55:58


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


  • HAL Id : hal-01117830, version 2



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



Consultations de
la notice


Téléchargements du document