For the most recent entries see the Petri Nets Newsletter.

Distributed disk-based algorithms for model checking very large Markov chains.

Bell, Alexander; Haverkort, Boudewijn R.

In: Formal Methods in System Design, Volume 29, 2, 2006, pages 177-196. September 2006. URL:

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.

Keywords: Markov chains; Matrix-vector product; Disk-based algorithms; State-space generation; CSL model checking; Distributed algorithms.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography