Markov reward model

An additional variable records the reward accumulated up to the current time.

[1] Features of interest in the model include expected reward at a given time and expected time to accumulate a given reward.

[2] The model appears in Ronald A. Howard's book.

The Markov Reward Model Checker tool can be used to numerically compute transient and stationary properties of Markov reward models.

The accumulated reward at a time t can be computed numerically over the time domain or by evaluating the linear hyperbolic system of equations which describe the accumulated reward using transform methods or finite difference methods.