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

Motivation

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.

Goal

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

Student

Stefan Mau

Tutor


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