In this paper we present an explicit verification algorithm for Probabilistic Systems defining {\em discrete time}/{\em finite state} Markov Chains. We restrict ourselves to verification of {\em Bounded} PCTL formulas (BPCTL), that is, PCTL formulas in which all {\em Until} operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain ${\cal M}$ and a BPCTL formula $\Phi$, our algorithm checks if $\Phi$ is satisfied in ${\cal M}$. This allows to verify important properties, such as reliability in {\em Discrete Time Hybrid Systems}. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ ({\em Finite Horizon Probabilistic} Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).