====== Paralleler und verteilter Aufbau des Zustandsraums im Model-Checker [mc]square ======
~~NOTOC~~
===== Motivation =====

Cluster auf Basis von normalen PC's sind mittlerweile weit verbreitet. Da die Methode des Model-Checkings sehr speicher- und rechenintensiv ist, macht es Sinn über eine Parallelisierung der in [mc]square verwendenten Algorithmen nachzudenken.

===== Ziel der Arbeit =====

Das Ziel dieser Arbeit ist es den Model-Checker [mc]square zu parallelisieren. Zu Beginn der Arbeit sollte eine Übersicht über parallele Algorithmen für CTL Model-Checking erstellt werden. Danach müssen die verschiedenen Ansätze miteinander verglichen werden und geprüft werden, welcher Ansatz am besten umzusetzen ist. Im Anschluss sollte eine Umsetzung in [mc]square erfolgen.

===== Studienrichtung =====

  * Informatik 

===== Vorkenntnisse =====

  * Java
  * Programmieren von parallelen Programmen
  * ggf. Model-Checking

===== Student =====
Stefan Mau

===== Betreuer =====

  * [[:lehrstuhl:mitarbeiter:schlich]]