This paper presents a scalable method for parallel symbolic on-the-fly
model checking on a distributed-memory environment of workstations.
Our method combines a parallel version of the model checker for RCTL
safety properties with a scalable scheme for reachability analysis.
The extra load of storage required for counter example generation
is evenly distributed among the processes by our memory balancing.
For the sake of scalability, at no point during computation the memory
of a single process contains all the data from any of the cycles.
The counter example generation is thus performed through collaboration
of the parallel processes.
We develop a method for the counter example generation keeping a
low peak memory requirement during the backward step and the
computation of the inverse transition relation.
We implemented our method on a standard, loosely-connected environment
of workstations, using a high-performance SMV-based model checker.
Our initial performance evaluation using several large circuits shows
that our method can check models that are too large to fit
in the memory of a single node.
Our on-the-fly approach may find counter examples even when the
model is too large to fit in the memory of the parallel system.