FHP-Murphi (Finite Horizon Probabilistic Murphi) is a probabilistic model checker developed on the top of Murphi.
The original Murphi web page is here, while a more up-to-date page is here.

FHP-Murphi implements two new probabilistic model checking algorithms. The first one is based on a BF visit of the state space and is limited to (finite horizon) probabilistic safety properties, the second one is based on a DF visit. These algorithms are described in [STTT 2006, FMCAD 2004].

The current version of FHP-Murphi is included in CMurphi.

Previous (out-of-date) versions of FHP-Murphi are listed below.


Browse all versions
FHP-Murphi latest version cmurphi5.2.4.2.tgz 2.1 MB
FHP-Murphi 5.2.3   cmurphi5.2.3.tgz 2.2 MB
FHP-Murphi 5.1.3   cmurphi5.1.3.tgz 2.2 MB
FHP-Murphi 5.1.2   cmurphi5.1.2.tgz 2.1 MB
FHP-Murphi 5.1   cmurphi5.1.tgz 2.1 MB