Parallel Model Checking for LTL, CTL*, and Lmu2

Martin Leucker Rafal Somla Michael Weber


We describe a parallel model-checking algorithm for the fragment of the mu-calculus that allows one alternation of minimal and maximal fixed-point operators. This fragment is also known as Lmu2. Since LTL and CTL* can be encoded in this fragment, we obtain parallel model checking algorithms for practically important temporal logics. Our solution is based on a characterization of this problem in terms of two-player games. We exhibit the structure of their game-graphs and show that we can iteratively work with game graphs that have the same special structure as the ones obtained for Lmu1-formulae. Since good parallel algorithms for colouring game-graphs for Lmu1-formulae exist, it is straightforward to implement this algorithm in parallel and good run-time results can be expected.