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.
