Distributed Disk-Based Solution of Very Large Markov Chains

Research output: Contribution to journalArticleScientificpeer-review

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

Fingerprint

Markov processes
Model checking
Petri nets
Message passing
Parallel algorithms
Data structures
Specifications
Data storage equipment

Keywords

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

Cite this

@article{199f24627d74408a90ff1690131b3f57,
title = "Distributed Disk-Based Solution of Very Large Markov Chains",
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 = "EWI-7868, IR-66559, METIS-238267",
author = "A. Bell and Haverkort, {Boudewijn R.H.M.}",
note = "Imported from research group DACS (ID number 430) M1 - 10.1007/s10703-006-0007-0",
year = "2006",
doi = "10.1007/s10703-006-0007-0",
language = "English",
volume = "29",
pages = "177--196",
journal = "Formal methods in system design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "2/2",

}

Distributed Disk-Based Solution of Very Large Markov Chains. / Bell, A.; Haverkort, Boudewijn R.H.M.

In: Formal methods in system design, Vol. 29, No. 2/2, 2006, p. 177-196.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

T1 - Distributed Disk-Based Solution of Very Large Markov Chains

AU - Bell, A.

AU - Haverkort, Boudewijn R.H.M.

N1 - Imported from research group DACS (ID number 430) M1 - 10.1007/s10703-006-0007-0

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - EWI-7868

KW - IR-66559

KW - METIS-238267

U2 - 10.1007/s10703-006-0007-0

DO - 10.1007/s10703-006-0007-0

M3 - Article

VL - 29

SP - 177

EP - 196

JO - Formal methods in system design

JF - Formal methods in system design

SN - 0925-9856

IS - 2/2

ER -