@techreport{Weber:2006a,
Author = {Michael Weber},
Institution = {RWTH Aachen University},
Keywords = {Verification, Model Checking, Games, mu-Calculus, parallel algorithms},
Month = {12},
Number = {AIB-2006-02},
Title = {Parallel Algorithms for Verification of Large Systems},
Url = {http://aib.informatik.rwth-aachen.de/2006/2006-02.pdf},
Year = {2006},
Abstract = {The model-checking problem is the question whether a given system model satisfies a property. The property is usually given as formula of a temporal logic, and the system model as labelled transition system. However, the well-known state-space explosion effect is responsible for yielding transition systems of exponential size when compared to their description, and common sequential algorithms often are not capable to solve the model-checking problem with resources available on a single computer.
In this thesis, we develop parallel and, in particular, distributed algorithms which exploit the combined resources of a network of commodity workstations to solve problem instances which are beyond the capabilities of today's sequential algorithms.
In a second part, we investigate ways to efficiently generate (low-level) transition systems suitable for many verification tools from compact high-level descriptions of the input model. We propose a virtual-machine based approach, which uses an intermediate format to break the translation from high-level to low-level representations of a model into two steps. This well-known compiler technique simplifies the translation and still is very fast in practice.
}}