Result Details

Complementing Büchi Automata with Ranker

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker. In Proceedings of the 34th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Haifa: Springer Verlag, 2022. no. 13372, p. 188-201. ISBN: 978-3-031-13187-5. ISSN: 0302-9743.
Type
conference paper
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D., DIFS (FIT), DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Šmahlíková Barbora, Ing.
Abstract

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.

Keywords

Büchi automata, complementation, rank-based complementation, omega-regular languages

Published
2022
Pages
188–201
Journal
Lecture Notes in Computer Science, no. 13372, ISSN 0302-9743
Proceedings
Proceedings of the 34th International Conference on Computer Aided Verification
Conference
34th International Conference on Computer Aided Verification
ISBN
978-3-031-13187-5
Publisher
Springer Verlag
Place
Haifa
DOI
10.1007/978-3-031-13188-2_10
UT WoS
000870310500010
EID Scopus
2-s2.0-85133529643
BibTeX 
@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"
}
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, completed
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, start: 2020-01-01, end: 2022-12-31, completed
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, start: 2020-03-01, end: 2023-02-28, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top