Technical report

 
Holík, L., Lengál, O., Šimáček, J., Vojnar, T.: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, FIT-TR-2011-04, Brno, CZ, FIT VUT, 2011, p. 22
Publication language:english
Original title:Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata
Title (cs):Efektivní testování inkluze explicitních a polo-symbolických stromových automatů
Pages:22
Place:FIT-TR-2011-04, Brno, CZ
Year:2011
Publisher:Faculty of Information Technology BUT
URL:http://www.fit.vutbr.cz/~ilengal/pub/FIT-TR-2011-04.pdf [HTML]
Keywords
tree automata, binary decision diagrams, language inclusion, downward inclusion checking, symbolic encoding
Annotation
The paper 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, utilizing antichains and simulations to optimize 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.
BibTeX:
@TECHREPORT{
   author = {Lukáš Holík and Ondřej Lengál and Jiří Šimáček and Tomáš
	Vojnar},
   title = {Efficient Inclusion Checking on Explicit and Semi-Symbolic
	Tree Automata},
   pages = {22},
   year = {2011},
   location = {FIT-TR-2011-04, Brno, CZ},
   publisher = {Faculty of Information Technology BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9708}
}