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.
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.
Stefan Mau