Department of Information Technology

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata


Ondrej Lengal

Date and Time

Thursday, November 10th, 2011 at 10:30


Polacksbacken, room 1245


The presentation considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilising antichains and simulations to optimise its run. Results of a set of experiments are provided, showing that such an approach often 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 inclusion is very often better than upward inclusion checking.

Expected duration

It should be quite short... approximately 30 minutes (maybe more if there are questions).

Back to the seminar page

Updated  2011-11-03 18:41:49 by Frédéric Haziza.