Distributed Model Checking for mu-calculus

Orna Grumberg, Tamir Heyman, Assaf Schuster

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


In this paper we propose a distributed symbolic algorithm for model checking of propositional mu--calculus formulas. mu-calculus is a powerful formalism and many problems like (fair) CTL and LTL model checking can be solved using the mu--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 is based on distributed evaluation of 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 enabling 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. Several further ingredients (such as the parallelization of the slicing procedure), are omitted for lack of space.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems