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

DOI10.1007/S10703-006-0007-0zbMATH Open1110.68071OpenAlexW2131837991MaRDI QIDQ2431769FDOQ2431769

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

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

zbMATH Keywords

Markov chainsDistributed algorithmsMatrix-vector productCSL model checkingDisk-based algorithmsState-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) Distributed algorithms (68W15) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A high-performance, portable implementation of the MPI message passing interface standard
• Title not available (Why is that?)
• Title not available (Why is that?)
• A symbolic out-of-core solution method for Markov models
• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• A decomposition approach for stochastic reward net models
• A probabilistic dynamic technique for the distributed generation of very large state spaces
• Title not available (Why is that?)

Cited In (9)

• Model-checking large structured Markov chains.
• 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
• Distributed Markovian bisimulation reduction aimed at CSL model checking
• Uniformization and hypergraph partitioning for the distributed computation of response time densities in very large Markov models
• Validation of Stochastic Systems
• Sequential and distributed model checking of Petri net specifications
• Tackling large state spaces in performance modelling

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)