Computing Cumulative Rewards Using Fast Adaptive Uniformisation
In Computational Methods in Systems Biology - 11th International
, pages 33-49, Springer
, Lecture Notes in Computer Science 8130, 2013.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-40708-6_4
Abstract. The computation of transient probabilities for continuous-time
Markov chains often employs uniformisation, also known as the Jensen's method.
The fast adaptive uniformisation method introduced by Mateescu approximates
the probability by neglecting insignificant states, and has proven to be
effective for quantitative analysis of stochastic models arising in chemical
and biological applications. However, this method has only been formulated for
the analysis of properties at a given point of time t. In this paper, we
extend fast adaptive uniformisation to handle expected reward properties which
reason about the model behaviour until time t, for example, the expected
number of chemical reactions that have occurred until t. To show the
feasibility of the approach, we integrate the method into the probabilistic
model checker PRISM and apply it to a range of biological models,
demonstrating superior performance compared to existing techniques.