Ranker: A Tool for Complementing Büchi Automata

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

software

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

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

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

Buchi automata complementation rank-based complementation language inclusion model checking

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.

https://github.com/vhavlena/ranker

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

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

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

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