APMC
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.