Detail publikace

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

Originální název

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

Anglický název

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

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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.

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",
  annote="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.",
  address="Springer Verlag",
  booktitle="Proceedings of TACAS'12",
  chapter="91457",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Springer Verlag",
  number="7214",
  volume="2012",
  year="2012",
  month="april",
  pages="79--94",
  publisher="Springer Verlag",
  type="journal article - other"
}