FHP-Murphi
- Details
- Category: Software
- Last Updated on Tuesday, 27 November 2012 10:23
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 | |||
|---|---|---|---|
| name | comments | file | size |
| FHP-Murphi 5.2.4.2 | 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 | |
© Model Checking Group -