Constrained Tree Automata

We study automata formalisms computing on trees of finite rank, labeled by symbols from a finite alphabet, extended by constraints, and different applications of these formalisms.

One of the first extensions of tree automata considered (see this book or this survey) consists of adding local constraints that test, during each transition, equalities (isomorphisms) and inequalities between neighboring subtrees (i.e., at a bounded distance). The corresponding models were introduced as decision tools in the context of automatic theorem proving, due to their link with non-linearity properties of variables in term rewriting systems. During my thesis and immediately afterwards, I worked on emptiness decision problems (is the tree language defined by a given automaton empty?) for different classes of local constraint tree automata (work presented at STACS’94 and ICALP’94), with for main result closing the open problem of the exact complexity of the ground reducibility property
(LICS’97 and IC’03). Later, we disproved an old conjecture on the emptiness decision for a broader class of such automata, called reduction automata (see also this book).

We studied an extension of these formalisms where local constraints are evaluated modulo equational theories (IJCAR’06 and JLAP’08). Representing these automata as sets of Horn clauses, we use a paramodulation calculus with appropriate strategies (basic, ordered, with selection) to establish the termination of decision algorithms. Previously, we had applied a similar approach to tree automata with more restrictive, so-called flat, modulo equation theory constraints, using another superposition calculus.

Another approach for extending tree automata is to add global constraints, which are tested all at once at the end of an automata calculation on a tree, and consist of a combination of equality and inequality tests between subtrees at positions defined during the automata calculation. A fundamental difference with the local constraints mentioned above is that the distance between the positions tested is arbitrary. The first class of tree automata of this type was introduced under the name TAGED. We studied a subclass of TAGEDs called Rigid Tree Automata (LATA’09 and IC’11), which have good decision and expressive properties. We have also solved the problem of void decidability for a model that strictly extends TAGED (LICS’07 and LMCS’13), in particular with arithmetic constraints and constraints similar to unary key constraints in databases.

The two theoretical problems of the complexity of ground reducibility and the decidability of the emptiness for the TAGED class were considered difficult within the community, remained unsolved for years, and were the subject of several theses before we solved them.

Finally, we proposed (FOSSACS’07 and LMCS’08) a class of tree automata (known as visible memory automata) extended by an auxiliary memory containing a tree, whose expressiveness lies between standard tree automata and context-free tree grammars. Unlike the latter, visible memory tree automata define a class of languages closed by intersection and complement, generalizing the automata of nested words.

Applications and Developments

The formalisms presented in
STACS’94,
ICALP’94, RTA’98 on the one hand, and IJCAR’06, JLAP’08 and LATA’09, IC’11 on the other, find applications respectively in automatic deduction (see LICS’97, IC’03, IJCAR’08, JAL’12, UNIF’06, RTA’09) and the implementation of in the system SPASS and in logical verification of security protocols, see IC’11 and the development of TACE.

The automata of the class TAGED were introduced by Emmanuel Filiot, Jean-Marc Talbot, and Sophie Tison in connection with the satisfiability decision for TQL spatial logic, in which queries on XML documents can be expressed. Their extensions proposed in LICS’07 and LMCS’13 are also well suited to the analysis of XML schemas: satisfiability, inclusion, or equivalence problems for schemas.

Dissemination

In addition to the publications cited above, in conferences or international journals, I have contributed to the online book TATA (Tree Automata Techniques and Applications), considered a reference in the field of tree automata theory and its applications and used in teaching this discipline.