Time-Bounded Reachability in Tree-Structured QBDs by Abstraction

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

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

    Publication series

    PublisherIEEE Computer Society


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


    • METIS-264128
    • EWI-16466
    • IR-68308

    Cite this