Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis

Publication: Research - peer-reviewJournal article – Annual report year: 2010

Standard

Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis. / Goranko, Valentin; Kyrilov, Angelo; Shkatov, Dmitry.

In: Electronic Notes in Theoretical Computer Science, Vol. 262, 2010, p. 113-125.

Publication: Research - peer-reviewJournal article – Annual report year: 2010

Harvard

APA

CBE

MLA

Vancouver

Author

Goranko, Valentin; Kyrilov, Angelo; Shkatov, Dmitry / Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis.

In: Electronic Notes in Theoretical Computer Science, Vol. 262, 2010, p. 113-125.

Publication: Research - peer-reviewJournal article – Annual report year: 2010

Bibtex

@article{559d31e8ebab45a9ab860d5b4899c1da,
title = "Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis",
publisher = "Elsevier BV",
author = "Valentin Goranko and Angelo Kyrilov and Dmitry Shkatov",
year = "2010",
doi = "10.1016/j.entcs.2010.04.009",
volume = "262",
pages = "113--125",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",

}

RIS

TY - JOUR

T1 - Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis

A1 - Goranko,Valentin

A1 - Kyrilov,Angelo

A1 - Shkatov,Dmitry

AU - Goranko,Valentin

AU - Kyrilov,Angelo

AU - Shkatov,Dmitry

PB - Elsevier BV

PY - 2010

Y1 - 2010

N2 - We report on the implementation and experimental analysis of an incremental multi-pass tableau-based procedure `a la Wolper for testing satisfiability in the linear time temporal logic LTL, based on a breadthfirst search strategy. We describe the implementation and discuss the performance of the tool on several series of pattern formulae, as well as on some random test sets, and compare its performance with an implementation of Schwendimann’s one-pass tableaux by Widmann and Gor´e on several representative series of pattern formulae, including eventualities and safety patterns. Our experiments have established that Schwendimann’s algorithm consistently, and sometimes dramatically, outperforms the incremental tableaux, despite the fact that the theoretical worst-case upper-bound of Schwendimann’s algorithm, 2EXPTIME, is worse than that of Wolper’s algorithm, which is EXPTIME. This shows, once again, that theoretically established worst-case complexity results do not always reflect truly the practical efficiency, at least when comparing decision procedures.

AB - We report on the implementation and experimental analysis of an incremental multi-pass tableau-based procedure `a la Wolper for testing satisfiability in the linear time temporal logic LTL, based on a breadthfirst search strategy. We describe the implementation and discuss the performance of the tool on several series of pattern formulae, as well as on some random test sets, and compare its performance with an implementation of Schwendimann’s one-pass tableaux by Widmann and Gor´e on several representative series of pattern formulae, including eventualities and safety patterns. Our experiments have established that Schwendimann’s algorithm consistently, and sometimes dramatically, outperforms the incremental tableaux, despite the fact that the theoretical worst-case upper-bound of Schwendimann’s algorithm, 2EXPTIME, is worse than that of Wolper’s algorithm, which is EXPTIME. This shows, once again, that theoretically established worst-case complexity results do not always reflect truly the practical efficiency, at least when comparing decision procedures.

KW - LTL, satisfiability checking, incremental tableaux, implementation, one-pass tableaux

UR - http://dx.doi.org/10.1016/j.entcs.2010.04.009

U2 - 10.1016/j.entcs.2010.04.009

DO - 10.1016/j.entcs.2010.04.009

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

VL - 262

SP - 113

EP - 125

ER -