Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/QEST.2009.9 | Perform. Eval. |
Keywords | DocType | Volume |
continuous time markov chain,markov decision process,reachability,tree structure,state space,queueing theory,direct method,model checking,markov chain,abstraction,markov chains,pushdown automata | Journal | 68 |
Issue | ISSN | Citations |
2 | 0166-5316 | 2 |
PageRank | References | Authors |
0.40 | 18 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Klink | 1 | 72 | 3.40 |
| Anne Remke | 2 | 175 | 23.96 |
| Boudewijn R. Haverkort | 3 | 1205 | 117.45 |
| Joost-Pieter Katoen | 4 | 4444 | 289.65 |