tr-announce January 2007

tr-announce@lists.rwth-aachen.de

1 participants
1 discussions

2006-02: Parallel Algorithms for Verification of Large Systems

by Peter Schneider-Kamp

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.

17 years, 8 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce January 2007