{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T10:40:07Z","timestamp":1751798407717,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319991535"},{"type":"electronic","value":"9783319991542"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_9","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T18:14:35Z","timestamp":1534270475000},"page":"140-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Incremental Verification of Parametric and Reconfigurable Markov Chains"],"prefix":"10.1007","author":[{"given":"Paul","family":"Gainer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_30"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bohnenkamp, H., van der Stok, P., Hermanns, H., Vaandrager, F.: Cost-optimization of the IPv4 zeroconf protocol, pp. 531\u2013540. IEEE Computer Society Press (2003)","DOI":"10.1109\/DSN.2003.1209963"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Dehnert, C., et al.: PROPhESY: a probabilistic parameter synthesis tool. In: CAV, pp. 214\u2013231 (2015)","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"9_CR6","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":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-35632-2_30","volume-title":"Runtime Verification","author":"V Forejt","year":"2013","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 314\u2013319. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_30"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-66335-7_14","volume-title":"Quantitative Evaluation of Systems","author":"P Gainer","year":"2017","unstructured":"Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: Investigating parametric influence on discrete synchronisation protocols using quantitative model checking. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 224\u2013239. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_14"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: The power of synchronisation: formal analysis of power consumption in networks of pulse-coupled oscillators. arXiv preprint arXiv:1709.04385 (2017)","DOI":"10.1007\/978-3-030-02450-5_10"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_56"},{"issue":"1","key":"9_CR11","doi-asserted-by":"publisher","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. STTT 13(1), 3\u201319 (2011)","journal-title":"STTT"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"9_CR13","unstructured":"Hopcroft, J.E.: Introduction to Automata Theory, Languages, and Computation. Pearson Education India (2008)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Jansen, N., et al.: Accelerating parametric probabilistic verification. In: QEST, pp. 404\u2013420 (2014)","DOI":"10.1007\/978-3-319-10696-0_31"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Johnson, B., Kress-Gazit, H.: Probabilistic analysis of correctness of high-level robot behavior with sensor error. In: Robotics: Science and Systems (2011)","DOI":"10.15607\/RSS.2011.VII.020"},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s10514-012-9301-4","volume":"33","author":"B Johnson","year":"2012","unstructured":"Johnson, B., Kress-Gazit, H.: Probabilistic guarantees for high-level robot behavior in the presence of sensor error. Auton. Robots 33(3), 309\u2013321 (2012)","journal-title":"Auton. Robots"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Johnson, B.L.: Synthesis, analysis, and revision of correct-by-construction controllers for robots with sensing and actuation errors. Ph.D. thesis, Cornell University (2015)","DOI":"10.1177\/0278364914562980"},{"key":"9_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov chains: with a chapter of Markov random fields by David Griffeath","author":"JG Kemeny","year":"2012","unstructured":"Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov chains: with a chapter of Markov random fields by David Griffeath, vol. 40. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220\u2013270. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6"},{"key":"9_CR20","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":"9_CR21","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: International Conference on Dependable Systems & Networks, pp. 359\u2013370. IEEE (2011)","DOI":"10.1109\/DSN.2011.5958249"},{"issue":"6","key":"9_CR22","doi-asserted-by":"publisher","first-page":"1645","DOI":"10.1137\/0150098","volume":"50","author":"RE Mirollo","year":"1990","unstructured":"Mirollo, R.E., Strogatz, S.H.: Synchronization of pulse-coupled biological oscillators. SIAM J. Appl. Math. 50(6), 1645\u20131662 (1990)","journal-title":"SIAM J. Appl. Math."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.: Parameter synthesis for Markov models: faster than ever. In: ATVA, pp. 50\u201367 (2016)","DOI":"10.1007\/978-3-319-46520-3_4"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T10:15:28Z","timestamp":1751796928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}