Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking

Volendam, The Netherlands October 04-October 08

DOI Bookmark:

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

12th IEEE International Symposium on ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	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

	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

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.