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},
}