{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:36:52Z","timestamp":1773247012925,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,8,10]],"date-time":"2014-08-10T00:00:00Z","timestamp":1407628800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10009-014-0343-0","type":"journal-article","created":{"date-parts":[[2014,8,9]],"date-time":"2014-08-09T10:56:41Z","timestamp":1407581801000},"page":"527-536","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Statistical model checking for biological applications"],"prefix":"10.1007","volume":"17","author":[{"given":"Paolo","family":"Zuliani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,8,10]]},"reference":[{"issue":"6","key":"343_CR1","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.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"343_CR2","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: QEST, pp. 143\u2013144 (2011)","DOI":"10.1109\/QEST.2011.24"},{"key":"343_CR3","doi-asserted-by":"crossref","unstructured":"Ballarini, P., M\u00e4kel\u00e4, J., Ribeiro, A.S.: Expressive statistical model checking of genetic networks with delayed stochastic dynamics. In: CMSB, volume 7605 of LNCS, pp. 29\u201348 (2012)","DOI":"10.1007\/978-3-642-33636-2_4"},{"key":"343_CR4","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: HSB, volume 125 of EPTCS, pp. 3\u201319 (2013)","DOI":"10.4204\/EPTCS.125.1"},{"key":"343_CR5","doi-asserted-by":"crossref","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: QEST, volume 8054 of LNCS, pp. 160\u2013164 (2013)","DOI":"10.1007\/978-3-642-40196-1_12"},{"key":"343_CR6","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010ceska, M., \u0160afr\u00e1nek, D.: Model checking of biological systems. In: SFM, volume 7938 of LNCS, pp. 63\u2013112 (2013)","DOI":"10.1007\/978-3-642-38874-3_3"},{"key":"343_CR7","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. In: QAPL, volume 85 of EPTCS, pp. 1\u201316 (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"343_CR8","doi-asserted-by":"crossref","unstructured":"Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. In: Transactions on Computational Systems Biology, volume 4220 of LNCS, pp. 68\u201394 (2006)","DOI":"10.1007\/11880646_4"},{"key":"343_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in BioLab: applications to the automated analysis of T-cell receptor signaling pathway. In: CMSB, volume 5307 of LNCS, pp. 231\u2013250 (2008)","DOI":"10.1007\/978-3-540-88562-7_18"},{"key":"343_CR10","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. In: ISoLA (1), volume 7609 of LNCS, pp. 388\u2013404 (2012)","DOI":"10.1007\/978-3-642-34026-0_29"},{"key":"343_CR11","doi-asserted-by":"crossref","unstructured":"Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: CMSB, volume 5307 of LNCS, pp. 269\u2013287 (2008)","DOI":"10.1007\/978-3-540-88562-7_20"},{"key":"343_CR12","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: CAV, volume 8044 of LNCS, pp. 264\u2013279 (2013)","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"343_CR13","doi-asserted-by":"crossref","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: LICS, pp. 305\u2013314 (2012)","DOI":"10.1109\/LICS.2012.41"},{"key":"343_CR14","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1016\/0021-9991(76)90041-3","volume":"22","author":"DT Gillespie","year":"1976","unstructured":"Gillespie, D.T.: A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. J. Comput. Phys. 22, 403\u2013434 (1976)","journal-title":"J. Comput. Phys."},{"key":"343_CR15","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1016\/0378-4371(92)90283-V","volume":"188","author":"DT Gillespie","year":"1992","unstructured":"Gillespie, D.T.: A rigorous derivation of the chemical master equation. Phys. A 188, 404\u2013425 (1992)","journal-title":"Phys. A"},{"issue":"4","key":"343_CR16","doi-asserted-by":"crossref","first-page":"1716","DOI":"10.1063\/1.1378322","volume":"115","author":"DT Gillespie","year":"2001","unstructured":"Gillespie, D.T.: Approximate accelerated stochastic simulation of chemically reacting systems. J. Chem. Phys. 115(4), 1716\u20131733 (2001)","journal-title":"J. Chem. Phys."},{"issue":"4","key":"343_CR17","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1093\/bioinformatics\/btg015","volume":"19","author":"M Hucka","year":"2003","unstructured":"Hucka, M., et al.: The systems biology markup language (SBML): a medium for representation and exchange of biochemical network models. Bioinformatics 19(4), 524\u2013531 (2003)","journal-title":"Bioinformatics"},{"key":"343_CR18","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: CMSB, volume 5688 of LNCS, pp. 218\u2013234 (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"issue":"3\/4","key":"343_CR19","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1504\/IJBRA.2012.048964","volume":"8","author":"SK Jha","year":"2012","unstructured":"Jha, S.K., Dutta, R.G., Langmead, C.J., Jha, S., Sassano, E.: Synthesis of insulin pump controllers from safety specifications using Bayesian model validation. IJBRA 8(3\/4), 263\u2013285 (2012)","journal-title":"IJBRA"},{"issue":"21","key":"343_CR20","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. Theory Comput. Sci. 412(21), 2162\u20132187 (2011)","journal-title":"Theory Comput. Sci."},{"key":"343_CR21","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Langmead, C.J.: Exploring behaviors of stochastic differential equation models of biological systems using change of measures. BMC Bioinform. 13(S\u20135), S8 (2012)","DOI":"10.1186\/1471-2105-13-S5-S8"},{"key":"343_CR22","doi-asserted-by":"crossref","unstructured":"Keating, S.M., Bornstein, B.J., Finney, A., Hucka, M.: SBMLToolbox: an SBML toolbox for MATLAB users. Bioinformatics 22(10), 1275\u20131277 (2006)","DOI":"10.1093\/bioinformatics\/btl111"},{"key":"343_CR23","doi-asserted-by":"crossref","unstructured":"Kitano, H.: Biological robustness. Nat. Rev. Genet. 5(11), 826\u2013837 (2004)","DOI":"10.1038\/nrg1471"},{"issue":"S\u201317","key":"343_CR24","doi-asserted-by":"crossref","first-page":"S15","DOI":"10.1186\/1471-2105-13-S17-S15","volume":"13","author":"CH Koh","year":"2012","unstructured":"Koh, C.H., Palaniappan, S.K., Thiagarajan, P.S., Wong, L.: Improved statistical model checking methods for pathway analysis. BMC Bioinform. 13(S\u201317), S15 (2012)","journal-title":"BMC Bioinform."},{"issue":"4","key":"343_CR25","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real Time Syst."},{"issue":"1","key":"343_CR26","doi-asserted-by":"crossref","first-page":"49","DOI":"10.2307\/3212147","volume":"7","author":"TG Kurtz","year":"1970","unstructured":"Kurtz, T.G.: Solutions of ordinary differential equations as limits of pure jump Markov processes. J. Appl. Prob. 7(1), 49\u201358 (1970)","journal-title":"J. Appl. Prob."},{"key":"343_CR27","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV, volume 6806 of LNCS, pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"1\u20132","key":"343_CR28","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"343_CR29","doi-asserted-by":"crossref","unstructured":"Palaniappan, S.K., Gyori, B.M., Liu, B., Hsu, D., Thiagarajan, P.S.: Statistical model checking based calibration and analysis of bio-pathway models. In: CMSB, volume 8130 of LNCS, pp. 120\u2013134 (2013)","DOI":"10.1007\/978-3-642-40708-6_10"},{"issue":"24","key":"343_CR30","doi-asserted-by":"crossref","first-page":"12784","DOI":"10.1063\/1.1627296","volume":"119","author":"M Rathinam","year":"2003","unstructured":"Rathinam, M., Petzold, L.R., Cao, Y., Gillespie, D.T.: Stiffness in stochastic chemically reacting systems: the implicit tau-leaping method. J. Chem. Phys. 119(24), 12784\u201312794 (2003)","journal-title":"J. Chem. Phys."},{"issue":"4","key":"343_CR31","doi-asserted-by":"crossref","first-page":"514","DOI":"10.2307\/2271358","volume":"33","author":"D Richardson","year":"1968","unstructured":"Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514\u2013520 (1968)","journal-title":"J. Symb. Log."},{"key":"343_CR32","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.E.: Simulating insulin infusion pump risks by in-silico modeling of the insulin-glucose regulatory system. In: CMSB, volume 7605 of LNCS, pp. 322\u2013341 (2012)","DOI":"10.1007\/978-3-642-33636-2_19"},{"key":"343_CR33","doi-asserted-by":"crossref","unstructured":"Schivo, S., Scholma, J., Wanders, B., Camacho, R.A U., van der Vet, P.E., Karperien, M., Langerak, R., van de Pol, J., Post, J.N.: Modelling biological pathway dynamics with timed automata. In: BIBE, pp. 447\u2013453. IEEE Press, New York (2012)","DOI":"10.1109\/BIBE.2012.6399719"},{"key":"343_CR34","doi-asserted-by":"crossref","unstructured":"\u010ceska, M., \u0160afr\u00e1nek, D., Dra\u017ean, S., Brim, L.: Robustness analysis of stochastic biochemical systems. PLoS One 9(4): e94553 (2014)","DOI":"10.1371\/journal.pone.0094553"},{"issue":"2","key":"343_CR35","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential test of stastistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"343_CR36","doi-asserted-by":"crossref","unstructured":"Wilkinson, D.J.: Stochastic modelling for systems biology, 2nd edn. CRC Press, Boca Raton (2011)","DOI":"10.1201\/b11812"},{"key":"343_CR37","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: VMCAI, volume 3855 of LNCS, pp. 142\u2013156 (2006)","DOI":"10.1007\/11609773_10"},{"key":"343_CR38","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV, volume 2404 of LNCS, pp. 223\u2013235 (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"key":"343_CR39","doi-asserted-by":"crossref","unstructured":"Zhang, F., Yeddanapudi, M., Mosterman, P.: Zero-crossing location and detection algorithms for hybrid system simulation. IFAC World Congress, pp. 7967\u20137972 (2008)","DOI":"10.3182\/20080706-5-KR-1001.01346"},{"key":"343_CR40","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink\/Stateflow verification. In: HSCC, pp. 243\u2013252 (2010)","DOI":"10.1145\/1755952.1755987"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0343-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0343-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0343-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,14]],"date-time":"2022-04-14T02:28:54Z","timestamp":1649903334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0343-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,10]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["343"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0343-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,10]]}}}