Článek v časopise

LENGÁL Ondřej, ŠIMÁČEK Jiří a VOJNAR Tomáš. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science. 2012, roč. 2012, č. 7214, s. 79-94. ISSN 0302-9743.
Jazyk publikace:angličtina
Název publikace:VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata
Název (cs):VATA: Knihovna pro efektivní manipulaci s nedeterministickými stromovými automaty
Strany:79-94
Kniha:Proceedings of TACAS'12
Místo vydání:DE
Rok:2012
Časopis:Lecture Notes in Computer Science, roč. 2012, č. 7214, DE
ISSN:0302-9743
Vydavatel:Springer Verlag
Klíčová slova
tree automaton, language inclusion, antichain, simulation, tree automata library
Anotace
Tento článek prezentuje knihovnu VATA, univerzální, efektivní a otevřenou knihovnu pro práci se stromovými automaty, jenž je použitelná např. ve formální verifikaci. Knihovna podporuje explicitní a semi-symbolickou reprezentaci nedeterministických stromových automatů a poskytuje efektivní implementace operací nad oběmi těmito verzemi. Semi-symbolická reprezentace je vhodná pro stromové automaty s velkými abecedami. Pro uložení jejich přechodových funkcí je použita nově implementovaná knihovna pro MTBDD. Z důvodu podpory co nejširší třídy aplikací i pro semi-symbolické kódování je poskytnuta jak reprezentace bottom-up, tak i reprezentace top-down. Knihovna implementuje několik vysoce optimalizovaných redukčních algoritmů založených na downward a upward simulacích a algoritmů pro testování inkluze založených na technikách downward a upward protiřetězců a simulacích. Porovnáváme výkon těchto algoritmů na testovací sadě příkladů taktéž porovnáváme výkon knihovny VATA s našimi předchozími implementacemi stromových automatů.
BibTeX:
@ARTICLE{
   author = {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 = {VATA: A Library for Efficient Manipulation of
	Non-Deterministic Tree Automata},
   pages = {79--94},
   booktitle = {Proceedings of TACAS'12},
   journal = {Lecture Notes in Computer Science},
   volume = {2012},
   number = {7214},
   year = {2012},
   publisher = {Springer Verlag},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=9844}
}

Vaše IPv4 adresa: 34.204.0.181
Přepnout na https