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

DSpace/Manakin Repository

Show simple item record

dc.contributor.author Kyrilov, Angelo
dc.date.accessioned 2011-06-10T09:17:51Z
dc.date.available 2011-06-10T09:17:51Z
dc.date.issued 2011-06-10
dc.identifier.uri http://hdl.handle.net/10539/10075
dc.description.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. en_US
dc.language.iso en en_US
dc.title Tableau-based decision procedure for linear time temporal logic: implementation, testing, performance analysis and optimisation en_US
dc.type Thesis en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search WIReDSpace


Advanced Search

Browse

My Account

Statistics