A characterization of Büchi tree automata

We show that a language of infinite binary trees is definable by a Σ₂-formula of the monadic second order logic of two successors (with no additional symbols) iff it can be accepted by a Büchi automaton. The same result has been obtained by G. Lenzi, but our proof is simpler.     

Complexity of weak acceptance conditions in tree automata

Weak acceptance conditions for automata on infinite words or trees are defined in terms of the set of states that appear in the run. This is in contrast with, more usual, strong conditions that are defined in terms of states appearing infinitely often on the run. Weak conditions appear in the context of model-checking and translations of logical formalisms to automata. We study the complexity of the emptiness problem for tree automata with weak conditions. We also study the translations between automata with weak and strong conditions.     

Weighted tree automata and weighted logics

We define a weighted monadic second order logic for trees where the weights are taken from a commutative semiring. We prove that a restricted version of this logic characterizes the class of formal tree series which are accepted by weighted bottom-up finite state tree automata. The restriction on the logic can be dropped if additionally the semiring is locally finite. This generalizes corresponding classical results of Thatcher, Wright, and Doner for tree languages and it extends recent results of Droste and Gastin [Weighted automata and weighted logics, in: Automata, Languages and Programming—32nd International Colloquium, ICALP 2005, Lisbon, Portugal, 2005, Proceedings, Lecture Notes in Computer Science, Vol. 3580, Springer, Berlin, 2005, pp. 513–525, full version in Theoretical Computer Science, to appear.] from formal power series on words to formal tree series.     

Folk theorems on the determinization and minimization of timed automata

Timed automata are known not to be complementable or determinizable. Natural questions are, then, could we check whether a given TA enjoys these properties? These problems are not algorithmically solvable. Minimizing the “resources” of a TA (number of clocks or size of constants) are also unsolvable problems. In this paper we provide simple undecidability proofs using a “constructive” version of the problems where we require not just a yes/no answer, but also a “witness”. Proofs are then simple reductions from the universality problem. Recent work of Finkel shows that the corresponding decision problems are also undecidable [O. Finkel, On decision problems for timed automata, Bulletin of the European Association for Theoretical Computer Science 87 (2005) 185-190].     

Closure properties and decision problems of dag automata

Tree automata are widely used in various contexts. They are closed under boolean operations and their emptiness problem is decidable in polynomial time. Dag automata are natural extensions of tree automata, operating on dags instead of on trees; they can also be used for solving problems. Our purpose in this paper is to show that algebraically they behave differently: the class of dag automata is not closed under complementation, dag automata are not determinizable, their membership problem is NP-complete, the universality problem is undecidable, and the emptiness problem is NP-complete even for deterministic labeled dag automata.     

The complexity of tree automata and XPath on grammar-compressed trees

The complexity of various membership problems for tree automata on compressed trees is analyzed. Two compressed representations are considered: dags, which allow to share identical subtrees in a tree, and straight-line context-free tree grammars, which moreover allow to share identical intermediate parts in a tree. Several completeness results for the classes NL, P, and PSPACE are obtained. Finally, the complexity of the evaluation problem for (structural) XPath queries on trees that are compressed via straight-line context-free tree grammars is investigated.     

Weighted automata with discounting

We investigate weighted automata with discounting and their behaviors over semirings and finitely generated graded monoids. We characterize the discounted behaviors of weighted automata precisely as rational formal power series with a discounted form of the Cauchy product. This extends a classical result of Kleene-Schützenberger. Here we show that the very special case of Schützenberger's result for free monoids over singleton alphabets suffices to deduce our generalization.     

Rigid tree automata and applications

We introduce the class of rigid tree automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and some inequality and disequality tests as well. Properties like determinism, pumping lemma, Boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA whereas membership of a given tree to the language of a given RTA is NP-complete. Our main result is the decidability of whether a given tree belongs to the rewrite closure of an RTA language under a restricted family of term rewriting systems, whereas this closure is not an RTA language. This result, one of the first on rewrite closure of languages of tree automata with constraints, is enabling the extension of model checking procedures based on finite tree automata techniques, in particular for the verification of communicating processes with several local non-rewritable memories, like security protocols. Finally, a comparison of RTA with several classes of tree automata with local and global equality tests, with dag automata and Horn clause formalisms is also provided.     

Linearity and nondeletion on monadic context-free tree grammars

In this paper, subclasses of monadic context-free tree grammars (CFTGs) are compared. Since linear, nondeleting, monadic CFTGs generate the same class of string languages as tree adjoining grammars (TAGs), it is examined whether the restrictions of linearity and nondeletion on monadic CFTGs are necessary to generate the same class of languages.     

Two-way deterministic automata with two reversals are exponentially more succinct than with one reversal

We prove that limiting the number of reversals from two to one can cause an exponential blow-up in the size of two-way deterministic automaton.     

Flip-pushdown automata with k pushdown reversals and E0L systems are incomparable

We prove that any propagating E0L system cannot generate the language {w#w|w∈{0,1}^?}$\{w\mathrm{\#}w|w\in {\{0,1\}}^{?}\}$. This result, together with some known ones, enables us to conclude that the flip-pushdown automata with k pushdown reversals, i.e., the pushdown automata with the ability to flip the pushdown, and E0L systems are incomparable. This result solves an open problem stated by Holzer and Kutrib in 2003.     

Tree pattern mining with tree automata constraints

Most work on pattern mining focuses on simple data structures such as itemsets and sequences of itemsets. However, a lot of recent applications dealing with complex data like chemical compounds, protein structures, XML and Web log databases and social networks, require much more sophisticated data structures such as trees and graphs. In these contexts, interesting patterns involve not only frequent object values (labels) appearing in the graphs (or trees) but also frequent specific topologies found in these structures. Recently, several techniques for tree and graph mining have been proposed in the literature. In this paper, we focus on constraint-based tree pattern mining. We propose to use tree automata as a mechanism to specify user constraints over tree patterns. We present the algorithm CoBMiner which allows user constraints specified by a tree automata to be incorporated in the mining process. An extensive set of experiments executed over synthetic and real data (XML documents and Web usage logs) allows us to conclude that incorporating constraints during the mining process is far more effective than filtering the interesting patterns after the mining process.