Minimization of Non-deterministic Büchi Automata using Bound Language Inclusion Checking
Coypright © 2010 Rüdiger Ehlers and Bernd Finkbeiner, Saarland University
Introduction
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.
Requirements
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.
ltl2baby Dennis Oddoux and Paul Gastinspotby Alexandre Duret-Lutz et al., version 0.5a or greater
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 NBWSat.pro. 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:
mkdir /tmp/test/path/to/spot/src/tgbatest/ltl2tgba -N -R3 -r7 "G F (a -> X X b)" > /tmp/test/pos.txt/path/to/spot/src/tgbatest/ltl2tgba -N -R3 -r7 "!( G F (a -> X X b))" > /tmp/test/neg.txt
Using ltl2ba, this task can be done as follows:
mkdir /tmp/test/path/to/ltl2ba/ltl2ba -f "[] <> (a -> X X b)" > /tmp/test/pos.txt/path/to/ltl2ba/ltl2ba -f "! ( [] <> (a -> X X b))" > /tmp/test/neg.txt
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:
/path/to/NBWSat/minimize.py /tmp/test
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:
/path/to/NBWSat/minimize.py --timeout=300 /tmp/test
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.
Benchmarks
We performed an experimental evaluation of the tool on three benchmark sets for LTL-to-Büchi converters:
- The 27 specifications from the paper “Efficient Büchi Automata from {LTL} Formulae” by Fabio Somenzi and Roderick Bloem
- The 12 specifications from the paper “Optimizing Büchi Automata” by Kousha Etessami and Gerard J. Holzmann
- 55 LTL properties built from the specification patterns in the paper “Property Specification Patterns for Finite-state Verification” by Matthew B. Dwyer, George S. Avrunin and James C. Corbett
The details of the experimental evaluation are avaliable here.
Publications
| [EF10] | Rüdiger Ehlers and Bernd Finkbeiner. On the Virtue of Patience: Minimizing Büchi Automata. Accepted at SPIN 2010. |
License
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.
Download
Note that this tool set is in a prototype stage. Thus, there may be bugs in the implementation.