{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:42:46Z","timestamp":1762101766019,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319234007"},{"type":"electronic","value":"9783319234014"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23401-4_3","type":"book-chapter","created":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T10:37:23Z","timestamp":1441103843000},"page":"15-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Qinsi","family":"Wang","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Zuliani","sequence":"additional","affiliation":[]},{"given":"Soonho","family":"Kong","sequence":"additional","affiliation":[]},{"given":"Sicun","family":"Gao","sequence":"additional","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,2]]},"reference":[{"key":"3_CR1","volume-title":"Stochastic Differential Equations: Theory and Applications","author":"L Arnold","year":"1974","unstructured":"Arnold, L.: Stochastic Differential Equations: Theory and Applications. Wiley - Interscience, New York (1974)"},{"key":"3_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/11587392","volume-title":"Stochastic Hybrid Systems: Theory and Safety Critical Applications","author":"HA Blom","year":"2006","unstructured":"Blom, H.A., Lygeros, J., Everdij, M., Loizou, S., Kyriakopoulos, K.: Stochastic Hybrid Systems: Theory and Safety Critical Applications. Springer, Heidelberg (2006)"},{"issue":"5","key":"3_CR3","doi-asserted-by":"publisher","first-page":"858","DOI":"10.1002\/cncr.22464","volume":"109","author":"N Bruchovsky","year":"2007","unstructured":"Bruchovsky, N., Klotz, L., Crook, J., Goldenberg, L.: Locally advanced prostate cancer: biochemical results from a prospective phase II study of intermittent androgen suppression for men with evidence of prostate-specific antigen recurrence after radiotherapy. Cancer 109(5), 858\u2013867 (2007)","journal-title":"Cancer"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1002\/cncr.21989","volume":"107","author":"N Bruchovsky","year":"2006","unstructured":"Bruchovsky, N., Klotz, L., et al.: Final results of the Canadian prospective phase II trial of intermittent androgen suppression for men in biochemical recurrence after radiotherapy for locally advanced prostate cancer. Cancer 107(2), 389\u2013395 (2006)","journal-title":"Cancer"},{"issue":"3","key":"3_CR5","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1016\/j.jtbi.2008.03.029","volume":"253","author":"A Bueno-Orovio","year":"2008","unstructured":"Bueno-Orovio, A., Cherry, E.M., Fenton, F.H.: Minimal model for human ventricular action potentials in tissue. J. Theor. Biol. 253(3), 544\u2013560 (2008)","journal-title":"J. Theor. Biol."},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011)"},{"issue":"4","key":"3_CR7","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ansi-c software. IEEE Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Softw. Eng."},{"key":"3_CR8","first-page":"1","volume":"17","author":"C Ellen","year":"2014","unstructured":"Ellen, C., Gerwinn, S., Fr\u00e4nzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int. J. Softw. Tools Technol. Transf. 17, 1\u201320 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC, pp. 43\u201352, April 2011","DOI":"10.1145\/1967701.1967710"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-78929-1_13","volume-title":"Hybrid Systems: Computation and Control","author":"M Fr\u00e4nzle","year":"2008","unstructured":"Fr\u00e4nzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172\u2013186. Springer, Heidelberg (2008)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Chen, W., Clarke, E.M.: $$\\delta $$-complete analysis for bounded reachability of hybrid systems (2014). CoRR, arXiv:1404.7171","DOI":"10.21236\/ADA613813"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Norman, G., Parker, D., Wachter, B., Zhang, L.: Game-based abstraction and controller synthesis for probabilistic hybrid systems. In: QEST, pp. 69\u201378. IEEE (2011)","DOI":"10.1109\/QEST.2011.17"},{"key":"3_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"The Theory of Hybrid Automata","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The Theory of Hybrid Automata. Springer, Berlin (2000)"},{"issue":"301","key":"3_CR14","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-46430-1_16","volume-title":"Hybrid Systems: Computation and Control","author":"J Hu","year":"2000","unstructured":"Hu, J., Lygeros, J., Sastry, S.S.: Towards a theory of stochastic hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 160\u2013173. Springer, Heidelberg (2000)"},{"issue":"430","key":"3_CR16","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1080\/01621459.1995.10476572","volume":"90","author":"RE Kass","year":"1995","unstructured":"Kass, R.E., Raftery, A.E.: Bayes factors. JASA 90(430), 773\u2013795 (1995)","journal-title":"JASA"},{"issue":"2","key":"3_CR17","first-page":"856","volume":"16","author":"TL Lai","year":"1988","unstructured":"Lai, T.L.: Nearly optimal sequential tests of composite hypotheses. AOS 16(2), 856\u2013886 (1988)","journal-title":"AOS"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Wang, Q., Miskov-Zivanov, N., Telmex, C., Clarke, E.M.: Formal analysis provides parameters for guiding hyperoxidation in\u00a0bacteria using phototoxic proteins. GLSVLSI 2015 (2015)","DOI":"10.1145\/2742060.2743762"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Shmarov, F., Zuliani, P.: Probreach: verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC (2015)","DOI":"10.1145\/2728606.2728625"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 31\u201345. Springer, Heidelberg (2000)"},{"key":"3_CR21","unstructured":"Sproston, J.: Model checking for probabilistic timed and hybrid systems. Ph.D. thesis. SCS, University of Birmingham (2001)"},{"issue":"1930","key":"3_CR22","doi-asserted-by":"publisher","first-page":"5029","DOI":"10.1098\/rsta.2010.0221","volume":"368","author":"G Tanaka","year":"2010","unstructured":"Tanaka, G., Hirata, Y., Goldenberg, L., Bruchovsky, N., Aihara, K.: Mathematical modelling of prostate cancer growth and its application to hormone therapy. Phil. Trans. Roy. Soc. A Math. Phys. Eng. Sci. 368(1930), 5029\u20135044 (2010)","journal-title":"Phil. Trans. Roy. Soc. A Math. Phys. Eng. Sci."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Tinelli, C.: SMT-based model checking. In: NASA FM, p. 1 (2012)","DOI":"10.1007\/978-3-642-28891-3_1"},{"issue":"2","key":"3_CR24","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"3_CR25","unstructured":"Younes, H.L.: Verification and planning for stochastic processes with asynchronous events. Technical report, DTIC Document (2005)"},{"issue":"2","key":"3_CR26","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/s10703-013-0195-3","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow\/simulink verification. Formal Methods Syst. Des. 43(2), 338\u2013367 (2013)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Computational Methods in Systems Biology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23401-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T11:51:52Z","timestamp":1676029912000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23401-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319234007","9783319234014"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23401-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"2 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}