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

  • Barnat J
  • Brim L
  • Ročkai P
  • 7


    Mendeley users who have this article in their library.
  • 5


    Citations of this article.


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) [1], we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments.

Author-supplied keywords

  • Explicit model checking
  • On-the-fly
  • Parallel
  • Partial order reduction

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Jií Barnat

  • Luboš Brim

  • Petr Ročkai

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free