{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:48:47Z","timestamp":1750308527010,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,2,17]],"date-time":"2015-02-17T00:00:00Z","timestamp":1424131200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC Advanced Grant VERIWARE"},{"name":"International Young Scientists","award":["61350110518"],"award-info":[{"award-number":["61350110518"]}]},{"name":"Microsoft Research PhD Studentship"},{"name":"Chinese Academy of Sciences Fellowship","award":["2013Y1GB0006"],"award-info":[{"award-number":["2013Y1GB0006"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2015,4,6]]},"abstract":"<jats:p>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<jats:italic>t<\/jats:italic>. In this article, we extend fast adaptive uniformization to handle expected reward properties that reason about the model behavior until time<jats:italic>t<\/jats:italic>, for example, the expected number of chemical reactions that have occurred until<jats:italic>t<\/jats:italic>. 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.<\/jats:p>","DOI":"10.1145\/2688907","type":"journal-article","created":{"date-parts":[[2015,2,18]],"date-time":"2015-02-18T13:24:05Z","timestamp":1424265845000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Computing Cumulative Rewards Using Fast Adaptive Uniformization"],"prefix":"10.1145","volume":"25","author":[{"given":"Frits","family":"Dannenberg","sequence":"first","affiliation":[{"name":"University of Oxford, Department of Computer Science, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[{"name":"University of Oxford, Department of Computer Science, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[{"name":"University of Oxford, Department of Computer Science, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,2,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810891.1810912"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"G. Clark T. Courtney D. Daly D. Deavours S. Derisavi J. M. Doyle W. H. Sanders and P. Webster. 2001. The m\u00f6bius modeling tool. In PNPM. 241--250. G. Clark T. Courtney D. Daly D. Deavours S. Derisavi J. M. Doyle W. H. Sanders and P. Webster. 2001. The m\u00f6bius modeling tool. In PNPM. 241--250.","DOI":"10.1109\/PNPM.2001.953373"},{"volume":"8141","volume-title":"Proc. 19th International Conference on DNA Computing and Molecular Programming (DNA 19)","author":"Dannenberg F.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"F. Dannenberg M. Kwiatkowska C. Thachuk and A. J. Turberfield. 2014. DNA walker circuits: Computational potential design and verification. Nat. Comput. (2014) 1--17. http:\/\/dx.doi.org\/10.1007\/s11047-014-9426-9. F. Dannenberg M. Kwiatkowska C. Thachuk and A. J. Turberfield. 2014. DNA walker circuits: Computational potential design and verification. Nat. Comput. (2014) 1--17. http:\/\/dx.doi.org\/10.1007\/s11047-014-9426-9.","DOI":"10.1007\/s11047-014-9426-9"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.33"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btm566"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/42404.42409"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_49"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.11.013"},{"key":"e_1_2_1_13_1","first-page":"87","article-title":"Markoff chains as an aid in the study of Markoff processes","volume":"36","author":"Jensen A.","year":"1953","journal-title":"Skand. Aktuarietidskr."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2010.04.001"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.camwa.2005.11.016"},{"volume":"4486","volume-title":"SFM\u201907","author":"Kwiatkowska M.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In CAV. 585--591. M. Kwiatkowska G. Norman and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In CAV. 585--591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_18_1","first-page":"1470","article-title":"Design and analysis of DNA strand displacement devices using probabilistic model checking","volume":"9","author":"Lakin M.","year":"2012","journal-title":"RSIF"},{"key":"e_1_2_1_19_1","unstructured":"M. Mateescu. 2011. Propagation Models for Biochemical Reaction Networks. Ph.D. Dissertation. EPFL. M. Mateescu. 2011. Propagation Models for Biochemical Reaction Networks. Ph.D. Dissertation. EPFL."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-syb.2010.0005"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2145882"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcp.2007.05.016"},{"volume-title":"Proc. American Control Conference. 2761--2766","author":"Munsky B.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03845-7_20"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.19"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.1132493"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"D. Spieler E. M. Hahn and L. Zhang. 2014. Model checking CSL for markov population models. In QAPL. 93--107. D. Spieler E. M. Hahn and L. Zhang. 2014. Model checking CSL for markov population models. In QAPL. 93--107.","DOI":"10.4204\/EPTCS.154.7"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"J. J. Tapia J. R. Faeder and B. Munsky. 2012. Adaptive coarse-graining for transient and quasi-equilibrium analyses of stochastic gene regulation. In CDC. 5361--5366. J. J. Tapia J. R. Faeder and B. Munsky. 2012. Adaptive coarse-graining for transient and quasi-equilibrium analyses of stochastic gene regulation. In CDC. 5361--5366.","DOI":"10.1109\/CDC.2012.6425828"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1080\/15326349408807313"},{"key":"e_1_2_1_30_1","unstructured":"A. P. A. van Moorsel and K. Wolter. 1998. Numerical solution of non-homogeneous Markov processes through uniformization. In 12th European Simulation MultiConference. Simulation - Past Present and Future. A. P. A. van Moorsel and K. Wolter. 1998. Numerical solution of non-homogeneous Markov processes through uniformization. In 12th European Simulation MultiConference. Simulation - Past Present and Future."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1038\/nnano.2011.253"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1038\/nnano.2010.284"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2688907","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2688907","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:55:46Z","timestamp":1750272946000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2688907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,17]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4,6]]}},"alternative-id":["10.1145\/2688907"],"URL":"https:\/\/doi.org\/10.1145\/2688907","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"type":"print","value":"1049-3301"},{"type":"electronic","value":"1558-1195"}],"subject":[],"published":{"date-parts":[[2015,2,17]]},"assertion":[{"value":"2014-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-02-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}