Tableau Tool for Testing Satisfiability in LTL: Implementation and Experimental Analysis

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. 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

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Valentin Goranko, Angelo Kyrilov, Dmitry Shkatov
• Keywords: ENTCS 2010, Multi-pass Tableau-based Procedure, Pattern Formulae, Temporal Logic Ltl