Gaston - Decision Procedure for WS1S Logic

Build Status

  1. About
  2. Download
  3. Compilation
  4. Usage
  5. Input Format
  6. Evaluation
    1. STRAND
    2. UABE
    3. Generated formulae
  7. Contact

About

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.

Prerequisities

Following packages are needed in order to compile and run Gaston on your system:

 git (>= 1.6.0.0)
 cmake (>= 2.8.2)
 gcc (>= 4.8.0)
 flex (>= 2.5.35)
 bison (>= 2.7.1)

Download

In order to compile and work with our tool we highly recommend to clone the repository to the local repository. You need to have the git version control system installed.

To download the library, run

   $ git clone https://github.com/tfiedor/Gaston.git

Compilation

In order to prepare the tool for compilation and commiting a background check for prerequisite package issue the following command in the root directory of the tool:

   $ cmake CMakeLists.txt

To further compile the source files to runable binary issue the following command:

   $ make

Input file syntax

The following grammar describes supported subset of MONA syntax for the specification of verified formulae. It uses the classical BNF-like notation.

For full syntax for MONA tool consult the tool manual at http://www.brics.dk/mona/mona14.pdf.

program ::= (header;)? (declaration;)+
header ::=  ws1s | ws2s

declaration ::= formula
             |  var0 (varname)+
             |  var1 (varname)+
             |  var2 (varname)+
             |  'pred' varname (params)? = formula
             |  'macro' varname (params)? = formula

formula ::= 'true' | 'false' | (formula)
         |  zero-order-var
         | ~formula
         | formula | formula
         | formula & formula
         | formula => formula
         | formula <=> formula
         | first-order-term = first-order-term 
         | first-order-term ~= first-order-term 
         | first-order-term < first-order-term 
         | first-order-term > first-order-term
         | first-order-term <= first-order-term 
         | first-order-term >= first-order-term
         | second-order-term = second-order-term
         | second-order-term = { (int)+ }
         | second-order-term ~= second-order-term
         | second-order-term 'sub' second-order-term
         | first-order-term 'in' second-order-term
         | ex1 (varname)+ : formula
         | all1 (varname)+ : formula
         | ex2 (varname)+ : formula
         | all2 (varname)+ : formula

first-order-term ::= varname | (first-order-term)
                  |  int
                  | first-order-term + int

second-order-term ::= varname | (second-order-term)
                   |  second-order-term + int

Evaluation

We have compared Gaston's performance with that of MONA [1], dWiNA implementing our previous approach [2], the Toss tool implementing the method of Kaizer and Ganzow [3], and the implementations of the decision procedures presented by papers [4] and [5] (which we denote as Coalg and SFA respectively). We didn't compare with the jMosel as their tool seems to be no longer available (see link).

In our experiments, we consider both formulae obtained from various formal verification tasks, as well as parametric families of formulae designed to stress-test WS1S decision procedures. We note that Gaston currently does not perform well on formulae with many Boolean variables and formulae in M2L(str) logic appearing in some other benchmarks, like e.g. Secrets [6] or old version of Strand benchmark [7] , which are not included in our experiments. To handle such formulae, further optimizations of Gaston, such as MONA's treatment of Boolean variables via a dedicated transition or usage of SAT/SMT solvers are needed.

We have obtained our results on a machine with Intel Core i7-4770@3.4 GHz processor and 32 GiB RAM and a machine with Intel Core i7-2600@3.4 GHz processor and 16 GiB RAM, both running Debian GNU/Linux. Note that we needed to use two different machines, as the Toss tool required specific version of OCaml (4.02), which is not available for stable versions of Debian GNU/Linux and thus we had to compare the tools on slower machine with unstable Debian GNU/Linux version. Moreover, the implementation of SFA is in C#, which does not run natively in GNU/Linux and were forced to use the mono compiler, that may not generate efficient code.

On Strand benchmark (see link for more detailed results), Gaston is mostly comparable, in two cases better, and in one case worse than MONA. On UABE (see link for more detailed results), Gaston outperformed MONA on seven out of twenty-three benchmarks, it was worse on ten formulae and comparable on the rest. However, these results still confirm that our approach can defeat MONA in practice.

On the second part of our experiment, where we compared Gaston with the rest of the tools on collective benchmark of parametric families of formulae, Gaston managed to win over the other tools on many of their own benchmark formulae (see link for more detailed results).


  1. Elgaard, J., Klarlund, N., Møller, A.: MONA 1.x: new techniques for WS1S and WS2S
  2. Fiedor, T., Holik, L., Lengal, O., Vojnar, T.: Nested antichains for WS1S
  3. Ganzow, T., Kaiser, L.: New algorithm for weak monadic second-order logic on inductive structures.
  4. Traytel, D.: A coalgebraic decision procedure for WS1S
  5. D'Antoni, L., Veanes, M.: Minimization of symbolic automata
  6. Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND.
  7. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets

Contact

If you have any questions, do not hesitate to contact the tool/method authors:


Copyright (c) 2016 Tomas Fiedor <ifiedortom@fit.vutbr.cz>