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.dotdot -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