Reducing (to) the Ranks: Efficient Rank-based B\"{u}chi Automata Complementation (Technical Report)

TL;DR

This paper introduces several practical optimizations to the rank-based approach for complementing Büchi automata, significantly reducing automata size and improving efficiency in many cases.

Contribution

It develops new pruning techniques for Schewe's optimal construction, preserving tight runs and producing smaller automata in practice.

Findings

Optimizations significantly improve the rank-based approach.

In many cases, the resulting automata are the smallest among state-of-the-art tools.

The techniques are validated on a large benchmark set.

Abstract

This paper provides several optimizations of the rank-based approach for complementing B\"{u}chi automata. We start with Schewe's theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by a large number of state-of-the-art tools for B\"{u}chi complementation.