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

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

View graph of relations

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.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Pages (from-to)113-125
StatePublished - 2010
CitationsWeb of Science® Times Cited: No match on DOI


  • LTL, satisfiability checking, incremental tableaux, implementation, one-pass tableaux
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 4870541