Detail produktu

Gaston - Symbolic WS1S Solver

Vznik: 2017

Název česky
Gaston - Symbolická WS1S Rozhodovací Procedura
Typ
software
Licence
vyžadována - zdarma
Autoři
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)
Popis

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. 

Umístění
Projekty
Výzkumné skupiny
Pracoviště
Nahoru