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).
It is highly recommended to use a recent Linux distribution for experimenting with libvata. A zip archive with the library is here.
Or you can clone the git repository with the library (the repository is available on github). For this you need to have the git version control system installed. To clone the repository, run
$ git clone git://github.com/ondrik/libvata.git
Follow the instructions in the README file in the root directory of the downloaded repository for compiling and running the command-line interface.
See the README file in the root directory of the downloaded repository for instructions about usage.
libvata so far supports only the Timbuk format of tree automata. The format is specified by the following grammar with the start symbol <file>:
<file> : 'Ops' <label_list> <automaton>
<label_list> : <label_decl> <label_decl> ... // a list of label declarations
<label_decl> : string ':' int // a symbol declaration (the name and the arity)
<automaton> : 'Automaton' string 'States' <state_list> 'Final States' <state_list> 'Transitions' <transition_list>
<state_list> : <state> <state> ... // a list of states
<state> : string // the name of a state
<transition_list> : <transition> <transition> ... // a list of transitions
<transition> : <label> '(' <state> ',' <state> ',' ... ')' '->' <state> // a transition
<label> : string // the name of a label
An example could look like this:
Ops a:0 b:1 c:2 Automaton A States q0 q1 q2 Final States q2 Transitions a() -> q0 b(q0) -> q1 c(q1, q1) -> q1 c(q1, q1) -> q2 c(q2, q2) -> q2
This work was supported by the Czech Science Foundation (within projects P103/10/0306 and 102/09/H042), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), and the EU/Czech IT4Innovations Centre of Excellence project CZ.1.05/1.1.00/02.0070.
If you have further questions, do not hesitate to contact authors (Ondrej Lengal, Jiri Simacek and Tomas Vojnar).