{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T20:59:44Z","timestamp":1757624384050,"version":"3.44.0"},"publisher-location":"Cham","reference-count":81,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031974380"},{"type":"electronic","value":"9783031974397"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"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":[[2026]]},"DOI":"10.1007\/978-3-031-97439-7_7","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:03Z","timestamp":1756551843000},"page":"158-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Probabilistic Model Checking: Applications and\u00a0Trends"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9326-4344","authenticated-orcid":false,"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"111275","DOI":"10.1016\/j.jss.2022.111275","volume":"188","author":"N Alasmari","year":"2022","unstructured":"Alasmari, N., Calinescu, R., Paterson, C., Mirandola, R.: Quantitative verification with adaptive uncertainty reduction. J. Syst. Softw. 188, 111275 (2022)","journal-title":"J. Syst. Softw."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Alexiou, N., Basagiannis, S., Katsaros, P., Deshpande, T., Smolka, S.A.: Formal analysis of the Kaminsky DNS cache-poisoning attack using probabilistic model checking. In: Proceedings 9th IEEE International Symposim on High Assurance Systems Engineering (HASE 2010), pp. 94\u2013103. IEEE Computer Society (2010)","DOI":"10.1109\/HASE.2010.25"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counter examples. In: Proceedings 6th International Conference on Quantitative Evaluation of Systems (QEST 2009), pp. 299\u2013308. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.8"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Andrei, O., Calder, M., Higgs, M., Girolami, M.: Probabilistic model checking of DTMC models of user activity patterns. In: Proceedings of the 11th International Conference on Quantitative Evaluation of Systems (QEST 2014). LNCS, vol. 8657, pp. 138\u2013153. Springer (2014)","DOI":"10.1007\/978-3-319-10696-0_11"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., et al.: Tools at the frontiers of quantitative verification. In: TOOLympics Challenge 2023, pp. 90\u2013146. Springer (2024)","DOI":"10.1007\/978-3-031-67695-6_4"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Proceedings of the 8th International Conference on Computer Aided Verification (CAV 1996). LNCS, vol.\u00a01102, pp. 269\u2013276. Springer (1996)","DOI":"10.1007\/3-540-61474-5_75"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Proc. 24th International Colloquium on Automata, Languages and Programming (ICALP 1997). LNCS, vol.\u00a01256, pp. 430\u2013440. Springer (1997)","DOI":"10.1007\/3-540-63165-8_199"},{"issue":"6","key":"7_CR8","doi-asserted-by":"publisher","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.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"9","key":"7_CR9","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010)","journal-title":"Commun. ACM"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Baier, C., Daum, M., Dubslaff, C., Klein, J., Kl\u00fcppelholz, S.: Energy-utility quantiles. In: NASA Formal Methods. LNCS, vol. 8430, pp. 285\u2013299. Springer (2014)","DOI":"10.1007\/978-3-319-06200-6_24"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: Proc. 23rd International Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS 2014), pp. 1:1\u20131:10. ACM (2014)","DOI":"10.1145\/2603088.2603089"},{"issue":"20","key":"7_CR13","doi-asserted-by":"publisher","first-page":"2019","DOI":"10.1016\/j.tcs.2010.02.010","volume":"411","author":"P Ballarini","year":"2010","unstructured":"Ballarini, P., Guerriero, M.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theoret. Comput. Sci. 411(20), 2019\u20132036 (2010)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Ben-Othman, J., Mokdad, L.: Quantitative verification of WiMAX traffic shaping solutions. In: Proceedings of the 7th International Symposium on Intelligent System Techniques for Ad hoc and Wireless Sensor Networks (IST-AWSN) (2012)","DOI":"10.1016\/j.procs.2012.06.142"},{"issue":"4","key":"7_CR15","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.cose.2011.02.001","volume":"30","author":"S Basagiannis","year":"2011","unstructured":"Basagiannis, S., Petridou, S.G., Alexiou, N., Papadimitriou, G.I., Katsaros, P.: Quantitative analysis of a certified e-mail protocol in mobile environments: a probabilistic model checking approach. Comput. Secur. 30(4), 257\u2013272 (2011)","journal-title":"Comput. Secur."},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Bertolini, C., Mota, A.: Using probabilistic model checking to evaluate GUI testing techniques. In: SEFM, pp. 115\u2013124. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.28"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Bordais, B., H\u00e9lou\u00ebt, L., Mari, T., Parreaux, J., Sankur, O.: Performance evaluation of metro regulations using probabilistic model-checking. In: RSSRail. LNCS, vol. 11495, pp. 59\u201376. Springer (2019)","DOI":"10.1007\/978-3-030-18744-6_4"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Bianco, A., de\u00a0Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1995). LNCS, vol.\u00a01026, pp. 499\u2013513. Springer (1995)","DOI":"10.1007\/3-540-60692-0_70"},{"key":"7_CR19","unstructured":"Bruna, M., Grigore, R., Kiefer, S., Ouaknine, J., Worrell, J.: Proving the Herman-protocol conjecture. In: Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). LIPIcs, vol.\u00a055, pp. 104:1\u2013104:12 (2016)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Budd, M., et al.: Probabilistic planning for AUV data harvesting from smart underwater sensor networks. In: Proceedings of the IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS 2022), pp. 12051\u201312057 (2022)","DOI":"10.1109\/IROS47612.2022.9981460"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification: QComp 2020 competition report. In: Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020). LNCS, vol. 12479, pp. 216\u2013241. Springer (2020)","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Calinescu, R., et al.: Controller synthesis for autonomous systems with deep-learning perception components. IEEE Trans. Softw. Eng. 50(6) (2024)","DOI":"10.1109\/TSE.2024.3385378"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Garlan, D., Schmerl, B.R., Pandey, A.: Optimal planning for architecture-based self-adaptation via model checking of stochastic games. In: Proceedings of the 30th ACM Symposium on Applied Computing (SAC 2015), pp. 428\u2013435. ACM (2015)","DOI":"10.1145\/2695664.2695680"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Chen, M., Mokdad, L., Ben-Othman, J., Fourneau, J.M.: Probabilistic performance evaluation of the class-A device in LoRaWAN protocol on the MAC layer. Perform. Eval. 166(C) (2024)","DOI":"10.1016\/j.peva.2024.102446"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Chen, S., Feng, L., Rickels, M.R., Peleckis, A., Sokolsky, O., Lee, I.: A data-driven behavior modeling and analysis framework for diabetic patients on insulin pumps. In: International Conference on Healthcare Informatics, pp. 213\u2013222 (2015)","DOI":"10.1109\/ICHI.2015.33"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers. In: Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS 2012), pp. 263\u2013272 (2012)","DOI":"10.1109\/RTSS.2012.77"},{"issue":"1","key":"7_CR27","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon, P., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30(1), 45\u201375 (2018)","journal-title":"Formal Aspects Comput."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Chrszon, P., et al.: Model checking of spacecraft operational designs: a scalability analysis. Softw. Syst. Model. (2025)","DOI":"10.1007\/s10270-025-01281-6"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Ciocchetta, F., Hillston, J.: Bio-PEPA for epidemiological models. In: Proceedings of the 4th International Workshop on Practical Applications of Stochastic Modelling (PASM 2009). ENTCS, vol.\u00a0261, pp. 43\u201369. Elsevier (2008)","DOI":"10.1016\/j.entcs.2010.01.005"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Clijmans, J., Roy, M., Davis, J.: Looking beyond the past: Analyzing the intrinsic playing style of soccer teams. In: Machine Learning and Knowledge Discovery in Databases. LNCS, vol. 13718, pp. 370\u2013385 (2023)","DOI":"10.1007\/978-3-031-26422-1_23"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite state probabilistic programs. In: Proceedings of the 29th Symposium on Foundations of Computer Science (FOCS 1988), pp. 338\u2013345. IEEE CS Press (1988)","DOI":"10.1109\/SFCS.1988.21950"},{"key":"7_CR32","unstructured":"Das, S., Sharma, A.: Probabilistic model checking of temporal interaction dynamics in the supreme court. In: Proceedings of the 11th International Symposium From Data to Models and Back (DataMod 2023) (2023)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Dombrowski, C., Junges, S., Katoen, J.P., Gross, J.: Model-checking assisted protocol design for ultra-reliable low-latency wireless networks. In: Proceedings of the IEEE 35th Symposium on Reliable Distributed Systems (SRDS 2016), pp. 307\u2013316 (2016)","DOI":"10.1109\/SRDS.2016.048"},{"issue":"6","key":"7_CR34","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. J. Softw. Tools Technol. Transf. 8(6), 621\u2013632 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Eiras, F., Lahijanian, M., Kwiatkowska, M.: Correct-by-construction advanced driver assistance systems based on a cognitive architecture. In: Proceedings of the IEEE 2nd Connected and Automated Vehicles Symposium (CAVS 2019), pp.\u00a01\u20137 (2019)","DOI":"10.1109\/CAVS.2019.8887768"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Emunds, T., Nie\u00dfen, N.: Evaluating railway junction infrastructure: a queueing-based, timetable-independent analysis. Transp. Res. Part C: Emerg. Technol. 165 (2024)","DOI":"10.1016\/j.trc.2024.104704"},{"issue":"4","key":"7_CR37","first-page":"1","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4), 1\u201321 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Controller synthesis for autonomous systems interacting with human operators. In: Proceedings of the ACM\/IEEE 6th International Conference on Cyber-Physical Systems (ICCPS 2015), pp. 70\u201379. ACM (2015)","DOI":"10.1145\/2735960.2735973"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Ghadhab, M., Junges, S., Katoen, J.-P., Kuntz, M., Volk, M.: Model-based safety analysis for vehicle guidance systems. In: Proceedings of the 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2017). LNCS, vol. 10488, pp. 3\u201319. Springer (2017)","DOI":"10.1007\/978-3-319-66266-4_1"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Glazier, T.J., C\u00e1mara, J., Schmerl, B.R., Garlan, D.: Analyzing resilience properties of different topologies of collective adaptive systems. In: SASO Workshops, pp. 55\u201360. IEEE Computer Society (2015)","DOI":"10.1109\/SASOW.2015.14"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Greifeneder, J., Frey, J.: Optimizing quality of control in networked automation systems using probabilistic models. In: Proceedings of the 11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2006), pp. 372\u2013379 (2006)","DOI":"10.1109\/ETFA.2006.355428"},{"issue":"5","key":"7_CR42","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). LNCS, vol. 8413, pp. 593\u2013598. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"7_CR44","unstructured":"Haverkort, B., Cloth, L., Hermanns, H., Katoen, J.P., Baier, C.: Model checking performability properties. In: Proceedings of the International Conference on Dependable Systems and Networks (DSN 2002). IEEE CS Press (2002)"},{"issue":"3","key":"7_CR45","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/MRA.2016.2636359","volume":"24","author":"N Hawes","year":"2017","unstructured":"Hawes, N., et al.: The STRANDS project: long-term autonomy in everyday environments. IEEE Robot. Autom. Mag. 24(3), 146\u2013156 (2017)","journal-title":"IEEE Robot. Autom. Mag."},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"He, F., Baresi, L., Ghezzi, C., Spoletini, P.: Formal analysis of publish-subscribe systems by probabilistic timed automata. In: Proceedings of the Formal Techniques for Networked and Distributed Systems (FORTE 2007). LNCS, vol. 4574, pp. 247\u2013262. Springer (2007)","DOI":"10.1007\/978-3-540-73196-2_16"},{"issue":"4","key":"7_CR47","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"7_CR48","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Hoque, K.A., Mohamed, O.A., Savaria, Y.: Towards an accurate reliability, availability and maintainability analysis approach for satellite systems based on probabilistic model checking. In: Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE 2015), pp. 1635\u20131640. ACM (2015)","DOI":"10.7873\/DATE.2015.0817"},{"issue":"19","key":"7_CR50","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1093\/bioinformatics\/btg015","volume":"1","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 1(19), 524\u2013531 (2003)","journal-title":"Bioinformatics"},{"issue":"1","key":"7_CR51","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10703-023-00442-x","volume":"62","author":"S Junges","year":"2024","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Design 62(1), 181\u2013259 (2024)","journal-title":"Formal Methods Syst. Design"},{"key":"7_CR52","doi-asserted-by":"crossref","unstructured":"Koziolek, H., Schlich, B., Bilich, C.: A large-scale industrial case study on architecture-based software reliability analysis. In: Proceedings of the IEEE 21st International Symposium on Software Reliability Engineering (ISSRE 2010), pp. 279\u2013288 (2010)","DOI":"10.1109\/ISSRE.2010.15"},{"key":"7_CR53","doi-asserted-by":"crossref","unstructured":"Kromer, J.A., M\u00e4rcker, S., Lange, S., Baier, C., Friedrich, B.M.: Decision making improves sperm chemotaxis in the presence of noise. PLoS Comput. Biol. 14(4) (2018)","DOI":"10.1371\/journal.pcbi.1006109"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Krotsiani, M., Kloukinas, C., Spanoudakis, G.: Validation of service level agreements using probabilistic model checking. In: Proceedings of the 14th IEEE International Conference on Services Computing (SCC 2017), pp. 148\u2013155 (2017)","DOI":"10.1109\/SCC.2017.26"},{"issue":"16","key":"7_CR55","doi-asserted-by":"publisher","first-page":"2793","DOI":"10.1242\/jcs.039701","volume":"122","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Heath, J.: Biological pathways as communicating computer systems. J. Cell Sci. 122(16), 2793\u20132800 (2009)","journal-title":"J. Cell Sci."},{"key":"7_CR56","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011). LNCS, vol. 6806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"7_CR57","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1146\/annurev-control-042820-010947","volume":"5","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Annu. Rev. Control Robot. Auton. Syst. 5, 385\u2013410 (2022)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"issue":"72","key":"7_CR58","doi-asserted-by":"publisher","first-page":"1470","DOI":"10.1098\/rsif.2011.0800","volume":"9","author":"M Lakin","year":"2012","unstructured":"Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. J. R. Soc. Interface 9(72), 1470\u20131485 (2012)","journal-title":"J. R. Soc. Interface"},{"key":"7_CR59","doi-asserted-by":"crossref","unstructured":"Li, N., Adepu, S., Kang, E., Garlan, D.: Explanations for human-on-the-loop: a probabilistic model checking approach. In: Proceedings of the IEEE\/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2020), pp. 181\u2013187. ACM (2020)","DOI":"10.1145\/3387939.3391592"},{"issue":"2","key":"7_CR60","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.ipl.2004.12.013","volume":"94","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: An elementary proof that Herman\u2019s ring is $$\\Theta \\mathit{(}N ^2)$$. Inf. Process. Lett. 94(2), 79\u201384 (2005)","journal-title":"Inf. Process. Lett."},{"key":"7_CR61","doi-asserted-by":"crossref","unstructured":"Moreno, G.A., C\u00e1mara, J., Garlan, D., Schmerl, B.R.: Proactive self-adaptation under uncertainty: a probabilistic model checking approach. In: Proceedings of the 10th Joint Meeting on Foundations of Software Engineering (FSE 2015), pp. 1\u201312. ACM (2015)","DOI":"10.1145\/2786805.2786853"},{"key":"7_CR62","doi-asserted-by":"crossref","unstructured":"Norman, G.: Analysing randomized distributed algorithms. In: Validation of Stochastic Systems: A Guide to Current Research. LNCS (Tutorial Volume), vol.\u00a02925, pp. 384\u2013418. Springer (2004)","DOI":"10.1007\/978-3-540-24611-4_11"},{"issue":"10","key":"7_CR63","doi-asserted-by":"publisher","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.: Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(10), 1629\u20131637 (2005)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"2","key":"7_CR64","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Design 43(2), 164\u2013190 (2013)","journal-title":"Formal Methods Syst. Design"},{"key":"7_CR65","doi-asserted-by":"crossref","unstructured":"Nuraishah, S., Jawaddi, A., Ismail, A., Sulaiman, M.S., Cardellini, V.: Analyzing energy-efficient and Kubernetes-based autoscaling of microservices using probabilistic model checking. J. Grid Comput. 23(3) (2024)","DOI":"10.1007\/s10723-024-09789-9"},{"key":"7_CR66","unstructured":"Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002)"},{"key":"7_CR67","doi-asserted-by":"publisher","first-page":"112324","DOI":"10.1016\/j.jss.2024.112324","volume":"222","author":"J P\u00e4\u00dfler","year":"2025","unstructured":"P\u00e4\u00dfler, J., ter Beek, M.H., Damiani, F., Johnsen, E.B., Tapia Tarifa, S.L.: Analysing self-adaptive systems as software product lines. J. Syst. Softw. 222, 112324 (2025)","journal-title":"J. Syst. Softw."},{"key":"7_CR68","doi-asserted-by":"publisher","first-page":"112598","DOI":"10.1109\/ACCESS.2020.3001352","volume":"8","author":"M Raitza","year":"2020","unstructured":"Raitza, M., et al.: Quantitative characterization of reconfigurable transistor logic gates. IEEE Access 8, 112598\u2013112614 (2020)","journal-title":"IEEE Access"},{"key":"7_CR69","doi-asserted-by":"crossref","unstructured":"Rungta, N., et al.: Aviation safety: modeling and analyzing complex interactions between humans and automated systems. In: Proceedings of the 3rd International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS 2013), pp. 27\u201337. ACM (2013)","DOI":"10.1145\/2494493.2494498"},{"key":"7_CR70","doi-asserted-by":"crossref","unstructured":"Rybinski, M., Szymanska, Z., Lasota, S., Gambin, A.: Modelling the efficacy of hyperthermia treatment. J. Roy. Soc. Interface 10(88) (2013)","DOI":"10.1098\/rsif.2013.0527"},{"key":"7_CR71","doi-asserted-by":"crossref","unstructured":"Sardar, M.U., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C., Kumar, A.: Performance evaluation of thermal-constrained scheduling strategies in multi-core systems. In: Proceedings of the 16th European Workshop on Computer Performance Engineering (EPEW 2019). LNCS, vol. 12039, pp. 133\u2013147. Springer (2019)","DOI":"10.1007\/978-3-030-44411-2_9"},{"key":"7_CR72","doi-asserted-by":"crossref","unstructured":"Siddique, U., Hoque, K.A., Johnson, T.T.: Formal specification and dependability analysis of optical communication networks. In: Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE 2017) (2017)","DOI":"10.23919\/DATE.2017.7927239"},{"issue":"2","key":"7_CR73","doi-asserted-by":"publisher","first-page":"102172","DOI":"10.1016\/j.ipm.2019.102172","volume":"57","author":"G Stamatelatos","year":"2020","unstructured":"Stamatelatos, G., Gyftopoulos, S., Drosatos, G., Efraimidis, P.S.: Revealing the political affinity of online entities through their twitter followers. Inf. Process. Manage. 57(2), 102172 (2020)","journal-title":"Inf. Process. Manage."},{"issue":"1\u20132","key":"7_CR74","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2006.08.042","volume":"367","author":"G Steel","year":"2006","unstructured":"Steel, G.: Formal analysis of PIN block attacks. Theoret. Comput. Sci. 367(1\u20132), 257\u2013270 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR75","doi-asserted-by":"crossref","unstructured":"Tavolato, P., Luh, R., Eresheim, S.: Formalizing real-world threat scenarios. In: Proceedings of the 8th International Conference on Information Systems Security and Privacy (ICISSP 2022), pp. 281\u2013289. SciTePress (2022)","DOI":"10.5220\/0010781300003120"},{"key":"7_CR76","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite state programs. In: Proceedings of the 26th Symposium on Foundations of Computer Science (FOCS 1985), pp. 327\u2013338. IEEE CS Press (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"7_CR77","doi-asserted-by":"crossref","unstructured":"Volk, M., Sher, F., Katoen, J.P., Stoelinga, M.: SAFEST: fault tree analysis via probabilistic model checking. In: Proceedings of the 70th Reliability and Maintainability Symposium (RAMS 2024), pp.\u00a01\u20137 (2024)","DOI":"10.1109\/RAMS51492.2024.10457719"},{"key":"7_CR78","doi-asserted-by":"crossref","unstructured":"Weik, N., Volk, M., Katoen, J., Nie\u00dfen, N.: DFT modeling approach for operational risk assessment of railway infrastructure. Int. J. Softw. Tools Technol. Transf. 24(3), 331\u2013350 (2022)","DOI":"10.1007\/s10009-022-00652-4"},{"key":"7_CR79","doi-asserted-by":"crossref","unstructured":"Younes, H., Simmons, R.: Probabilistic verification of discrete event systems using acceptance sampling. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002). LNCS, vol.\u00a02404. Springer (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"key":"7_CR80","doi-asserted-by":"crossref","unstructured":"Zheng, X., Bolton, M.L., Daly, C., Biltekoff, E.: The development of a next-generation human reliability analysis: systems analysis for formal pharmaceutical human reliability (SAFPH). Reliab. Eng. Syst. Saf. 202 (2020)","DOI":"10.1016\/j.ress.2020.106927"},{"key":"7_CR81","unstructured":"PRISM bibliography. prismmodelchecker.org\/bib.php"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T13:09:07Z","timestamp":1757423347000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}