Artifact for the CAV'22 paper 'Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition'

In our paper, we present a divide-and-conquer determinization algorithm for nondeterministic Büchi automata (NBAs). We classify each strongly connected component (SCC) according to its nondeterministic and acceptance properties and we determinize each SCC independently from the others, by means of specialized algorithms. Lastly, we combine the obtained deterministic outcomes to derive the final deterministic Emerson-Lei automaton. We implemented our algorithm in a prototype tool named COLA (made anonymous as "ourDC" in the submitted double-blind draft) and empirically evaluate COLA with the state-of-the-art tools SPOT and OWL on a large set of benchmarks from literature. For artifact evaluation, we provide a Virtual Machine image with 2 cores and 4GB of RAM (which should be suitable for all recent desktop and laptop machines), whose operating system is Ubuntu 20.04; login is automatic, but in case of need, use "experiments" for both username and password. In the home directory of the user "experiments" we include the source code of our tool COLA, the benchmarks used in the experiments and the script files for running the experiments and generating the plots included in the paper. Please note that in the paper, we performed the experiments natively on a desktop machine with 16GB of RAM and a 3.6 GHz Intel Core i7-4790 CPU. We used Benchexec to trace and constrain the tools' executions, and as parameters for each single execution, we used cpuCores="1", memlimit="12000 MB", and timelimit="10 min" to allow each execution to use a single core and 12 GB of memory, and imposed a timeout of 10 minutes. Due to the 4GB of RAM set as memory size for the virtual machine, we reduced the memory assigned to the experiments from 12GB to 3GB, which might result in few more failures by memory exhaustion for some of the experiments, and thus might not exactly reproduce the same results as in the paper, but the overall trend of the results should be similar. If the reviewer's machine has enough memory, we suggest to increase the ...