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.