Time-Bounded Reachability in Tree-Structured QBDs by Abstraction

Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost P. Katoen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    209 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, results 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 languageEnglish
    Title of host publicationSixth International Conference on the Quantitative Evaluation of Systems, (QEST '09)
    Number of pages10
    ISBN (Print)978-0-7695-3808-2
    Publication statusPublished - Sept 2009
    Event6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary
    Duration: 13 Sept 200916 Sept 2009
    Conference number: 6


    Conference6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
    Abbreviated titleQEST
    Internet address


    Dive into the research topics of 'Time-Bounded Reachability in Tree-Structured QBDs by Abstraction'. Together they form a unique fingerprint.

    Cite this