Seminator is a free tool for semi-determinization and complementation of omega-automata.
Seminator 2 was presented at CAV'2020 and is described in the paper
Seminator 2 can complement generalized Büchi automata via improved semi-determinization.
The presentation of the paper is available on YouTube
Seminator depends on the Spot library. You need version 2.8.4 or higher
installed in your system before compiling Seminator.
Also, unless Python bindings are disabled (with ./configure --disable-python),
you will need Python 3 development files installed on your system.
If you would like to run the notebooks or the test-suite, you need Jupyter notebook v 5.0+.
After Spot is installed you can run ./configure && make to compile Seminator.
You may use ./configure --prefix=PREFIXDIR && make && sudo make install to
install Seminator in the same place as Spot. If you need to install Seminator
in a different location, use ./configure --prefix=OTHERDIR --with-spot=PREFIXDIR,
replacing PREFIXDIR by the directory that was passed to Spot's --prefix
configuration option.
On Linux, if you installed Seminator with --prefix=/usr/local (the default) or
--prefix=/usr, make sure you run sudo ldconfig after sudo make install so
that the shared library can be found. If you installed Seminator in another
directory, you probably need to set the LD_LIBRARY_PATH environment variable
to the directory where the shared library was installed.
You might need to run autoreconf -i before calling ./configure && make.
The SPOT's sandbox comes with Seminator 2 pre-installed and also
contains the notebooks from the notebooks directory.
The following command translates a possibly nondeterministic transition-based
generalized Büchi automaton (TGBA) placed in file aut.hoa into a
semi-deterministic Büchi automaton (SDBA) and prints the result in the
HOA format to the standard output.
./seminator aut.hoa
The following command complements the TGBA placed in file aut.hoa using semi-determinization as an intermediate step.
./seminator --complement aut.hoa
For more information run:
./seminator --help
The following picture gives a summary of the different options and how they affect the tool.
For example of using the Python bindings, see the notebooks in the notebooks/
directory. 
Unless you have run make install to install the seminator binary and all the
Python bindings, is using the bindings require a bit of setup to make sure that
Python finds the correct files. The easiest way to use the non-installed bindings
is use the tests/pyrun script: use tests/pyrun python3 or
tests/pyrun jupyter notebookfor interactive uses, ortests/pyrun mycript.py`
for an actual script.
The experimental evaluation for version 2.0 is now kept in a separate repository and is accessible in a Docker image, see below.
The evaluation of the previous versions, check out the source of this repository for version 1.2 (or older).
A Docker image containing a compiled version of Seminator, several related tools
readily usable to reproduce the experimental-evaluation or simply experiment
with the tools can be found on DockerHub.
If you need to reference Seminator in an academic publication, please cite the following paper.
Seminator 2 can complement generalized Büchi automata via improved semi-determinization. František Blahoudek, Alexandre Duret-Lutz, and Jan Strejček. In Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20), volume 12225 of Lecture Notes in Computer Science, pages 15–27. Springer, July 2020. DOI: 10.1007/978-3-030-53291-8_2 [bib, pdf]
Version 1.1 of Seminator was presented in the following paper.
Seminator: A Tool for Semi-Determinization of Omega-Automata. František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský and Jan Strejček. Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-21), volume 46 of EPiC Series in Computing, pages 356–367. EasyChair Publications, May 2017. DOI: 10.29007/k5nl [bib, pdf]