Computing Cumulative Rewards Using Fast Adaptive Uniformization

Frits Dannenberg, Ernst Moritz Hahn, Marta Z. Kwiatkowska

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

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 pages23
JournalACM Transactions on Modeling and Computer Simulation
Volume25
Issue number2
DOIs
Publication statusPublished - 06 Apr 2015
Externally publishedYes

Fingerprint Dive into the research topics of 'Computing Cumulative Rewards Using Fast Adaptive Uniformization'. Together they form a unique fingerprint.

Cite this