Combining equational tree automata over AC and ACI theories

Abstract

In this paper, we study combining equational tree automata in two different senses: (1) whether decidability results about equational tree automata over disjoint theories ε1 and ε2 imply similar decidability results in the combined theory ε1 ∪ ε2; (2) checking emptiness of a language obtained from the Boolean combination of regular equational tree languages. We present a negative result for the first problem. Specifically, we show that the intersection-emptiness problem for tree automata over a theory containing at least one AC symbol, one ACI symbol, and 4 constants is undecidable despite being decidable if either the AC or ACI symbol is removed. Our result shows that decidability of intersection-emptiness is a non-modular property even for the union of disjoint theories. Our second contribution is to show a decidability result which implies the decidability of two open problems: (1) If idempotence is treated as a rule f(x,x) →x rather than an equation f(x,x)=x, is it decidable whether an AC tree automata accepts an idempotent normal form? (2) If ε contains a single ACI symbol and arbitrary free symbols, is emptiness decidable for a Boolean combination of regular ε-tree languages? © 2008 Springer-Verlag.