# DBA Minimizer

Coypright © 2010 Ruediger Ehlers, Saarland University

## Introduction

Deterministic Büchi automata (DBA) can be used to model most properties found in the specification of circuits in practice. While the class of languages representable by DBA does not include for example all properties representable by linear-time temporal logic (LTL), in contrast to non-deterministic Büchi automata, they have an important advantage: the problem of deciding whether an automaton is minimal is contained in the complexity class NP. Hence, for the minimization of these automata, SAT solvers can be used.

The *DBA Minimizer* tool set uses an external SAT solver to perform such a minimization task. It contains tools for encoding the state space reduction problem into a DIMACS SAT instance and interpreting a satisfying assignment back to a smaller DBA. An included python script encapsulates all steps.

## Requirements

For correct operation of the *DBA Minimizer* tool set, a moderately modern Linux distribution with Python 2.x installed is required. For SAT solving, the solver picosat is required. Using Debian or Ubuntu Linux, this can for example made sure by installing the `picosat`

package. For obtaining the initial deterministic automata from LTL specifications, the tools `ltl2dstar`

by Joachim Klein and `ltl2ba`

by Dennis Oddoux and Paul Gastin need to be installed. Installation instructions can be found on the respective homepages.

## Description & Usage

The DBA Minimizer tool set aims at automating the task of minimising deterministic Büchi automata. It is assumed that the input file is given in the file format as put out by `ltl2dstar`

. As an example, consider the LTL specification **GF (a → XXb)**. The specification can be converted to a deterministic Rabin automaton by writing it in prefix notation to a file and running `ltl2dstar`

on this file. Assuming that both `ltl2dstar`

and `ltl2ba`

are installed, this can be done using the using the following command sequence:

`echo "G F i a X X b" > /tmp/example.ltl`

`/path/to/ltl2dstar --ltl2nba=spin:/path/to/ltl2ba --output=automaton /tmp/example.ltl /tmp/example.aut`

Assuming that the DBA Minimiser tools have been compiled (by running `make`

in the “Minimizer” directory after extracting the *DBA Minimizer* archive), the automaton can be minimized by running the “minimize” script included.

`/path/to/minimize.py /tmp/example.aut > /tmp/best.aut`

Whenever the automaton is not representable as a DBA, this results in an error message. In case a different SAT solver should be used, the “minimize.py” script can be changed. The result is again stored in form of a file in the ltl2dstar output file format as a one-pair Rabin automaton without rejecting states. The resulting automaton can be visualised using the tool included in the *DBA Minimizer* distribution:

`/path/to/dbaminimizer/Minimizer/dotbuilder /tmp/best.aut > /tmp/best.dot`

`dot -Tpng -o /tmp/best.png /tmp/best.dot`

The latter step requires that the graphviz package is installed correctly.

## Benchmarks

We performed an experimental evaluation of the tool set on the 8 out of 12 example LTL formulas representable as DBAs from the paper *Optimizing Büchi Automata* by Etessami and Holzmann. Additionally, some LTL formulas typical for applications in synthesis and model checking have been added. The details of the experimental evaluation is avaliable here.

## Publications

[Ehl10d] | Rüdiger Ehlers. Minimising Deterministic Büchi Automata Precisely using SAT Solving. Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2010). |

## Download

Note that this tool set is in a prototype stage. Thus, there may be bugs in the implementation. 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.

DBA Minimizer package, version from the 25th of November 2011