eTheses Repository

Implementation of symbolic model checking for probabilistic systems

Parker, David Anthony (2003)
Ph.D. thesis, University of Birmingham.

PDF (1728Kb)


In this thesis, we present efficient implementation techniques for probabilistic model checking, a method which can be used to analyse probabilistic systems such as randomised distributed algorithms, fault-tolerant processes and communication networks. A probabilistic model checker inputs a probabilistic model and a specification, such as "the message will be delivered with probability 1", "the probability of shutdown occurring is at most 0.02" or "the probability of a leader being elected within 5 rounds is at least 0.98", and can automatically verify if the specification is true in the model. Motivated by the success of symbolic approaches to non-probabilistic model checking, which are based on a data structure called binary decision diagrams (BDDs), we present an extension to the probabilistic case, using multi-terminal binary decision diagrams (MTBDDs). We demonstrate that MTBDDs can be used to perform probabilistic analysis of large, structured models with more than 7.5 billion states, way out of the reach of conventional, explicit techniques, based on sparse matrices. We also propose a novel, hybrid approach, combining features of both symbolic and explicit implementations and show, using results from a wide range of case studies, that this technique can almost match the speed of sparse matrix based implementations, but uses significantly less memory. This increases, by approximately an order of magnitude, the size of model which can be handled on a typical workstation.

Type of Work:Ph.D. thesis.
Supervisor(s):Kwiatkowska, M. Z. (Marta Z.) (1957-)
School/Faculty:Schools (1998 to 2008) > School of Computer Science
Department:Computer Science
Subjects:QA75 Electronic computers. Computer science
Institution:University of Birmingham
Library Catalogue:Check for printed version of this thesis
ID Code:229
This unpublished thesis/dissertation is copyright of the author and/or third parties. The intellectual property rights of the author or third parties in respect of this work are as defined by The Copyright Designs and Patents Act 1988 or as modified by any successor legislation. Any use made of information contained in this thesis/dissertation must be in accordance with that legislation and must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the permission of the copyright holder.
Export Reference As : ASCII + BibTeX + Dublin Core + EndNote + HTML + METS + MODS + OpenURL Object + Reference Manager + Refer + RefWorks
Share this item :
QR Code for this page

Repository Staff Only: item control page