Distributed Disk-Based Solution of Very Large Markov Chains

Research output: Contribution to journalArticleScientificpeer-review

12 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)177-196
Number of pages20
JournalFormal methods in system design
Issue number2/2
Publication statusPublished - 2006
Externally publishedYes


  • EWI-7868
  • IR-66559
  • METIS-238267


Dive into the research topics of 'Distributed Disk-Based Solution of Very Large Markov Chains'. Together they form a unique fingerprint.

Cite this