Detail produktu
Gaston - Symbolic WS1S Solver
Vznik: 2017
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Janků Petr, Ing., Ph.D. (VZ VERIFIT)
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
Efektivní automaty pro formální rozhodování, GAČR, Juniorské granty, GJ16-24707Y, zahájení: 2016-01-01, ukončení: 2018-12-31, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
Přibližná ekvivalence pro aproximativní počítání, GAČR, Standardní projekty, GA16-17538S, zahájení: 2016-01-01, ukončení: 2018-12-31, ukončen