libVATA - A C++ library for efficient manipulation with non-deterministic finite (tree) automata. libvata is a highly optimised non-deterministic finite tree automata library. The main focus of the library is to be used in formal verification, but we believe that it can be effectively used in other domains as well. There are two supported encoding of tree automata supported by the library: explicit and semi-symbolic. The semi-symbolic encoding uses multi-terminal binary decision diagrams (MTBDDs) for storing the transition table of the automaton. It is intended to be used for automata with large alphabets, which appear in several formal verification techniques using tree automata, e.g., in the context of verification of programs with complex dynamic data structures, such as the abstract regular tree model checking (ARTMC), or decision procedures of several logics, such as the monadic second-order logic (MSO) or the weak second-order theory of k successors (WSkS). Moreover, the library can also be used for finite word automata (which are, basically, unary trees).

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Clemente, Lorenzo; Mayr, Richard: Efficient reduction of nondeterministic automata with application to language inclusion testing (2019)