Product Details

Gaston - Symbolic WS1S Solver

Created: 2017

Czech title
Gaston - Symbolická WS1S Rozhodovací Procedura
Type
software
License
required - free
Authors
Fiedor Tomáš, Ing., Ph.D. (FIT BUT)
Holík Lukáš, doc. 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).

Projects
Research groups
Departments
Back to top