Bounded Probabilistic Model Checking with the Murphi Verifier