Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Marta Kwiatkowska Articles by David Parker Articles by Yi Zhang Articles by Rashid Mehmood

12th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04)

Volendam, The Netherlands

October 04-October 08

ISBN: 0-7695-2251-3

	ASCII Text	x
	Marta Kwiatkowska, David Parker, Yi Zhang, Rashid Mehmood, "Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking," Modeling, Analysis, and Simulation of Computer Systems, International Symposium on, pp. 123-130, 12th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04), 2004.

	BibTex	x
	@article{ 10.1109/MASCOT.2004.1348189, author = {Marta Kwiatkowska and David Parker and Yi Zhang and Rashid Mehmood}, title = {Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking}, journal ={Modeling, Analysis, and Simulation of Computer Systems, International Symposium on}, volume = {0}, year = {2004}, issn = {1526-7539}, pages = {123-130}, doi = {http://doi.ieeecomputersociety.org/10.1109/MASCOT.2004.1348189}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Modeling, Analysis, and Simulation of Computer Systems, International Symposium on TI - Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking SN - 1526-7539 SP123 EP130 A1 - Marta Kwiatkowska, A1 - David Parker, A1 - Yi Zhang, A1 - Rashid Mehmood, PY - 2004 KW - null VL - 0 JA - Modeling, Analysis, and Simulation of Computer Systems, International Symposium on ER -

Marta Kwiatkowska, University of Birmingham

David Parker, University of Birmingham

Yi Zhang, University of Birmingham

Rashid Mehmood, University of Cambridge

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MASCOT.2004.1348189

In this paper, we describe the dual-processor parallelisation of a symbolic (BDD-based) implementation of probabilistic model checking. We use multi-terminal BDDs, which allow a compact representation of large, structured Markov chains. We show that they also provide a convenient block decomposition of the Markov chain which we use to implement a parallelised version of the Gauss-Seidel iterative method. We provide experimental results on a range of case studies to illustrate the effectiveness of the technique, observing an average speed-up of 1.8 with two processors. Furthermore, we present an optimisation for our method based on preconditioning.

Citation:

Marta Kwiatkowska, David Parker, Yi Zhang, Rashid Mehmood, "Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking," mascots, pp.123-130, 12th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04), 2004

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.