Publication Details
Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)
Büchi automata,rank-based complementation,super-tight runs
This paper provides several optimizations of the rank-based approach for
complementing Bü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 state-of-the-art
tools for Büchi complementation.
@techreport{BUT175802,
author="Vojtěch {Havlena} and Ondřej {Lengál}",
title="Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)",
year="2021",
address="Ithaca",
pages="1--28",
url="https://arxiv.org/abs/2010.07834"
}