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 journalArticleScientificpeer-review

5 Citations (Scopus)


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 languageEnglish
Pages (from-to)105-125
Number of pages21
JournalPerformance Evaluation
Issue number2
Publication statusPublished - Feb 2011
Externally publishedYes


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


Dive into the research topics of 'Time-bounded reachability in tree-structured QBDs by abstraction'. Together they form a unique fingerprint.

Cite this