2026-07-25T06:21:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14379 2024-03-06T10:54:15Z ddc:004 open_access

Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation Havlena, Vojtěch Lengál, Ondřej 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vojtěch Havlena and Ondřej Lengál 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.2 urn:nbn:de:0030-drops-143799 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.2 eng https://creativecommons.org/licenses/by/4.0/legalcode