Homepage: http://www.daxc.de/eth

Experimental Results

Contents

  1. Obligation Formulas
  2. Experimental Evaluation
    1. Experiment 1: Comparing Automata Sizes of LTL to Automata Translators
    2. Experiment 2: Performance for Finite State Model Checking

Obligation Formulas

  Formulas (SPIN syntax) Results on negated formulas
12 formulas from Etessami and Holzmann [bib] eh_spin.txt survey_eh.txt
27 formulas from Somenzi and Bloem [bib] sb_spin.txt survey_sb.txt
50 patterns of commonly used specification formulas [link] patterns_spin.txt survey_patterns.txt


  # of formulas safety guarantee obligation
eh 12 3 (25%) 1 (8%) 4 (33%)
sb 27 8 (30%) 9 (33%) 15 (56%)
patterns 55 36 (65%) 1 (2%) 40 (73%)

Experimental Evaluation

For both experiments we used a computer with an Intel Pentium 4 processor with 3GHz and with 4GBytes of main memory.

Used LTL to Automata Translators:

  
SPINhttp://spinroot.com/spin/whatispin.html
TMPhttp://www1.bell-labs.com/project/TMP/
LTL2BAhttp://spinroot.com/spin/Man/README.html
MODELLAhttp://www.science.unitn.it/~stonetta/modella.html
WDBAhttp://www.inf.ethz.ch/personal/daxc/wdba/

Experiment 1: Comparing Automata Sizes of LTL to Automata Translators

Each row corresponds to the i-th formula in patterns40_spin.txt. The numbers denote the sizes of the resulting automata.

 1234567891011121314151617181920
SPIN 2 3 3 4 6 1 6 3 7 36 -- -- -- -- 2 3 3 4 6 4
TMP 2 3 3 4 3 1 2 3 3 6 7 7 8 7 2 3 3 4 3 4
LTL2BA 2 3 3 4 3 1 2 3 3 6 7 12 8 7 2 3 3 4 3 4
MODELLA 2 3 3 5 4 1 2 2 4 6 7 7 9 11 2 3 3 5 4 4
WDBA 2 3 3 4 3 1 2 2 3 6 7 7 8 7 2 3 3 4 3 4


 2122232425262728293031323334353637383940
SPIN 3 4 6 7 8 14 6 40 7 15 8 4 82 5 16 9 15 16 15 --
TMP 3 4 3 3 4 3 4 4 5 4 3 4 22 5 4 5 4 5 4 5
LTL2BA 3 4 3 3 4 3 4 4 5 4 4 4 10 5 14 5 4 5 4 5
MODELLA 3 5 4 3 6 3 4 4 6 5 4 5 5 7 23 5 4 8 4 10
WDBA 3 4 3 3 4 3 4 4 5 4 3 4 4 5 4 5 4 5 4 5


Automata Sizes of 40 Obligation Formulas



  Formulas (SPIN syntax)
50 patterns of commonly used specification formulas [link] patterns_spin.txt
40 obligation formulas from patterns patterns40_spin.txt
40 automata sizes for SPIN sizes40_spin.txt
40 automata sizes for TMP sizes40_tmp.txt
40 automata sizes for LTL2BA sizes40_ltl2ba.txt
40 automata sizes for MODELLA sizes40_modella.txt
40 automata sizes for WDBA sizes40_wdba.txt

Experiment 2: Performance for Finite State Model Checking

1. bopdb

A detailed description can be found at http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=bopdp

Specification:

Automata generated by the translators:

Models:

Performance (Time/Memory):
  SPIN TMP LTL2BA MODELLA WDBA
bopdp.7.pm 0m05/172 MB 0m05/172 MB 0m05/172 MB 0m05/172 MB 0m03/155 MB
bopdp.14.pm 0m21/367 MB 0m21/367 MB 0m21/367 MB 0m21/367 MB 0m13/297 MB
bopdp.28.pm 1m32/1146 MB 1m32/1146 MB 1m32/1146 MB 1m32/1146 MB 0m55/877 MB
bopdp.56.pm* 14m04/2856 MB 14m04/2856 MB 14m04/2856 MB 14m04/2856 MB 8m05/2112 MB
* with SPIN option -DCOLLAPSE
2. elevator2

A detailed description can be found at http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=elevator2

Specification (SPIN syntax):

Automata generated by the translators:

* note that the specification is not an obligation formula. However, we can use the WDBA construction to obtain a small weak Büchi automaton:
  1. We negate the specification and push the negation inside the [] operator: "≤≥ ! (r0 -> (!p0 U (p0 U (!p0 U (p0 U (p0 /\ co))))))".
  2. The formula after the [] operator is an obligation formula. We translate it to a WDBA
  3. We add a new initial state q to the WDBA with transitions from q to q and from q to the old initial state of the WDBA

Models:

Performance (Time/Memory):
  SPIN TMP LTL2BA MODELLA WDBA
elevator2.1.pm 0m00/112 MB 0m00/368 MB 0m00/240 MB 0m01/368 MB 0m00/240 MB
elevator2.2.pm 0m00/240 MB 0m01/368 MB 0m00/240 MB 0m01/369 MB 0m00/240 MB
elevator2.3.pm 5m57/1667 MB 2m42/1182 MB 2m42/1054 MB 2m28/1149 MB 2m26/1021 MB
elevator2.4.pm* >3000 MB 6m41/2162 MB 7m16/2107 MB 7m19/2235 MB 6m31/2034 MB
elevator2.5.pm*          
* with SPIN option -DCOLLAPSE
3. giop

A detailed description can be found in [bib].

Specifications (SPIN syntax):

Automata generated by the translators:

The model:

Performance (Time/Memory):
  SPIN TMP LTL2BA MODELLA WDBA
giop3.pm >3000 MB 0m04/378 MB 0m13/664 MB >3000 MB 0m06/350 MB
4. signarch

A detailed description can be found in [bib].

The specifications:

Automata generated by the translators:

The model:

Performance (Time/Memory):
  SPIN TMP LTL2BA MODELLA WDBA
Specification 1* 7m09/1058 MB 7m07/1058 MB 7m07/1058 MB 7m10/1061 MB 4m55/779 MB
Specification 2* 17m57/2003 MB 14m25/2003 MB 14m23/2003 MB 14m09/2003 MB 5m17/788 MB
* with SPIN option -DCOLLAPSE