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