Kofola: Modular Complementation and Inclusion Checking for Omega Automata

Kofola is an open source tool for an efficient complementation and inclusion checking of automata over infinite words (omega automata). Kofola has been built on top of SPOT and inspired by Seminator and COLA.

Requirements and dependencies

For a successful build of Kofola, cmake of version 3.16 (or higher) together with a C++ compiler with a support of C++-17 standard is required. Additional requirements include:

• Spot

For Debian-like systems, Spot can be installed using the package libspot-dev. For building Spot from sources, download the recent version and run:

./configure

One can set the maximal number of colors for an automaton when configuring Spot with --enable-max-accsets=INT.

make
sudo make install

Building Kofola

Please run the following steps to compile Kofola after cloning this repo:

mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make

Then you will get an executable in build/src/kofola. Alternatively you can run make release in the root directory.

Basic usage

Kofola assumes input omega automata in HOA format. The following command translates general (nondeterministic) omega-automaton stored in file A.hoa into a complementary omega automaton and prints it to the standard output:

./kofola A.hoa --complement

Note that Kofola produces automata with a general accepting condition (different output type might be specified by --tba for transition-based Büchi automata or --tgba for transition-based generalized Büchi automata).

The following command then checks if the language specified by the omega automaton A.hoa is included in the language specified by B.hoa and prints the result to the standard output:

./kofola A.hoa B.hoa --inclusion

Additional parameters might be passed using --params, e.g., --params='merge_iwa=yes'. In order to get a program help, run

./kofola --help

Parameters

The complementation and the inclusion checking might be adjusted by the following key-value parameters passed as --params='key1=val1;key2=val2':

Key	Value	Description
merge_iwa	yes,no	Merge inherently weak components for the synchronous construction
merge_det	yes,no	Merge deterministic components for the synchronous construction
preproc_incl_A	low,medium,high	Level of preprocessing applied on the first automaton (--inclusion only)
preproc_incl_B	low,medium,high	Level of preprocessing applied on the second automaton (--inclusion only)
nac-alg	subs_tup	Algorithm applied on nondeterministic accepting components. subs_tup = subset tuple construction (default for --inclusion). If not specified otherwise, complementation may use determinization-based construction.
postponed	yes,no	Use postponed construction instead the synchronous one (--complement only)
dir_sim	yes,no	Use direct simulation for macrostate pruning
sim-ms-prune	yes,no	Use simulation-based pruning of macrostates during complementation (default: yes; may auto-disable for very large automata)
early_sim	yes,no	Use early simulation for macrostate pruning (--inclusion only)
early_plus_sim	yes,no	Use early+1 simulation for macrostate pruning (--inclusion only)
gfee	yes,no	Use a good for emptiness relation for early termination (--inclusion only)
tela	yes,no	If yes, use TELA-specific algorithms for complementation (if no, the input is converted to TBA)
sh-break	yes,no	Enable shared breakpoint across partial algorithms; when yes partial algorithms that support shared breakpoints propagate a common breakpoint across partitions
tela_det_alg	inductive, dnf-tela	Algorithm selection for complementing deterministic TELA components (default dnf-tela)

Testing

Kofola includes a comprehensive test suite using the Catch2 framework to ensure the correctness of its components.

Running Tests

To build and run the tests:

cd build
cmake .. -DBUILD_TESTS=ON
make kofola_tests
./tests/kofola_tests

Alternatively, use the convenience script:

./tests/run_tests.sh

For more details, see the tests README.

Publications

• V. Havlena, O. Lengál, Y. Li, B. Šmahlíková and A. Turrini. Modular Mix-and-Match Complementation of Büchi Automata. In Proc. of TACAS'23, volume 13993 of LNCS, pages 249-270, 2023. Springer.