Ranker: A Tool for Complementing Büchi Automata

Typ

software

Jazyk

anglicky

Autoři

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

Popis

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.

Klíčová slova

Buchi automata
complementation
rank-based complementation
language inclusion
model checking

URL

https://github.com/vhavlena/ranker

Licence

Využití výsledku jiným subjektem je možné bez nabytí licence (výsledek není licencován)

Licenční poplatek

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Licenční podmínky

Volně šiřitelný software pod MIT licencí https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE

Projekty

Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
Spolehlivé, bezpečné a efektivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-20-6427, zahájení: 2020-03-01, ukončení: 2023-02-28, ukončen
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů, GAČR, Standardní projekty, GA20-07487S, zahájení: 2020-01-01, ukončení: 2022-12-31, ukončen

Výzkumné skupiny

Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Pracoviště

Ústav inteligentních systémů (UITS)