An efficient translation from a modal μ-calculus over finite trees 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.
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01117830
Contributor : Tyrex Equipe <>
Submitted on : Friday, December 9, 2016 - 11:00:10 AM
Last modification on : Thursday, October 11, 2018 - 8:48:04 AM
Document(s) archivé(s) le : Monday, March 20, 2017 - 8:52:56 PM

File

aaai17 (1).pdf
Files produced by the author(s)

Identifiers

  • 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 trees with converse to tree automata. 2016. ⟨hal-01117830v2⟩

Share

Metrics

Record views

427

Files downloads

100