Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Gziped Postscript (.ps.gz)
Copyright noticeThis material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
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.
Bertrand Jeannet
Bertrand.Jeannet@irisa.fr
@InProceedings{jeannet01a,
Author = {D'Argenio, P.R. and Jeannet, B. and Jensen, H.E. and Larsen, K.J.},
Title = {Reachability Analysis of Probabilistic Systems by Successive Refinements},
BookTitle = {Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBM 2001},
Volume = {2165},
Series = {LNCS},
Address = {Aachen, Germany},
Month = {September},
Year = {2001}
}
Get EndNote Reference (.ref)