# Automata Library

The Ultimate Automata Library supports the following kinds of automata.

- Finite automata (see example)
- Nested word automata, aka visibly pushdown automata
- Büchi automata (see example)
- Büchi nested word automata (see example)
- Petri net automata, i.e., Petri nets used as language acceptors (see example)
- Alternating finite automata
- Tree automata

The library is maintained by Matthias Heizmann, Alexander Nutz, and Christian Schilling.

## Web Interface

The library is available via a web interface.
We devised a small script language called *Automata Script* that allows to define automata and specify operations that should be performed.
You can find several sample files in the web interface.

## News

### Minimization based on partial Max-SAT for nested word automata available (2017-02-09)

The operation minimizeNwaPmaxSat (see example) implements the algorithm of the Minimization of Visibly Pushdown Automata Using Partial Max-SAT paper which was published at TACAS 2017.
It uses a domain-specific partial Max-SAT solver for reducing the size of nondeterministic nested word automata.

Additional material: extended version,
slides

### Optimized complementation for semi-deterministic Büchi automata available (2016-04-12)

The operation buchiComplementNCSB (see example) implements the algorithm of the Complementing Semi-deterministic Büchi Automata paper which was published at TACAS 2016.

Additional material: preprint, files to reproduce evaluation, slides

### Computation of loop complexity available (2015-09-15)

The operation loopComplexity computes the loop complexity of finite automata. An example automata script file is available in our web interface.

## Source Code

The source code is available at GitHub.