Minimization of Non-deterministic Büchi Automata using Bound Language Inclusion Checking

Coypright © 2010 Rüdiger Ehlers and Bernd Finkbeiner, Saarland University


Non-deterministic Büchi automata (NBA) can efficiently represent properties in the formal methods context. For success of using them in model checking, they should be minimised prior to application. The NBWMiminizer tool is able to find smaller automata in many cases where classical bisimulation quotienting-based techniques fail.


For correct operation of the NBWMiminizer tool, a moderately modern Linux distribution with Python 2.x installed is required. The tool has to be compiled before usage. We use qmake as the building tool. Under Ubuntu Linux, it should suffice to install the packages build-essential and qmake-qt4.

Additionally, at least one of the following LTL-to-Büchi converters should be installed for computing the input to the NBWMinimizer tool.

Installation instructions can be found on the respective homepages. The latter tool typically produces smaller automata, so its usage is preferred.

Description & Usage

Firstly, the NBWMinimizer tool needs to be extract it to a directory. In this directory, the file Makefile is built by running qmake This should not result in any error messages. Afterwards, by running make, the tool is built.

Before the tool can be used for the minimization of some Büchi automaton, the automaton has to be computed. In fact, we assume that two automata are given: the one that needs to be minimized and an automaton for the complement language. The two automata need to be given a in SPIN never claim format. They have to be named pos.txt and neg.txt and must reside in the same directory. As an example, assume that we want to find a small automaton for the LTL formula “GF(a -> X X b)”. Using spot, the initial automata can be produced as follows:

Using ltl2ba, this task can be done as follows:

Note that the tool will not give a warning if neg.txt does not contain an automaton for the complement language of pos.txt. Automaton minimisation can then be performed by running:

Note that this can take a long time. The Python script performs successive calls to the NBWSat backend program. There exists the possibility to specify a timeout for each individual call:

The timeout needs to be specified in seconds. If the tool succeds, it prints a SPIN never-claim for the automaton to the terminal and otherwise reports that no smaller automaton has been found.


We performed an experimental evaluation of the tool on three benchmark sets for LTL-to-Büchi converters:

The details of the experimental evaluation are avaliable here.


[EF10] Rüdiger Ehlers and Bernd Finkbeiner. On the Virtue of Patience: Minimizing Büchi Automata. Accepted at SPIN 2010.


The prototype is free for use in academic context. For all other purposes, including integration into other tools, please contact the author. Furthermore, the licensing details stated in this document apply.

The tool uses (a slight modification of) minisat v.1.12b by Niklas Eén and Niklas Sörensson as a reasoning backend. The sources in the Minisat directory of the download archive found below are thus under a different license, namely the one found in that directory.


Note that this tool set is in a prototype stage. Thus, there may be bugs in the implementation.

The NBWMinimizer tool


Rüdiger Ehlers