Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata
Lukaÿ sH ol, Ondÿ rej Lengal · 2011
The paper considers several issues related to efficient use of tree au- tomata in formal verification. First, a new efficient algorithm for inclusion check- ing on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach of- ten very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclu- sion is very often better than upward inclusion checking.