Name
Abstract | ||
|---|---|---|
We report on a novel development to model check quantitative reachability properties on Markov decision processes together with its prototype implementation. The innovation of the technique is that the analysis is performed on an abstraction of the model under analysis. Such an abstraction is significantly smaller than the original model and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis necessary to determine the validity of the property is more costly than the refinement process, the technique profits from applying such numerical analysis on smaller state spaces. |
Year | Venue | Keywords |
|---|---|---|
2001 | PAPM-PROBMIV | quantitative reachability property,markov decision,probabilistic systems,original model,numerical analysis,novel development,prototype implementation,reachability analysis,refinement process,required property,smaller state space,successive refinements,technique profit,model checking,state space,profitability,markov decision process |
Field | DocType | ISBN |
Discrete mathematics,Path (graph theory),Model checking,Abstraction,Computer science,Markov decision process,Algorithm,Reachability,Probabilistic logic,Numerical analysis,Process calculus | Conference | 3-540-42556-X |
Citations | PageRank | References |
91 | 3.69 | 17 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pedro R. D'Argenio | 1 | 1004 | 63.53 |
| Bertrand Jeannet | 2 | 641 | 29.06 |
| Henrik Ejersbo Jensen | 3 | 212 | 16.17 |
| Kim Guldstrand Larsen | 4 | 4434 | 346.88 |