Gaston - Symbolic WS1S Solver

Gaston - Symbolická WS1S Rozhodovací Procedura

software

vyžadována - zdarma

Fiedor Tomáš, Ing., Ph.D. (FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Janků Petr, Ing. (FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)

Gaston je implementace rozhodovací procedury pro logku WS1S (slabá druho-řadá logika s jedním následníkem). Nástroj využívá knihovnu libmona, vysoce optimalizovanou knihovnu pro práci s deterministickými konečnými automaty, která podporuje polo-symbolické kódování pomocí multi-terminálních binárních rozhodovacích diagramu (tzv. MTBDD) pro uložení přechodové relace automatu. Procedura generuje stavový prostor 'on-the-fly' a prořezává stavy pomocí technik založených na protiřetězcích (antichains). Nástroj pracuje nad symbolickou reprezentaci formule, tzv. symbolickými automaty a snaží se dokázat, že průnik koncových a počátečních stavů formule je neprázdný k dokázání (ne)validity. 

Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/ a https://github.com/tfiedor/gaston

Bezpečné a spolehlivé počítačové systémy (FIT-S-17-4014)
Efektivní automaty pro formální rozhodování (GJ16-24707Y)
IT4Innovations excellence in science (LQ1602)
Přibližná ekvivalence pro aproximativní počítání (GA16-17538S)

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

Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)