{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:35:54Z","timestamp":1743046554007,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031684159"},{"type":"electronic","value":"9783031684166"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-68416-6_12","type":"book-chapter","created":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T07:02:40Z","timestamp":1724828560000},"page":"196-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Rare-Event Guided Analysis of\u00a0Infinite-State Chemical Reaction Networks"],"prefix":"10.1007","author":[{"given":"Mohammad","family":"Ahmadi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lukas","family":"Buecherl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris J.","family":"Myers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Winstead","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hao","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,8,29]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1021\/acssynbio.2c00553","volume":"12","author":"M Ahmadi","year":"2022","unstructured":"Ahmadi, M., Thomas, P.J., Buecherl, L., Winstead, C., Myers, C.J., Zheng, H.: A comparison of weighted stochastic simulation methods for the analysis of genetic circuits. ACS Synthetic Biol. 12, 287\u2013304 (2022)","journal-title":"ACS Synthetic Biol."},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/TSE.2009.57","volume":"36","author":"H Aljazzar","year":"2009","unstructured":"Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. Softw. Eng. 36(1), 37\u201360 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"12_CR3","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1109\/MCS.2009.932926","volume":"29","author":"V Chellaboina","year":"2009","unstructured":"Chellaboina, V., Bhat, S.P., Haddad, W.M., Bernstein, D.S.: Modeling and analysis of mass-action kinetics. IEEE Control Syst. Mag. 29(4), 60\u201378 (2009)","journal-title":"IEEE Control Syst. Mag."},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Design 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Design"},{"issue":"4","key":"12_CR5","doi-asserted-by":"publisher","first-page":"01B628","DOI":"10.1063\/1.3522769","volume":"134","author":"BJ Daigle Jr","year":"2011","unstructured":"Daigle, B.J., Jr., Roh, M.K., Gillespie, D.T., Petzold, L.R.: Automated estimation of rare event probabilities in biochemical systems. J. Chem. Phys. 134(4), 01B628 (2011)","journal-title":"J. Chem. Phys."},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-11936-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C Dehnert","year":"2014","unstructured":"Dehnert, C., Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.-P.: Fast debugging of PRISM models. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146\u2013162. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_11"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-030-45190-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Funke","year":"2020","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS 2020. LNCS, vol. 12078, pp. 324\u2013345. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_18"},{"issue":"22","key":"12_CR9","doi-asserted-by":"publisher","first-page":"224103","DOI":"10.1063\/1.5090979","volume":"150","author":"CS Gillespie","year":"2019","unstructured":"Gillespie, C.S., Golightly, A.: Guided proposals for efficient weighted stochastic simulation. J. Chem. Phys. 150(22), 224103 (2019)","journal-title":"J. Chem. Phys."},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Gillespie, D.T.: A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. J. Comput. Phys. 22(4), 403\u2013434 (1976). https:\/\/doi.org\/10.1016\/0021-9991(76)90041-3, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0021999176900413","DOI":"10.1016\/0021-9991(76)90041-3"},{"issue":"11","key":"12_CR11","doi-asserted-by":"publisher","first-page":"1367","DOI":"10.1287\/mnsc.35.11.1367","volume":"35","author":"PW Glynn","year":"1989","unstructured":"Glynn, P.W., Iglehart, D.L.: Importance sampling for stochastic simulations. Manage. Sci. 35(11), 1367\u20131392 (1989)","journal-title":"Manage. Sci."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-642-02658-4_49","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2009","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: INFAMY: an infinite-state Markov model checker. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 641\u2013647. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_49"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-540-71209-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 72\u201386. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_8"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-75596-8_24","volume-title":"Automated Technology for Verification and Analysis","author":"T Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Providing evidence of likely being on time: counterexample generation for CTMC model checking. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 331\u2013346. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_24"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-031-43835-6_7","volume-title":"Quantitative Evaluation of Systems","author":"J Jeppson","year":"2023","unstructured":"Jeppson, J., et al.: Stamina in c++: modernizing an infinite-state probabilistic model checker. In: Jansen, N., Tribastone, M. (eds.) QEST 2023. LNCS, vol. 14287, pp. 101\u2013109. Springer Nature Switzerland, Cham (2023)"},{"issue":"16","key":"12_CR16","doi-asserted-by":"publisher","first-page":"10B619","DOI":"10.1063\/1.2987701","volume":"129","author":"H Kuwahara","year":"2008","unstructured":"Kuwahara, H., Mura, I.: An efficient and exact stochastic simulation method to analyze rare events in biochemical systems. J. Chem. Phys. 129(16), 10B619 (2008)","journal-title":"J. Chem. Phys."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Advances and challenges of probabilistic model checking. In: 2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pp. 1691\u20131698. IEEE (2010)","DOI":"10.1109\/ALLERTON.2010.5707120"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","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, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-030-25540-4_31","volume-title":"Computer Aided Verification","author":"T Neupane","year":"2019","unstructured":"Neupane, T., Myers, C.J., Madsen, C., Zheng, H., Zhang, Z.: STAMINA: STochastic approximate model-checker for INfinite-state analysis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 540\u2013549. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_31"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Nielsen, A.A.K., et al.: Genetic circuit design automation. Science 352(6281) (2016). https:\/\/doi.org\/10.1126\/science.aac7341, https:\/\/www.sciencemag.org\/lookup\/doi\/10.1126\/science.aac7341","DOI":"10.1126\/science.aac7341"},{"issue":"17","key":"12_CR22","doi-asserted-by":"publisher","first-page":"174106","DOI":"10.1063\/1.3493460","volume":"133","author":"MK Roh","year":"2010","unstructured":"Roh, M.K., Gillespie, D.T., Petzold, L.R.: State-dependent biasing method for importance sampling in the weighted stochastic simulation algorithm. J. Chem. Phys. 133(17), 174106 (2010)","journal-title":"J. Chem. Phys."},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-28756-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Wimmer","year":"2012","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299\u2013314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_21"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-68416-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,28]],"date-time":"2024-08-28T07:07:23Z","timestamp":1724828843000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-68416-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031684159","9783031684166"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-68416-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All Python scripts used in this work are accessible at .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Additional Information"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Calgary, AB","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}