Publication Details

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. Lecture Notes in Computer Science, vol. 2011, no. 6996, pp. 243-258. ISSN 0302-9743.
Czech title
Efektivní testování inkluze explicitních a polo-symbolických stromových automatů
Type
journal article
Language
english
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Šimáček Jiří, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords

tree automata, binary decision diagrams, language inclusion, downward inclusion checking, symbolic encoding

Abstract

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.

Published
2011
Pages
243-258
Journal
Lecture Notes in Computer Science, vol. 2011, no. 6996, ISSN 0302-9743
Publisher
Springer Verlag
BibTeX 
@ARTICLE{FITPUB9703,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l and Ji\v{r}\'{i} \v{S}im\'{a}\v{c}ek and Tom\'{a}\v{s} Vojnar",
   title = "Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata",
   pages = "243--258",
   journal = "Lecture Notes in Computer Science",
   volume = 2011,
   number = 6996,
   year = 2011,
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9703"
}
Back to top