Gaston - Symbolická WS1S Rozhodovací Procedura

Autoři:Fiedor Tomáš, Holík Lukáš, Janků Petr, Lengál Ondřej, Vojnar Tomáš
Typ:software
Vznik:2017
Licence:vyžadována - zdarma
Klíčová slova:
WS1S
finite automata
logic
antichains
lazy evaluation
subsumption
monadic second-order logic
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í:
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
Výzkumné skupiny:
Pracoviště:
Licenční podmínky:
Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).

Vaše IPv4 adresa: 107.22.126.144
Přepnout na IPv6 spojení

DNSSEC [dnssec]