DJJL02

P. D'Argenio, B. Jeannet, H.E. Jensen, K.G. Larsen. Reduction and Refinement Strategies for Probabilistic Analysis. In Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBMIV 2002, LNCS, Volume 2399, Copenhagen, Denmark, July 2002.

Download [help]

Download paper: Gziped Postscript

Copyright notice: This 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.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

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

Contact

Bertrand Jeannet http://www.irisa.fr/prive/bjeannet

BibTex Reference

@InProceedings{DJJL02,
   Author = {D'Argenio, P. and Jeannet, B. and Jensen, H.E. and Larsen, K.G.},
   Title = {Reduction and Refinement Strategies for Probabilistic Analysis},
   BookTitle = {Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBMIV 2002},
   Volume = {2399},
   Series = {LNCS},
   Address = {Copenhagen, Denmark},
   Month = {July},
   Year = {2002}
}

EndNote Reference [help]

Get EndNote Reference (.ref)