Detail publikace

VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata

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, roč. 2012, č. 7214, s. 79-94. ISSN 0302-9743.
Název česky
VATA: Knihovna pro efektivní manipulaci s nedeterministickými stromovými automaty
Typ
článek v časopise
Jazyk
angličtina
Autoři
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Abstrakt

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ů.

Rok
2012
Strany
79-94
Časopis
Lecture Notes in Computer Science, roč. 2012, č. 7214, ISSN 0302-9743
Kniha
Proceedings of TACAS'12
Vydavatel
Springer Verlag
BibTeX 
@ARTICLE{FITPUB9844,
   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 = "https://www.fit.vut.cz/research/publication/9844"
}
Nahoru