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.
- Queueing Theory
- Markov chains
- Probabilistic simulation
Klink, D., Remke, A. K. I., Haverkort, B. R. H. M., & Katoen, J. P. (2011). Time-bounded reachability in tree-structured QBDs by abstraction. Performance evaluation, 68(2), 105-125. https://doi.org/10.1016/j.peva.2010.04.002