Model Checking Markov Chains: Techniques and Tools

I.S. Zapreev

Abstract

This dissertation deals with four important aspects of model checking Markov chains: the development of efficient model-checking tools, the improvement of model-checking algorithms, the efficiency of the state-space reduction techniques, and the development of simulation-based model-checking procedures. First, we introduce MRMC, a model checker for DMRMs and CMRMs, that supports reward extensions of PCTL and CSL. We study the efficiency of the tool in comparison with probabilistic model checkers such as E ⊢MC^2, PRISM, Ymer and VESTA, and focus on fully probabilistic systems. Further, we provide a precise procedure for steady-state detection for time-bounded reachability on CTMCs. After that we study the effect of bisimulation minimization in model checking of monolithic DTMCs, CTMCs and the variants thereof with rewards. We conclude our work by deriving techniques based on discrete-event simulation and sequential confidence intervals for model checking CSL properties on CTMCs.
Original languageUndefined
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Katoen, Joost P., Supervisor
  • Brinksma, Hendrik , Supervisor
Sponsors
Date of Award7 Mar 2008
Place of PublicationZutphen
Publisher
Print ISBNs978-90-8570-298-6
DOIs
StatePublished - 7 Mar 2008

Fingerprint

Model checking
Discrete event simulation
Markov processes

Keywords

  • METIS-251051
  • EWI-13000
  • IR-58974

Cite this

Zapreev, I. S. (2008). Model Checking Markov Chains: Techniques and Tools Zutphen: Woehrmann Printing Service DOI: 10.3990/1.9789085702986
Zapreev, I.S.. / Model Checking Markov Chains: Techniques and Tools. Zutphen : Woehrmann Printing Service, 2008. 229 p.
@misc{70fec899eeb44fcb9dc2c234ba267978,
title = "Model Checking Markov Chains: Techniques and Tools",
abstract = "This dissertation deals with four important aspects of model checking Markov chains: the development of efficient model-checking tools, the improvement of model-checking algorithms, the efficiency of the state-space reduction techniques, and the development of simulation-based model-checking procedures. First, we introduce MRMC, a model checker for DMRMs and CMRMs, that supports reward extensions of PCTL and CSL. We study the efficiency of the tool in comparison with probabilistic model checkers such as E ⊢MC^2, PRISM, Ymer and VESTA, and focus on fully probabilistic systems. Further, we provide a precise procedure for steady-state detection for time-bounded reachability on CTMCs. After that we study the effect of bisimulation minimization in model checking of monolithic DTMCs, CTMCs and the variants thereof with rewards. We conclude our work by deriving techniques based on discrete-event simulation and sequential confidence intervals for model checking CSL properties on CTMCs.",
keywords = "METIS-251051, EWI-13000, IR-58974",
author = "I.S. Zapreev",
note = "10.3990/1.9789085702986",
year = "2008",
month = "3",
doi = "10.3990/1.9789085702986",
isbn = "978-90-8570-298-6",
publisher = "Woehrmann Printing Service",
school = "University of Twente",

}

Zapreev, IS 2008, 'Model Checking Markov Chains: Techniques and Tools', University of Twente, Zutphen. DOI: 10.3990/1.9789085702986

Model Checking Markov Chains: Techniques and Tools. / Zapreev, I.S.

Zutphen : Woehrmann Printing Service, 2008. 229 p.

Research output: ScientificPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Model Checking Markov Chains: Techniques and Tools

AU - Zapreev,I.S.

N1 - 10.3990/1.9789085702986

PY - 2008/3/7

Y1 - 2008/3/7

N2 - This dissertation deals with four important aspects of model checking Markov chains: the development of efficient model-checking tools, the improvement of model-checking algorithms, the efficiency of the state-space reduction techniques, and the development of simulation-based model-checking procedures. First, we introduce MRMC, a model checker for DMRMs and CMRMs, that supports reward extensions of PCTL and CSL. We study the efficiency of the tool in comparison with probabilistic model checkers such as E ⊢MC^2, PRISM, Ymer and VESTA, and focus on fully probabilistic systems. Further, we provide a precise procedure for steady-state detection for time-bounded reachability on CTMCs. After that we study the effect of bisimulation minimization in model checking of monolithic DTMCs, CTMCs and the variants thereof with rewards. We conclude our work by deriving techniques based on discrete-event simulation and sequential confidence intervals for model checking CSL properties on CTMCs.

AB - This dissertation deals with four important aspects of model checking Markov chains: the development of efficient model-checking tools, the improvement of model-checking algorithms, the efficiency of the state-space reduction techniques, and the development of simulation-based model-checking procedures. First, we introduce MRMC, a model checker for DMRMs and CMRMs, that supports reward extensions of PCTL and CSL. We study the efficiency of the tool in comparison with probabilistic model checkers such as E ⊢MC^2, PRISM, Ymer and VESTA, and focus on fully probabilistic systems. Further, we provide a precise procedure for steady-state detection for time-bounded reachability on CTMCs. After that we study the effect of bisimulation minimization in model checking of monolithic DTMCs, CTMCs and the variants thereof with rewards. We conclude our work by deriving techniques based on discrete-event simulation and sequential confidence intervals for model checking CSL properties on CTMCs.

KW - METIS-251051

KW - EWI-13000

KW - IR-58974

U2 - 10.3990/1.9789085702986

DO - 10.3990/1.9789085702986

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-8570-298-6

PB - Woehrmann Printing Service

ER -

Zapreev IS. Model Checking Markov Chains: Techniques and Tools. Zutphen: Woehrmann Printing Service, 2008. 229 p. Available from, DOI: 10.3990/1.9789085702986