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.

Version 2

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)