Publication Details
Complementing Büchi Automata with Ranker
Lengál Ondřej, Ing., Ph.D. (DITS)
Šmahlíková Barbora, Ing. (RG VERIFIT)
Büchi automata, complementation, rank-based complementation, omega-regular
languages
We present the tool Ranker for complementing Büchi 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.
@inproceedings{BUT178204,
author="Vojtěch {Havlena} and Ondřej {Lengál} and Barbora {Šmahlíková}",
title="Complementing Büchi Automata with Ranker",
booktitle="Proceedings of the 34th International Conference on Computer Aided Verification",
year="2022",
journal="Lecture Notes in Computer Science",
number="13372",
pages="188--201",
publisher="Springer Verlag",
address="Haifa",
doi="10.1007/978-3-031-13188-2\{_}10",
isbn="978-3-031-13187-5",
issn="0302-9743"
}