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

Valentin Goranko, Angelo Kyrilov, Dmitry Shkatov

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    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
    Volume262
    Pages (from-to)113-125
    ISSN1571-0661
    DOIs
    Publication statusPublished - 2010

    Keywords

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

    Cite this