Parallel and Distributed Construction of the State Spaces in the Model Checker [mc]square


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.

Fields of Study

  • Computer science

Required Knowledge

  • Java
  • Programming of parallel programs
  • Model checking if applicable


Stefan Mau


This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany