tr-announce

Download

tr-announce@lists.rwth-aachen.de

January 2007

1 participants
1 discussions

2006-02: Parallel Algorithms for Verification of Large Systems
by Peter Schneider-Kamp 26 Jan '07

26 Jan '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: Parallel Algorithms for Verification of Large Systems Michael Weber AIB 2006-02 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.

1 0