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.