Publication result detail

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

LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.

Original Title

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

English Title

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

Type

Peer-reviewed article not indexed in WoS or Scopus

Original Abstract

In this paper, we present VATA, a versatile and efficient open-source tree automata library applicable, e.g., in formal verification. The library supports both explicit and semi-symbolic encoding of non-deterministic finite tree automata and provides efficient implementation of standard operations on both. The semi-symbolic encoding is intended for tree automata with large alphabets. For storing their transition functions, a newly implemented MTBDD library is used. In order to enable the widest possible range of applications of the library even for the semi-symbolic encoding, we provide both bottom-up and top-down semi-symbolic representations. The library implements several highly optimised reduction algorithms based on downward and upward simulations as well as algorithms for testing automata inclusion based on upward and downward antichains and simulations. We compare the performance of the algorithms on a set of testcases and we also compare the performance of VATA with our previous implementations of tree automata.

English abstract

In this paper, we present VATA, a versatile and efficient open-source tree automata library applicable, e.g., in formal verification. The library supports both explicit and semi-symbolic encoding of non-deterministic finite tree automata and provides efficient implementation of standard operations on both. The semi-symbolic encoding is intended for tree automata with large alphabets. For storing their transition functions, a newly implemented MTBDD library is used. In order to enable the widest possible range of applications of the library even for the semi-symbolic encoding, we provide both bottom-up and top-down semi-symbolic representations. The library implements several highly optimised reduction algorithms based on downward and upward simulations as well as algorithms for testing automata inclusion based on upward and downward antichains and simulations. We compare the performance of the algorithms on a set of testcases and we also compare the performance of VATA with our previous implementations of tree automata.

Keywords

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

Key words in English

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

Authors

LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.

RIV year

2013

Released

01.04.2012

Publisher

Springer Verlag

Book

Proceedings of TACAS'12

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

2012

Number

7214

State

Federal Republic of Germany

Pages from

79

Pages to

94

Pages count

16

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