Model Checking Markov Chains: Techniques and Tools

I.S. Zapreev

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    933 Downloads (Pure)


    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
    • Katoen, Joost-Pieter, Supervisor
    • Brinksma, Ed, Supervisor
    Thesis sponsors
    Award date7 Mar 2008
    Place of PublicationZutphen
    Print ISBNs978-90-8570-298-6
    Publication statusPublished - 7 Mar 2008


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

    Cite this