| HAL-Inria | Publications, software ... of Inria's scientists |
An efficient translation from a modal μ-calculus over finite trees with converse to tree automata
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.
Cited literature [23 references]
https://hal.inria.fr/hal-01117830
Contributor : Tyrex Equipe <>
Submitted on : Friday, December 9, 2016 - 11:00:10 AM
Last modification on : Thursday, May 20, 2021 - 1:54:01 PM
Long-term archiving on: : Monday, March 20, 2017 - 8:52:56 PM
Contributor : Tyrex Equipe <>
Submitted on : Friday, December 9, 2016 - 11:00:10 AM
Last modification on : Thursday, May 20, 2021 - 1:54:01 PM
Long-term archiving on: : Monday, March 20, 2017 - 8:52:56 PM
File
aaai17 (1).pdf
Files produced by the author(s)