Product Details
Ranker: A Tool for Complementing Büchi Automata
Created: 2022
Czech title
Ranker: Nástroj pro komplementaci Büchiho automatů
Type
software
License
Use of the result by another entity is possible without acquiring a license (the result is not licensed)
License Fee
The licensor does not require a license fee for the result
Authors
Havlena Vojtěch, Ing., Ph.D.
(DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Šmahlíková Barbora, Ing. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Šmahlíková Barbora, Ing. (DITS)
Keywords
Buchi automata complementation rank-based complementation language inclusion model checking
Description
Ranker is a tool for complementing Büchi automata, necessary, e.g., in automata-based model checking of reactive systems. It uses rank-based complementation as its basic procedure, but enriches it with many optimizations and heuristics. Moreover, for automata of specific types (e.g., inherently weak automata, semi-deterministic automata), it contains specialized constructions with novel optimizations.
Location
License Conditions
Open source software under the MIT license https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, 2020-2024, running
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, 2020-2022, running
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, 2020-2023, completed
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, 2020-2022, running
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, 2020-2023, completed
Research groups
Departments