Distributed Disk-Based Solution of Very Large Markov Chains

Bell, Alexander and Haverkort, Boudewijn R. (2006) Distributed Disk-Based Solution of Very Large Markov Chains. Formal Methods in System Design, 29 (2). pp. 177-196. ISSN 0925-9856

Preview

PDF
403Kb

Abstract:	In this paper we present data structures and distributed algorithms for CSL model checking-based performance and dependability evaluation. We show that all the necessary computations are composed of series or sums of matrix-vector products. We discuss sparse storage structures for the required matrices and present efficient sequential and distributed disk-based algorithms for performing these matrix-vector products. We illustrate the effectivity of our approach in a number of case studies in which continuous-time Markov chains (generated in a distributed way from stochastic Petri net specifications) with several hundreds of millions of states are solved on a workstation cluster with 26 dual-processor nodes. We show details about the memory consumption, the solution times, and the speedup. The distributed message-passing algorithms have been implemented in a tool called PARSECS, that also takes care of the distributed Markov chain generation and that can also be used for distributed CTL model checking of Petri nets.
Item Type:	Article
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Design and Analysis of Communication Systems (DACS)
Link to this item:	http://purl.utwente.nl/publications/66559
Official URL:	http://dx.doi.org/10.1007/s10703-006-0007-0
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 238267