zbMATH — the first resource for mathematics

Reachability analysis of probabilistic systems by successive refinements. (English) Zbl 1007.68131
De Alfaro, Luca (ed.) et al., Process algebra and probabilistic methods. Performance modelling and verification. Joint international workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2165, 39-56 (2001).
Summary: 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.
For the entire collection see [Zbl 0971.00028].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link