Distributed symbolic model checking for μ-calculus

Abstract

In this paper we propose a distributed symbolic algorithm for model checking of propositional μ-calculus formulas. μ-calculus is a powerful formalism and many problems like (fair) CTL and LTL model checking can be solved using the μ-calculus model checking. Previous works on distributed symbolic model checking were restricted to reachability analysis and safety properties. This work thus significantly extends the scope of properties that can be verified for very large designs. The algorithm distributively evaluates subformulas. It results in sets of states which are evenly distributed among the processes.We show that this algorithm is scalable, and thus can be implemented on huge distributed clusters of computing nodes. In this way, the memory modules of the computing nodes collaborate to create a very large store, thus enables the checking of much larger designs. We formally prove the correctness of the parallel algorithm. We complement the distribution of the state sets by showing how to distribute the transition relation.