Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata

This report provides the full version of a CIAA'08 paper, in which we propose a new antichain-based algorithms for checking universality and inclusion of nondeterministic tree automata (NTA).  We have implemented these algorithms in a prototype tool and our experiments show that they provide a significant improvement over the traditional determinisation-based approaches. We use our antichain-based inclusion checking algorithm to build an abstract regular tree model checking framework based entirely on NTA. We showthe significantly improved efficiency of this  framework through aseries of experiments with verifying various programs over dynamiclinked tree-shaped data structures.