Faculty of Information Technology, BUT

Product Details

Gaston - Symbolic WS1S Solver

Created: 2017

Czech title
Gaston - Symbolická WS1S Rozhodovací Procedura
Type
software
License
required - free
Authors
Fiedor Tomáš, Ing. (FIT BUT)
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Janků Petr, Ing. (FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords

WS1S
finite automata
logic
antichains
lazy evaluation
subsumption
monadic second-order logic
Description
Gaston is an implementation of backward decision procedure for WS1S logic (weak second-order theory of k successors). The tool is using libmona a highly optimised deterministic finite tree automata library that supports semi-symbolic encoding using multi-terminal binary decision diagrams (MTBDDs) for storing transition table of the automaton. Procedure generates state space on-the-fly and prunes the states using the antichain-based approach. The tool works on the symbolical representation of the formula as Symbolic Automata and tries to prove on-the-fly that the initial states intersect the final states to (dis)prove validity.
Location
Licence
Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).
Back to top