www.prismmodelchecker.org
[DHK14] Frits Dannenberg, Ernst Moritz Hahn and Marta Kwiatkowska. Computing Cumulative Rewards using Fast Adaptive Uniformisation. ACM Transactions on Modeling and Computer Simulation, Special Issue on Computational Methods in Systems Biology. 2014. [pdf] [bib] [Develops fast adaptive uniformisation techniques for cumulative reward properties, implemented in PRISM.]
Downloads:  pdf pdf (426 KB)  bib bib
Links: [Google] [Google Scholar]
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 et al. 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. The performance of the method is enhanced by the use of interval splitting. We compare our implementation to standard uniformisation implemented in PRISM and to fast adaptive uniformisation without support for cumulative rewards implemented in MARCIE, demonstrating superior performance.

Publications