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

DOI10.1007/S10703-006-0007-0MaRDI QIDQ2431769zbMATH OpenOpenAlexFDO

Authors Alexander Bell, B. R. Haverkort

Publication date 24 October 2006

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://research.utwente.nl/en/publications/distributed-diskbased-solution-of-very-large-markov-chains(2e956f97-5212-4459-9104-78a0cee3d827).html

zbMATH Keywords

CSL model checkingDisk-based algorithmsDistributed algorithmsMarkov chainsMatrix-vector productState-space generation

Mathematics Subject Classification ID

Markov chains (discrete-time Markov processes on discrete state spaces) (60J10) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed algorithms (68W15)

Recommendations

• Model-checking large structured Markov chains.
• Accelerated model checking of parametric Markov chains
• Theoretical Aspects of Computing - ICTAC 2004
• On the complexity of model checking interval-valued discrete time Markov chains
• Distributed Markovian bisimulation reduction aimed at CSL model checking
• scientific article; zbMATH DE number 2006656

Cites work

• A decomposition approach for stochastic reward net models
• A high-performance, portable implementation of the MPI message passing interface standard
• A probabilistic dynamic technique for the distributed generation of very large state spaces
• A symbolic out-of-core solution method for Markov models
• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 2090707 (Why is no real title available?)
• scientific article; zbMATH DE number 763717 (Why is no real title available?)
• scientific article; zbMATH DE number 814821 (Why is no real title available?)
• On the use of MTBDDs for performability analysis and verification of stochastic systems.

Cited in

(9)

• Model-checking large structured Markov chains.
• Uniformization and hypergraph partitioning for the distributed computation of response time densities in very large Markov models
• Sequential and distributed model checking of Petri net specifications
• Tackling large state spaces in performance modelling
• Explicit model checking of very large MDP using partitioning and secondary storage
• Performance evaluation of OpenMP-based algorithms for handling Kronecker descriptors
• Distributed Markov chains
• Validation of Stochastic Systems
• Distributed Markovian bisimulation reduction aimed at CSL model checking

Describes a project that uses

Uses Software

• MPI/MPICH

This page was built for publication: Distributed disk-based algorithms for model checking very large Markov chains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2431769)