Ranker: A Tool for Complementing Büchi Automata

Název česky

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

Typ

software

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

Autoři

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

Klíčová slova

Buchi automata
complementation
rank-based complementation
language inclusion
model checking

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

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, řeš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

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

Pracoviště

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