Before revision:  We adapt our previous HSR model and propose its stochastic extension, which we then analyze using the approximate probabilistic model checking (APMC) technique.
After revision:  We adapt our previous HSR model and propose its stochastic extension, which we then analyse using the approximate probabilistic model checking (APMC) technique.