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