Cola includes complement algorithms for unambiguous nondeterministic Büchi automata (UNBA) and limit deterministic Büchi automata (LDBA), as well as a determinization algorithm for LDBAs. Cola has been built on top of Seminator.

• The GitHub repo COLA is under developing and much different from the version in this artifact submission. Here we provided the version we used in the experiments of the submission paper.

• Complementing UNBA: the slice-based algorithm

• Determinizing LDBA: in submission

• Spot

autoreconf -i

./configure

make

sudo ldconfig

Then you will get an executable file named cola .

Input an LDBA named "filename", and run ./cola --determinize=parity filename, then you will get an equivalent deterministic parity automaton (DPA) on standard output! To output the DPA to a file, use ./cola --determinize=parity filename -o out_filename