TY - JOUR
T1 - Reachability Analysis of Probabilistic Systems
AU - D'Argenio, P. R.
AU - Jeanett, B.
AU - Jensen, Henrik Ejersbo
AU - Larsen, Kim Guldstrand
PY - 2001
Y1 - 2001
N2 - We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called {essential states}, and heuristic strategies for guiding the refinement process.
AB - We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called {essential states}, and heuristic strategies for guiding the refinement process.
M3 - Journal article
SN - 1611-3349
VL - 2165
SP - 39
EP - 56
JO - Lecture Notes in Computer Science: Process Algebra and Probabilistic Methods, Performance Modelling and Verification
JF - Lecture Notes in Computer Science: Process Algebra and Probabilistic Methods, Performance Modelling and Verification
ER -