Computing cumulative rewards using fast adaptive uniformization

Frits Dannenberg, Ernst Moritz Hahn, Marta Kwiatkowska

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)


The computation of transient probabilities for continuous-time Markov chains often employs uniformization, also known as the Jensen method. The fast adaptive uniformization 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 article, we extend fast adaptive uniformization to handle expected reward properties that reason about the model behavior 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 uniformization implemented in PRISM and to fast adaptive uniformization without support for cumulative rewards implemented in MARCIE, demonstrating superior performance.

Original languageEnglish
Article number9
Number of pages1
JournalACM transactions on modeling and computer simulation
Issue number2
Publication statusPublished - 2015
Externally publishedYes


  • DNA computation
  • DNA strand displacement
  • Fast adaptive uniformisation
  • Markov models
  • Probabilistic model checking
  • Quantitative model checking


Dive into the research topics of 'Computing cumulative rewards using fast adaptive uniformization'. Together they form a unique fingerprint.

Cite this