  We study and develop the stochastic Markov reward model (sMRM), which extends
the Markov chain where transition time/reward as modelled as random variables.
Techniques are presented to enable computing first-passage time distributions
(or reward distributions) with high accuracy for only modestly sized systems
when solved for on a single computer. In contrast, naive simulations technique
scale and are sufficient for a plethora of problems where high accuracy is not
an issue, but this work perhaps would be valuable when extremely accurate
solutions are demanded if it can be modelled precisely (a potentially big
caveat).
  The work presented is intertwined with theory of temporal logics, although
not the major contribution of the work, achieves the connection of this work to
the field of automated probabilistic analysis/verification. Although its
admittance does obfuscate the algorithmic details that are major, however.
  We present equations for computing first-passage reward densities, expected
value problems, and other reachability problems. The focus was on finding
strictly numerical solutions for first-passage time/reward densities. We
adapted linear algebra algorithms such as Gaussian elimination, and iterative
methods such as the power method, Jacobi and Gauss-Seidel. We provide solutions
for both discrete-reward sMRMs, where all rewards discrete (lattice) random
variables. And for continuous-reward sMRMs, where all rewards are strictly
continuous random variables. Our solutions involve the use of fast Fourier
transform (FFT) for faster computation, and we were able to adapt existing
quadrature rules for convolution to gain more accurate solutions, rules such as
the trapezoid rule, Simpson's rule and Romberg's method.
