Time-bounded reachability in tree-structured QBDs by abstraction

Structured QBDs by Abstraction Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Fellow, IEEE, and Joost-Pieter Katoen, Member, IEEE Computer Society —This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These treestructured 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 ial blow-up— by applying abstraction. We contrast ion based on Markov decision processes (MDPs) and -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 gridlike schemes, in contrast to chain- and tree-like ones, yield y precise approximations for rather coarse abstractions.

• Type: Journal
• Year: 2011
• Where: PE
• Authors: Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen
• Keywords: Abstractions, Markov Chains, Optimization, PE 2011, Reachability Probabilities