Publication Details

Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)

HAVLENA Vojtěch and LENGÁL Ondřej. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report). Ithaca, 2021. Available from: https://arxiv.org/abs/2010.07834
Czech title
Snižování úrovní: efektivní komplementace Büchiho automatů založená na úrovních (technická zpráva)
Type
technical report
Language
english
Authors
URL
Keywords

Büchi automata,rank-based complementation,super-tight runs

Abstract

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.

Published
2021
Pages
1-28
Place
Ithaca, US
BibTeX
@TECHREPORT{FITPUB12535,
   author = "Vojt\v{e}ch Havlena and Ond\v{r}ej Leng\'{a}l",
   title = "Reducing (to) the Ranks: Efficient Rank-based B{\"{u}}chi Automata Complementation (Technical Report)",
   pages = "1--28",
   year = 2021,
   location = "Ithaca, US",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12535"
}
Back to top