Time-bounded reachability in tree-structured QBDs by abstraction

Daniel Klink, Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, Joost P. Katoen

    Research output: Contribution to journalArticleAcademicpeer-review

    5 Citations (Scopus)
    33 Downloads (Pure)


    This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performance evaluation. We determine time-bounded reachability probabilities in these processes–which with direct methods, i.e., uniformization, result in an exponential blow-up–by applying abstraction. We contrast abstraction based on Markov decision processes (MDPs) and interval-based abstraction; study various schemes to partition the state space, and empirically show their influence on the accuracy of the obtained reachability probabilities. Results show that grid-like schemes, in contrast to chain- and tree-like ones, yield extremely precise approximations for rather coarse abstractions.
    Original languageUndefined
    Pages (from-to)105-125
    Number of pages21
    JournalPerformance evaluation
    Issue number2
    Publication statusPublished - Feb 2011


    • EWI-18354
    • Queueing Theory
    • Reachability
    • IR-72833
    • Markov chains
    • Probabilistic simulation
    • METIS-271008
    • Abstraction

    Cite this