Tableau-based decision procedure for linear time temporal logic: implementation, testing, performance analysis and optimisation
Date
2011-06-10
Authors
Kyrilov, Angelo
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
This thesis reports on the implementation and experimental analysis of an
incremental multi-pass tableau-based procedure a la Wolper for testing satis-
ability in the linear time temporal logic LTL, based on a breadth- rst search
strategy. I 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. The experiments have
established that Schwendimann's algorithm consistently, and sometimes dra-
matically, outperforms the incremental tableaux, despite the fact that the the-
oretical 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 re
ect truly the practical e ciency, at least when comparing decision
procedures.