Sciweavers

PE
2011
Springer

Time-bounded reachability in tree-structured QBDs by abstraction

13 years 7 months ago
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.
Daniel Klink, Anne Remke, Boudewijn R. Haverkort,
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where PE
Authors Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen
Comments (0)