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