Ranker: A Tool for Complementing Büchi Automata

Název česky

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

Typ

software

Licence

ne - zdarma

Autoři

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

Popis

Ranker je nástroj pro komplementaci Büchiho automatů, což je operace potřebná např. při model-checkingu reaktivních systémů založeném na automatech. Ranker používá rank-based proceduru jako základ pro komplementaci, ale tato procedura je doplněna o řadu optimalizací a heuristik. Navíc nástroj používá specializované a optimalizované procedury pro automaty specifických typů, jako jsou inherentně slabé automaty a semi-deterministické automaty.

Umístění

https://github.com/vhavlena/ranker

Licence

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

Projekty

Efektivní konečné automaty pro automatické usuzování (LL1908)
Spolehlivé, bezpečné a efektivní počítačové systémy (FIT-S-20-6427)
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů (GA20-07487S)

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ů FIT VUT v Brně (UITS FIT VUT)