Seminator is a free tool for semi-determinization of omega automata.
Switch branches/tags
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


Seminator is a free tool for semi-determinization of omega-automata.


Seminator depends on the Spot library. You need a version 2.4 or higher installed in your system before compiling Seminator.

After Spot is installed you can use the attached makefile to compile Seminator.


Basic usage

The following command translates a possibly nondeterministic transition-based generalized Büchi automaton (TGBA) placed in file aut.hoa into a semi-detetrministic Büchi automaton (SDBA) and prints the result int the HOA format to the standard output.

./seminator -f aut.hoa

For more information run:

./seminator --help

Experimental evaluation

Seminator was presented in the paper František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmir Kretinsky and Jan Strejcek. Seminator: A Tool for Semi-Determinization of Omega-Automata. In Proceedings of LPAR-21, 2017.

Jupyter notebook Experimental evaluation will guide you through the steps we used to generete the evaluation presented there. It compares Seminator to ltl2ldba and nba2ldba from the Owl library.

However, both Owl and Seminator evolved since the paper was published so new in this version of scripts you will find comparison with the current version of Seminator and a recent version of Owl.

If the preview of the notebooks on gitHub does not work, use Jupyter nbviewer instead


If you would like to run the notebook by yourself, you need to have the folowing tools installed in PATH on your system.

  • SPOT v. 2.4+ with Python bindings
  • Pandas Python library v. 0.21.0+
  • Jupyter notebook v 5.0+
  • R with libraries ggplot2 and colorspace