Complementing B\"uchi Automata with Ranker (Technical Report)

TL;DR

The paper introduces Ranker, a tool for complementing B"uchi automata that employs advanced heuristics and optimizations to produce smaller automata, demonstrating superior performance on real-world benchmarks.

Contribution

Ranker extends previous rank-based automata complementation with new heuristics and specialized optimizations for weak and semi-deterministic automata, improving automata size and usability.

Findings

Ranker produces smaller automata than existing tools in most cases.

Extensive experiments confirm the effectiveness of the optimizations.

The tool is robust and applicable to real-world benchmarks.

Abstract

We present the tool Ranker for complementing B\"uchi automata (BAs). Ranker builds on our previous optimizations of rank-based BA complementation and pushes them even further using numerous heuristics to produce even smaller automata. Moreover, it contains novel optimizations of specialized constructions for complementing (i) inherently weak automata and (ii) semi-deterministic automata, all delivered in a robust tool. The optimizations significantly improve the usability of Ranker, as shown in an extensive experimental evaluation with real-world benchmarks, where Ranker produced in the majority of cases a strictly smaller complement than other state-of-the-art tools.