Symbolic tree automata

• Classical tree automata are extended to work modulo infinite alphabet theories.
• Most important classical properties effectively generalize to the symbolic case.
• The key results are effective closure under complement, and intersection.
• The results are relevant in program analysis using state-of-the-art SMT solvers.

We introduce symbolic tree automata as a generalization of finite tree automata with a parametric alphabet over any given background theory. We show that symbolic tree automata are closed under Boolean operations, and that the operations are effectively uniform in the given alphabet theory. This generalizes the corresponding classical properties known for finite tree automata.