APMC: Approximate Probabilistic Model Checker is an approximate distributed model checker for fully probabilistic systems. APMC uses a randomized algorithm to approximate the probability that a LTL formula is true, by using sampling of execution paths of the system. APMC uses a distributed computation model to distribute path generation and formula verification on a cluster of workstations. The implementation of the tool started in 2003 and was originally done using C programming language together with lex and yacc. APMC was rewritten recently in Java for its version 3.0. A specific version has been developped for the CELL architecture, please let us know if you’re interested.
This is the last « stable » version of APMC.
APMC2.0 tar.gz file (618 kB)
APMC2.0 tar.bz2 file (422 kB)
This version, which is no longer supported, goes with a user friendly GUI:
APMC GUI tar.gz file (115 kB)
APMC GUI tar.bz2 file (95 kB)
But the new version is APMC3.0, which supports DTMCs and CTMCs.
To download the beta version of APMC3.0:
APMC3.0b tar.gz file (95 kB)