Články v časopisech
| Holík, L., Lengál, O., Šimáček, J., Vojnar, T.: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, In: Lecture Notes in Computer Science, roč. 2011, č. 6996, DE, s. 243-258, ISSN 0302-9743 | | Jazyk publikace: | angličtina |
|---|
| Název publikace: | Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata |
|---|
| Název (cs): | Efektivní testování inkluze explicitních a polo-symbolických stromových automatů |
|---|
| Strany: | 243-258 |
|---|
| Místo vydání: | DE |
|---|
| Rok: | 2011 |
|---|
| Časopis: | Lecture Notes in Computer Science, roč. 2011, č. 6996, DE |
|---|
| ISSN: | 0302-9743 |
|---|
| Klíčová slova |
|---|
tree automata, binary decision diagrams, language inclusion, downward inclusion checking, symbolic encoding
|
| Anotace |
|---|
Tento článek pojednává o několika problémech jež se vážou k efektivnímu použití stromových automatů ve formální verifikaci. Nejdříve je popsán nový efektivní algoritmus pro testování inkluze nedeterministických stromových automatů. Algoritmus prochází automatem směrem shora dolů, využívajíc protiřetězce a simulace ke svému urychlení. Výsledky sady experimentů ukazují, že tento přístup často výrazně převyšuje dosud nejčastěji používané testování inkluze zdola nahoru. Dále je navžena nová polo-symbolická reprezentace nedeterministických stromových automatů, jež je vhodná pro automaty s velkými abecedami, spolu s algoritmy pro testování inkluze shora dolů i zdola nahoru využívajících této reprezentace. Výsledky experimentů porovnávající tyto algoritmy znovu ukazují, ze testování inkluze shora dolů je velmi často lepší než testování inkluze zdola nahoru.
|
| BibTeX: |
|---|
@ARTICLE{
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 = {243--258},
journal = {Lecture Notes in Computer Science},
volume = {2011},
number = {6996},
year = {2011},
ISSN = {0302-9743},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9703}
} |
|