Evaluating LTL Satisfiability Solvers

This page contains additional material for the following paper:

V. Schuppan and L. Darmawan: Evaluating LTL Satisfiability Solvers. In: T. Bultan, P.-A. Hsiung (eds.): Automated Technology for Verification and Analysis - 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Volume 6996 of Lecture Notes in Computer Science, pp. 397-413. Springer, 2011. Download: publisher, preprint (zipped), full (zipped)

Raw Data

This file contains the raw data of the main stage of our evaluation.

Tables and Plots

The following documents collect additional tables and plots of our data from the main stage of our evaluation.

Link Size No. Pages
Tables of aggregated perfomance data pdf 16 MB 689
Cactus plots pdf 163 MB 14556
Line plots pdf 229 MB 14556
Scatter plots - non-negated versus negated versions pdf 38 MB 4931
Scatter plots - model construction disabled versus enabled pdf 12 MB 1312
Scatter plots - winning configurations pdf 44 MB 4777
Scatter plots - tools (no TRP++) pdf 125 MB 13401
Scatter plots - tools (TRP++ s, r) pdf 127 MB 14171
Scatter plots - tools (TRP++ no s, r) pdf 127 MB 14171
Scatter plots - tools (TRP++ no s, no r) pdf 125 MB 14171

Benchmarks

The following table provides links to the sources of our benchmarks as well as to archives containing the benchmarks in the formats of the respective solvers. This file contains all families in all formats.

Benchmark Family Homepage Archive for
ALASKA LWB NuSMV pltl TRP++ TSPASS
acacia Link tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2
alaska Link tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2
anzu Link tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2
forobots not available tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2
rozier Link tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2
schuppan not available tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2
trp Link tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2 tar.bz2

Solvers

ALASKA, LWB, NuSMV, pltl, TRP++, TSPASS.

Support

This work was partly funded by the Provincia Autonoma di Trento (project EMTELOS).