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

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F12%3APU98165" target="_blank" >RIV/00216305:26230/12:PU98165 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

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 possiblerange 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 simulationsas 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 previou

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2012

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Volume of the periodical

2012

Issue of the periodical within the volume

7214

Country of publishing house

DE - GERMANY

Number of pages

16

Pages from-to

79-94

UT code for WoS article

—

EID of the result in the Scopus database

—