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.
tree automata algorithms logic satisfiability modulo theories formal methods