Ranker: A Tool for Complementing Büchi Automata

Czech title

Ranker: Nástroj pro komplementaci Büchiho automatů

Type

software

License

no - free

Authors

Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Šmahlíková Barbora, Ing. (FIT BUT)

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

https://github.com/vhavlena/ranker

Licence

Open source software under the MIT license https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE

Projects

Efficient Finite Automata for Automated Reasoning (LL1908)
Reliable, Secure, and Efficient Computer Systems (FIT-S-20-6427)
Scalable Techniques for Analysis of Complex Properties of Computer Systems (GA20-07487S)

Research groups

Automata@FIT (VZ Automata@FIT)
Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)

Departments

Department of Intelligent Systems FIT BUT (DITS FIT BUT)