Distributed Disk-Based Solution of Very Large Markov Chains

A. Bell, Boudewijn R.H.M. Haverkort

    Research output: Contribution to journalArticleAcademicpeer-review

    12 Citations (Scopus)
    221 Downloads (Pure)


    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 languageUndefined
    Article number10.1007/s10703-006-0007-0
    Pages (from-to)177-196
    Number of pages20
    JournalFormal methods in system design
    Issue number2/2
    Publication statusPublished - 2006


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

    Cite this