Detail publikace

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

LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 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
anglicky
Autoři
Lengál Ondřej, Ing., Ph.D. (UITS)
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Klíčová slova

tree automaton, language inclusion, antichain, simulation, tree automata library

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{BUT91457,
  author="Ondřej {Lengál} and Jiří {Šimáček} and Tomáš {Vojnar}",
  title="VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7214",
  pages="79--94",
  issn="0302-9743"
}
Nahoru