Gaston - Symbolic WS1S Solver

Gaston - Symbolická WS1S Rozhodovací Procedura

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

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

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

WS1S finite automata logic antichains lazy evaluation subsumption monadic second-order logic

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, VUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, ukončen
Efektivní automaty pro formální rozhodování, GAČR, Juniorské granty, GJ16-24707Y, 2016-2018, řešení
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, ukončen
Přibližná ekvivalence pro aproximativní počítání, GAČR, Standardní projekty, GA16-17538S, 2016-2018, řešení

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

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