Tableau-based decision procedure for linear time temporal logic: implementation, testing, performance analysis and optimisation

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.