loading...
APMC 3.0: Approximate Verification of Discrete and Continuous Time Markov Chains
Riverside, California September 11-September 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2006.5Third International Conference on the ...
 This Article 
 
PDF
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Thomas Herault, LRI - U. Paris-Sud, France
Richard Lassaigne, Equipe de Logique - U. Paris VII
Sylvain Peyronnet, LRDE/EPITA
In this paper, we give a brief overview of APMC (Approximate Probabilistic Model Checker). APMC implements approximate probabilistic verification of probabilistic systems. It is based on Monte-Carlo method and the theory of randomized approximation schemes and allows to verify extremly large models without explicitely representing the global transition system. To avoid the state-space explosion phenomenon, APMC gives an accurate approximation of the satisfaction probability of the property instead of the exact value, but using only a very small amount of memory. The version of APMC we present can handle efficiently both discrete and continuous time probabilistic systems.
Citation:
Thomas Herault, Richard Lassaigne, Sylvain Peyronnet, "APMC 3.0: Approximate Verification of Discrete and Continuous Time Markov Chains," qest, pp.129-130, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.