APMC 3.0: Approximate Verification of Discrete and Continuous Time Markov Chains

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 extremely large models without explicitly 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