Clusters on the basis of regular PCs are widely used by now. As the approach of model checking consumes alot of memory and is computationally intensive, it is reasonable to think about parallelizing the algorithms that have been used in [mc]square.
The goal of this thesis is the parallelization of the model checker [mc]square. Your first task is to create an overview of parallel algorithms for CTL model-checking. After that you're supposed to compare the different approaches with each other and examine which of the approaches is the best to implement. Finally, you shall convert it into [mc]square.
Stefan Mau