{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T12:23:49Z","timestamp":1777465429794,"version":"3.51.4"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2016,3,28]],"date-time":"2016-03-28T00:00:00Z","timestamp":1459123200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["VERIWARE"],"award-info":[{"award-number":["VERIWARE"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001824","name":"Grantov\u00e1 Agentura \u010cesk\u00e9 Republiky","doi-asserted-by":"publisher","award":["GA15-11089S"],"award-info":[{"award-number":["GA15-11089S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1007\/s00236-016-0265-2","type":"journal-article","created":{"date-parts":[[2016,3,28]],"date-time":"2016-03-28T11:23:38Z","timestamp":1459164218000},"page":"589-623","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":40,"title":["Precise parameter synthesis for stochastic biochemical systems"],"prefix":"10.1007","volume":"54","author":[{"given":"Milan","family":"\u010ce\u0161ka","sequence":"first","affiliation":[]},{"given":"Frits","family":"Dannenberg","sequence":"additional","affiliation":[]},{"given":"Nicola","family":"Paoletti","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,28]]},"reference":[{"key":"265_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Brim, L., \u010ce\u0161ka, M., Kwiatkowska, M.: Adaptive aggregation of markov chains: quantitative analysis of chemical reaction networks. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification (CAV), LNCS, vol. 9206, pp. 195\u2013213. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_12"},{"key":"265_CR2","doi-asserted-by":"crossref","unstructured":"Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Parameter identification for Markov models of biochemical reactions. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification (CAV), LNCS, pp. 83\u201398. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_8"},{"key":"265_CR3","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification (CAV), LNCS, vol. 1102, pp. 269\u2013276. Springer (1996)","DOI":"10.1007\/3-540-61474-5_75"},{"issue":"6","key":"265_CR4","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans Softw Eng"},{"key":"265_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) Computational Methods in Systems Biology (CMSB), pp. 164\u2013177. Springer (2013)","DOI":"10.1007\/978-3-642-40708-6_13"},{"issue":"18","key":"265_CR6","doi-asserted-by":"crossref","first-page":"2415","DOI":"10.1093\/bioinformatics\/btm362","volume":"23","author":"G Batt","year":"2007","unstructured":"Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18), 2415\u20132422 (2007)","journal-title":"Bioinformatics"},{"issue":"11","key":"265_CR7","doi-asserted-by":"crossref","first-page":"1749","DOI":"10.1109\/TAC.2006.884957","volume":"51","author":"C Belta","year":"2006","unstructured":"Belta, C., Habets, L.: Controlling a class of nonlinear systems on rectangles. IEEE Trans Autom Control 51(11), 1749\u20131759 (2006)","journal-title":"IEEE Trans Autom Control"},{"key":"265_CR8","volume-title":"Probability and Measure","author":"P Billingsley","year":"2008","unstructured":"Billingsley, P.: Probability and Measure. Wiley, Hoboken (2008)"},{"key":"265_CR9","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time markov chains. CoRR. arXiv:1402.1450 (2014)"},{"key":"265_CR10","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) Quantitative Evaluation of Systems (QEST), LNCS, vol. 8054, pp. 89\u2013105. Springer (2013)","DOI":"10.1007\/978-3-642-40196-1_7"},{"key":"265_CR11","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification (CAV), LNCS, vol. 8044, pp. 107\u2013123. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_7"},{"key":"265_CR12","unstructured":"Caron, R., Traynor, T.: The zero set of a polynomial. Technical report, University of Windsor (2005)"},{"key":"265_CR13","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) Computational Methods in Systems Biology (CMSB), pp. 86\u201398. Springer (2014)","DOI":"10.1007\/978-3-319-12982-2_7"},{"key":"265_CR14","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Theoretical Aspects of Software Engineering (TASE), pp. 85\u201392. IEEE (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"265_CR15","volume-title":"Introduction to Calculus and Analysis","author":"R Courant","year":"2012","unstructured":"Courant, R., John, F.: Introduction to Calculus and Analysis, vol. 2. Springer, Berlin (2012)"},{"key":"265_CR16","doi-asserted-by":"crossref","unstructured":"Dannenberg, F., Hahn, E.M., Kwiatkowska, M.: Computing cumulative rewards using fast adaptive uniformisation. In: Gupta, A., Henzinger, T.A. (eds.) Computational Methods in Systems Biology (CMSB), LNCS, vol. 8130, pp. 33\u201349. Springer (2013)","DOI":"10.1007\/978-3-642-40708-6_4"},{"key":"265_CR17","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s11047-014-9426-9","volume":"14","author":"F Dannenberg","year":"2014","unstructured":"Dannenberg, F., Kwiatkowska, M., Thachuk, C., Turberfield, A.: DNA walker circuits: computational potential, design, and verification. Nat. Comput. 14, 195\u2013211 (2014)","journal-title":"Nat. Comput."},{"key":"265_CR18","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 167\u2013170. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_17"},{"issue":"4","key":"265_CR19","first-page":"440","volume":"31","author":"BL Fox","year":"1988","unstructured":"Fox, B.L., Glynn, P.W.: Computing Poisson probabilities. CACM 31(4), 440\u2013445 (1988)","journal-title":"Computing Poisson probabilities. CACM"},{"issue":"25","key":"265_CR20","doi-asserted-by":"crossref","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"DT Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340\u20132381 (1977)","journal-title":"J. Phys. Chem."},{"issue":"1","key":"265_CR21","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0305-0548(77)90007-7","volume":"4","author":"W Grassmann","year":"1977","unstructured":"Grassmann, W.: Transient solutions in Markovian queueing systems. Comput. Oper. Res. 4(1), 47\u201353 (1977)","journal-title":"Comput. Oper. Res."},{"issue":"1","key":"265_CR22","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. (STTT) 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"265_CR23","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Real-Time Systems Symposium (RTSS), pp. 173\u2013182. IEEE (2008)","DOI":"10.1109\/RTSS.2008.19"},{"key":"265_CR24","first-page":"87","volume":"36","author":"A Jensen","year":"1953","unstructured":"Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Skand. Aktuarietidskr. 36, 87\u201391 (1953)","journal-title":"Skand. Aktuarietidskr."},{"issue":"21","key":"265_CR25","doi-asserted-by":"crossref","first-page":"2162","DOI":"10.1016\/j.tcs.2011.01.012","volume":"412","author":"SK Jha","year":"2011","unstructured":"Jha, S.K., Langmead, C.J.: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement. Theor. Comput. Sci. 412(21), 2162\u20132187 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"265_CR26","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time markov chains. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 311\u2013324. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_37"},{"issue":"1","key":"265_CR27","first-page":"57","volume":"53","author":"W Kermack","year":"1991","unstructured":"Kermack, W., McKendrick, A.: Contributions to the mathematical theory of epidemicsii. The problem of endemicity. Bull. Math. Biol. 53(1), 57\u201387 (1991)","journal-title":"Bull. Math. Biol."},{"key":"265_CR28","doi-asserted-by":"crossref","unstructured":"Klarner, H., Streck, A., \u0160afr\u00e1nek, D., Kol\u010d\u00e1k, J., Siebert, H.: Parameter identification and model ranking of thomas networks. In: Gilbert, D., Heiner, M. (eds.) Computational Methods in Systems Biology (CMSB), pp. 207\u2013226. Springer (2012)","DOI":"10.1007\/978-3-642-33636-2_13"},{"issue":"1","key":"265_CR29","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1145\/2480359.2429125","volume":"48","author":"AS Koksal","year":"2013","unstructured":"Koksal, A.S., Pu, Y., Srivastava, S., Bodik, R., Fisher, J., Piterman, N.: Synthesis of biological models from mutation experiments. SIGPLAN Not. 48(1), 469\u2013482 (2013)","journal-title":"SIGPLAN Not."},{"key":"265_CR30","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/j.camwa.2005.11.016","volume":"51","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Pacheco, A.: Model checking expected time and expected reward formulae with random time bounds. Comput. Math. Appl. 51, 305\u2013316 (2006)","journal-title":"Comput. Math. Appl."},{"key":"265_CR31","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for Performance Evaluation (SFM), LNCS, vol. 4486, pp. 220\u2013270. Springer (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"265_CR32","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, LNCS, vol. 6806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"265_CR33","doi-asserted-by":"crossref","unstructured":"Madsen, C., Myers, C., Roehner, N., Winstead, C., Zhang, Z.: Utilizing stochastic model checking to analyze genetic circuits. In: Computational Intelligence in Bioinformatics and Computational Biology (CIBCB), pp. 379\u2013386. IEEE (2012)","DOI":"10.1109\/CIBCB.2012.6217255"},{"issue":"6","key":"265_CR34","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1049\/iet-syb.2010.0005","volume":"4","author":"M Mateescu","year":"2010","unstructured":"Mateescu, M., Wolf, V., Didier, F., Henzinger, T.A.: Fast adaptive uniformization of the chemical master equation. IET Syst. Biol. 4(6), 441\u2013452 (2010)","journal-title":"IET Syst. Biol."},{"issue":"333\u2013369","key":"265_CR35","first-page":"352","volume":"49","author":"L Michaelis","year":"1913","unstructured":"Michaelis, L., Menten, M.L.: Die kinetik der invertinwirkung. Biochem. z 49(333\u2013369), 352 (1913)","journal-title":"Die kinetik der invertinwirkung. Biochem. z"},{"key":"265_CR36","doi-asserted-by":"crossref","unstructured":"Paoletti, N., Yordanov, B., Hamadi, Y., Wintersteiger, C.M., Kugler, H.: Analyzing and synthesizing genomic logic functions. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification (CAV), pp. 343\u2013357. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_23"},{"issue":"11","key":"265_CR37","doi-asserted-by":"crossref","first-page":"4999","DOI":"10.1063\/1.1545446","volume":"118","author":"CV Rao","year":"2003","unstructured":"Rao, C.V., Arkin, A.P.: Stochastic chemical kinetics and the quasi-steady-state assumption: application to the gillespie algorithm. J. Chem. Phys. 118(11), 4999\u20135010 (2003)","journal-title":"J. Chem. Phys."},{"issue":"1","key":"265_CR38","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/0305-0548(88)90026-3","volume":"15","author":"A Reibman","year":"1988","unstructured":"Reibman, A.: Numerical transient analysis of Markov models. Comput. Oper. Res. 15(1), 19\u201336 (1988)","journal-title":"Comput. Oper. Res."},{"key":"265_CR39","unstructured":"Sanft, K.R., Gillespie, D.T., Petzold, L.R.: Legitimacy of the stochastic Michaelis-Menten approximation. Syst. Biol., IET 5(1), 58\u201369 (2011)"},{"key":"265_CR40","doi-asserted-by":"crossref","unstructured":"Sassi, B., Amin, M., Girard, A.: Control of polynomial dynamical systems on rectangles. In: European Control Conference (ECC), pp. 658\u2013663. IEEE (2013)","DOI":"10.23919\/ECC.2013.6669360"},{"key":"265_CR41","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3920, pp. 394\u2013410. Springer (2006)","DOI":"10.1007\/11691372_26"},{"issue":"10","key":"265_CR42","doi-asserted-by":"crossref","first-page":"1506","DOI":"10.1093\/bioinformatics\/bth110","volume":"20","author":"M Swat","year":"2004","unstructured":"Swat, M., Kel, A., Herzel, H.: Bifurcation analysis of the regulatory modules of the mammalian G1\/S transition. Bioinformatics 20(10), 1506\u20131511 (2004)","journal-title":"Bioinformatics"},{"key":"265_CR43","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1038\/nnano.2011.253","volume":"7","author":"SFJ Wickham","year":"2012","unstructured":"Wickham, S.F.J., Bath, J., Katsuda, Y., Endo, M., Hidaka, K., Sugiyama, H., Turberfield, A.J.: A DNA-based molecular motor that can navigate a network of tracks. Nat. Nanotechnol. 7, 169\u2013173 (2012)","journal-title":"Nat. Nanotechnol."},{"issue":"2","key":"265_CR44","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1504\/IJCBDD.2009.028825","volume":"2","author":"J Zhang","year":"2009","unstructured":"Zhang, J., Watson, L.T., Cao, Y.: Adaptive aggregation method for the chemical master equation. Int. J. Comput. Biol. Drug Des. 2(2), 134\u2013148 (2009)","journal-title":"Int. J. Comput. Biol. Drug Des."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0265-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0265-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0265-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0265-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T00:20:08Z","timestamp":1748823608000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0265-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,28]]},"references-count":44,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["265"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0265-2","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,28]]}}}