Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata
- 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).