This version of Murphi (namely CMurphi 5.2.4) is able to perform Finite Horizon Probabilistic Model Checking, i.e. to verify PCTL properties with only bounded untils (BPCTL) on Discrete Time Markov Chains. Unlike the other probabilistic model checkers (such as PRISM), the algorithms we use to this achive this goal are based on explicit enumeration. For major details, see CHARME03 and FMCAD04 papers. Moreover, this release includes the cache and disk extensions of CMurphi 4.2.

CMurphi 5.2.4 can be downloaded from here (.tgz).

Previous releases of Caching Murphi may be found here.