FHP-Murphi

FHP-Murphi (Finite Horizon Probabilistic Murphi) is a probabilistic model checker developed on the top of Murphi.

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 the following two publications:

Finite Horizon Analysis of Markov Chains with the Murphi Verifier, 2006

@article{dellapenna-etal:2006:sttt,
author = {Della Penna, G. and Intrigila, B. and Melatti, I. and Tronci, E. and Venturini Zilli, M.},
doi = {10.1007/s10009-005-0216-7},
journal = {International Journal on Software Tools for Technology Transfer},
number = {4--5},
pages = {397-409},
publisher = {Springer},
title = {Finite Horizon Analysis of {M}arkov Chains with the {M}urphi Verifier},
volume = {8},
year = {2006},
}

Bounded Probabilistic Model Checking with the Murphy Verifier, 2004

@inproceedings{dellapenna-etal:2004:bounded,
author = {Della Penna, G. and Intrigila, B. and Melatti, I. and Tronci, E. and Venturini Zilli, M.},
booktitle = {Proceedings of 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2004)},
pages = {214--229},
publisher = {IEEE},
title = {Bounded Probabilistic Model Checking with the {Mur$\varphi$} Verifier},
year = {2004},
}