  The determinization of a nondeterministic B\"uchi automaton (NBA) is a
fundamental construction of automata theory, with applications to probabilistic
verification and reactive synthesis. The standard determinization
constructions, such as the ones based on the Safra-Piterman's approach, work on
the whole NBA. In this work we propose a divide-and-conquer determinization
approach. To this end, we first classify the strongly connected components
(SCCs) of the given NBA as inherently weak, deterministic accepting, and
nondeterministic accepting. We then present how to determinize each type of SCC
independently from the others; this results in an easier handling of the
determinization algorithm that takes advantage of the structure of that SCC.
Once all SCCs have been determinized, we show how to compose them so to obtain
the final equivalent deterministic Emerson-Lei automaton, which can be
converted into a deterministic Rabin automaton without blow-up of states and
transitions. We implement our algorithm in a our tool COLA and empirically
evaluate COLA with the state-of-the-art tools Spot and OWL on a large set of
benchmarks from the literature. The experimental results show that our
prototype COLA outperforms Spot and OWL regarding the number of states and
transitions.
