Divide-and-Conquer Determinization of B\"uchi Automata based on SCC Decomposition

TL;DR

This paper introduces a divide-and-conquer method for determinizing nondeterministic B"uchi automata by classifying and independently determinizing SCCs, leading to more efficient automata construction and better empirical performance.

Contribution

It proposes a novel SCC-based divide-and-conquer determinization approach for NBA, improving efficiency and automata size compared to traditional methods.

Findings

COLA outperforms Spot and OWL in state and transition counts

The approach simplifies determinization by leveraging SCC structure

Experimental results demonstrate efficiency gains

Abstract

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.