Treffer: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties

Abstract: One of the most important open problems of parallel LTL model checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would provide the same optimality we have in sequential LTL model checking. In this paper we give a partial solution to the problem: we propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Büchi automata. In addition to the previous version of the paper (Barnat et al., 2009) , we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments. [Copyright &y& Elsevier]