@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.
}}