{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:55:36Z","timestamp":1777766136349,"version":"3.51.4"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"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_2","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:03:55Z","timestamp":1756551835000},"page":"15-69","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Nondeterminism in Interactive Markov Chains, with Application to the Erlangen Mainframe"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"2_CR1","unstructured":"Baier, C.: On Algorithmic Verification Methods for Probabilistic Systems,: Habilitation thesis. Universit\u00e4t Mannheim, Germany (1998)"},{"issue":"6","key":"2_CR2","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.R., Hermanns, H., Katoen, J.P.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(6), 524\u2013541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","journal-title":"IEEE Trans. Software Eng."},{"issue":"1","key":"2_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C Baier","year":"2005","unstructured":"Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.: Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. Theoret. Comput. Sci. 345(1), 2\u201326 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Katoen, J.P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains. In: Baeten, J.C.M., Mauw, S. (eds.) Proceedings of the 10th International Conference on Concurrency Theory (CONCUR\u201999), Eindhoven, The Netherlands. Lecture Notes in Computer Science, vol.\u00a01664, pp. 146\u2013161. Springer (Aug 1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_12","DOI":"10.1007\/3-540-48320-9_12"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Bernardo, M., Corradini, F., Tesei, L.: Timed Process Calculi with Deterministic or Stochastic Delays: Commuting between Durational and Durationless Actions. Theoretical Computer Science 629, 2\u201339 (2016). https:\/\/doi.org\/10.1016\/J.TCS.2016.02.022","DOI":"10.1016\/J.TCS.2016.02.022"},{"issue":"1\u20132","key":"2_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"202","author":"M Bernardo","year":"1998","unstructured":"Bernardo, M., Gorrieri, R.: A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities. Probabilities and Time. Theoretical Computer Science 202(1\u20132), 1\u201354 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(97)00127-8","journal-title":"Probabilities and Time. Theoretical Computer Science"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1109\/TSE.2008.102","volume":"35","author":"E B\u00f6de","year":"2009","unstructured":"B\u00f6de, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J.H., Wimmer, R., Becker, B.: Compositional Dependability Evaluation for STATEMATE. IEEE Trans. Software Eng. 35(2), 274\u2013292 (2009). https:\/\/doi.org\/10.1109\/TSE.2008.102","journal-title":"IEEE Trans. Software Eng."},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Buchholz, P., Hahn, E.M., Hermanns, H., Zhang, L.: Model Checking Algorithms for CTMDPs. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911), Snowbird, UT, USA. Lecture Notes in Computer Science, vol.\u00a06806, pp. 225\u2013242. Springer (Jul 2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_19","DOI":"10.1007\/978-3-642-22110-1_19"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative Model and Tool Interaction. In: Legay, A., Margaria, T. (eds.) Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201917), Part II, Uppsala, Sweden. Lecture Notes in Computer Science, vol. 10206, pp. 151\u2013168 (Apr 2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest Approach to Markov Automata. ACM Transactions on Modeling and Computer Simulation 31(3), 14:1\u201314:34 (2021). https:\/\/doi.org\/10.1145\/3449355","DOI":"10.1145\/3449355"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Krc\u00e1l, J.: Optimal Continuous Time Markov Decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201915), Shanghai, China. Lecture Notes in Computer Science, vol.\u00a09364, pp. 166\u2013182. Springer (Oct 2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12","DOI":"10.1007\/978-3-319-24953-7_12"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-Run Rewards for Markov Automata. In: Legay, A., Margaria, T. (eds.) Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201917), Part II, Uppsala, Sweden. Lecture Notes in Computer Science, vol. 10206, pp. 188\u2013203 (Apr 2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11","DOI":"10.1007\/978-3-662-54580-5_11"},{"key":"2_CR13","unstructured":"Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 7.5) (Feb 2025), https:\/\/cadp.inria.fr\/publications\/Champelovier-Clerc-Garavel-et-al-10.html, INRIA, Grenoble, France"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Zidouni, M., Mateescu, R.: Modeling Multiprocessor Cache Protocol Impact on MPI Performance. In: Proceedings of the IEEE International Workshop on Quantitative Evaluation of Large-Scale Systems and Technologies (QuEST\u201909), Bradford, UK. pp. 1073\u20131078. IEEE Computer Society Press (May 2009)","DOI":"10.1109\/WAINA.2009.117"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten Years of Performance Evaluation for Concurrent Systems Using CADP. In: Margaria, T., Steffen, B. (eds.) Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2010 (Amirandes, Heraclion, Crete), Part II. Lecture Notes in Computer Science, vol.\u00a06416, pp. 128\u2013142. Springer (Oct 2010)","DOI":"10.1007\/978-3-642-16561-0_18"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards Performance Prediction of Compositional Models in Industrial GALS Designs. In: Bouajjani, A., Maler, O. (eds.) Proceedings of the 21th International Conference on Computer Aided Verification (CAV\u201909), Grenoble, France. Lecture Notes in Computer Science, vol.\u00a05643, pp. 204\u2013218. Springer (Jul 2009)","DOI":"10.1007\/978-3-642-02658-4_18"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0166-5316(93)90035-S","volume":"18","author":"W Fischer","year":"1993","unstructured":"Fischer, W., Meier-Hellstern, K.S.: The Markov-Modulated Poisson Process (MMPP) Cookbook. Perform. Eval. 18(2), 149\u2013171 (1993). https:\/\/doi.org\/10.1016\/0166-5316(93)90035-S","journal-title":"Perform. Eval."},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Garavel, H.: Revisiting Sequential Composition in Process Calculi. Journal of Logical and Algebraic Methods in Programming 84(6), 742\u2013762 (Nov 2015). https:\/\/doi.org\/10.1016\/j.jlamp.2015.08.001","DOI":"10.1016\/j.jlamp.2015.08.001"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Garavel, H., Hermanns, H.: On Combining Functional Verification and Performance Evaluation using CADP. In: Eriksson, L.H., Lindsay, P.A. (eds.) Proceedings of the 11th International Symposium of Formal Methods Europe (FME\u201902), Copenhagen, Denmark. Lecture Notes in Computer Science, vol.\u00a02391, pp. 410\u2013429. Springer (Jul 2002), full version available as INRIA Research Report 4492","DOI":"10.1007\/3-540-45614-7_23"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Garavel, H., Hermanns, H., Parker, D.: Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe. In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M. (eds.) Principles of Verification: Cycling the Probabilistic Landscape (Part II) \u2013 Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 15261, pp. 46\u201374. Springer (Nov 2024). https:\/\/doi.org\/10.1007\/978-3-031-75775-4","DOI":"10.1007\/978-3-031-75775-4"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201901), Cheju Island, Korea. pp. 377\u2013392. Kluwer Academic Publishers (Aug 2001). https:\/\/doi.org\/10.1007\/0-306-47003-9_24, full version available as INRIA Research Report\u00a0RR-4223","DOI":"10.1007\/0-306-47003-9_24"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2), 89\u2013107 (Apr 2011). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","DOI":"10.1007\/s10009-012-0244-z"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mounier, L.: Compositional Verification in Action. In: Howar, F., Barnat, J. (eds.) Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201918), Maynooth, Ireland \u2013 Essays Dedicated to Susanne Graf at the Occasion of Her 60th Birthday. Lecture Notes in Computer Science, vol. 11119, pp. 189\u2013210. Springer (Sep 2018)","DOI":"10.1007\/978-3-030-00244-2_13"},{"issue":"3","key":"2_CR24","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ van Glabbeek","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"G\u00f6tz, N., Herzog, U., Rettelbach, M.: Multiprocessor and Distributed System Design: The Integration of Functional Specification and Performance Analysis Using Stochastic Process Algebras. In: Donatiello, L., Nelson, R.D. (eds.) Performance Evaluation of Computer and Communication Systems, Joint Tutorial Papers of Performance\u201993 and Sigmetrics\u201993, Santa Clara, CA, USA. Lecture Notes in Computer Science, vol.\u00a0729, pp. 121\u2013146. Springer (May 1993). https:\/\/doi.org\/10.1007\/BFB0013851","DOI":"10.1007\/BFB0013851"},{"key":"2_CR26","unstructured":"Gros, T.P.: Markov Automata Taken by Storm. Master\u2019s thesis, Saarland University, Germany (Jan 2018)"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Guck, D., Han, T., Katoen, J.P., Neuh\u00e4u\u00dfer, M.R.: Quantitative Timed Analysis of Interactive Markov Chains. In: Goodloe, A., Person, S. (eds.) Proceedings of the 4th International NASA Formal Methods Symposium (NFM\u201912), Norfolk, VA, USA. Lecture Notes in Computer Science, vol.\u00a07226, pp. 8\u201323. Springer (Apr 2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_4","DOI":"10.1007\/978-3-642-28891-3_4"},{"issue":"2","key":"2_CR28","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10703-012-0167-Z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A Compositional Modelling and Analysis Framework for Stochastic Hybrid Systems. Formal Methods in System Design 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0167-Z","journal-title":"Formal Methods in System Design"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914), Grenoble, France. Lecture Notes in Computer Science, vol.\u00a08413, pp. 593\u2013598. Springer (Apr 2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"issue":"4","key":"2_CR30","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. Transfer 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"2_CR31","first-page":"135","volume":"74","author":"H Hermanns","year":"2001","unstructured":"Hermanns, H.: Construction and Verification of Performance and Reliability Models. Bulletin of the EATCS 74, 135\u2013154 (2001)","journal-title":"Bulletin of the EATCS"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality, Lecture Notes in Computer Science, vol.\u00a02428. Springer (2002)","DOI":"10.1007\/3-540-45804-2"},{"issue":"1\u20134","key":"2_CR33","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional Performance Modelling with the TIPPtool. Perform. Eval. 39(1\u20134), 5\u201335 (2000). https:\/\/doi.org\/10.1016\/S0166-5316(99)00056-5","journal-title":"Perform. Eval."},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Hermanns, H., Herzog, U., Merksiotakis, V.: Stochastic Process Algebras as a Tool for Performance and Dependability Modelling. In: Iyer, R.K. (ed.) Proceedings of the International Computer Performance and Dependability Symposium (IPDS\u201995), Erlangen, Germany. pp. 102\u2013111. IEEE (Apr 1995). https:\/\/doi.org\/10.1109\/IPDS.1995.395813","DOI":"10.1109\/IPDS.1995.395813"},{"issue":"9\u201310","key":"2_CR35","doi-asserted-by":"publisher","first-page":"901","DOI":"10.1016\/S0169-7552(97)00133-5","volume":"30","author":"H Hermanns","year":"1998","unstructured":"Hermanns, H., Herzog, U., Mertsiotakis, V.: Stochastic Process Algebras - Between LOTOS and Markov Chains. Comput. Netw. 30(9\u201310), 901\u2013924 (1998). https:\/\/doi.org\/10.1016\/S0169-7552(97)00133-5","journal-title":"Comput. Netw."},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Joubert, C.: A Set of Performance and Dependability Analysis Components for CADP. In: Garavel, H., Hatcliff, J. (eds.) Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201903), Warsaw, Poland. Lecture Notes in Computer Science, vol.\u00a02619, pp. 425\u2013430. Springer (Apr 2003)","DOI":"10.1007\/3-540-36577-X_30"},{"key":"2_CR37","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00019-2","volume-title":"Automated compositional markov chain generation for a plain-old telephone system","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.P.: Automated compositional markov chain generation for a plain-old telephone system. Sci. Comput, Program (2000)"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Katoen, J.P.: The How and Why of Interactive Markov Chains. In: de\u00a0Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) Revised Selected Papers of the 8th International Symposium on Formal Methods for Components and Objects (FMCO\u201909), Eindhoven, The Netherlands. Lecture Notes in Computer Science, vol.\u00a06286, pp. 311\u2013337. Springer (Nov 2009)","DOI":"10.1007\/978-3-642-17071-3_16"},{"key":"2_CR39","unstructured":"Hermanns, H., Rettelbach, M.: Syntax, Semantics, Equivalences, and Axioms for MTIPP. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the 2nd Workshop on Process Algebras and Performance Modelling (PAPM\u201994), Erlangen, Germany. Lecture Notes in Computer Science, vol.\u00a01601, pp. 71\u201388. University of Erlangen-N\u00fcrnberg, Germany (Jul 1994)"},{"key":"2_CR40","doi-asserted-by":"publisher","unstructured":"Herzog, U.: Formal Description, Time and Performance Analysis: A Framework. In: H\u00e4rder, T., Wedekind, H., Zimmermann, G. (eds.) Entwurf und Betrieb verteilter Systeme, Proceedings Fachtagung des Sonderforschungsbereiche 124 und 182 (Dagstuhl, Germany). Informatik-Fachberichte, vol.\u00a0264, pp. 172\u2013190. Springer (Sep 1990). https:\/\/doi.org\/10.1007\/978-3-642-76309-0_10","DOI":"10.1007\/978-3-642-76309-0_10"},{"key":"2_CR41","unstructured":"Herzog, U., Merksiotakis, V.: Stochastic Process Algebras Applied to Failure Modelling. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the 2nd Workshop on Process Algebras and Performance Modelling (PAPM\u201994), Regensberg\/Erlangen, Germany. pp. 107\u2013126 (Jul 1994), https:\/\/www.researchgate.net\/publication\/2731331"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511569951"},{"key":"2_CR43","unstructured":"Johr, S.: Model Checking Compositional Markov Systems. Ph.D. thesis, Saarland University (Aug 2007)"},{"key":"2_CR44","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Undergraduate Texts in Mathematic, Springer (1976)"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Paviot-Adet, E., Jezequel, L., Rodr\u00edguez, C., Hulin-Hubard, F.: MCC\u20192015 \u2013 The Fifth Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency XI, 262\u2013273 (2016)","DOI":"10.1007\/978-3-662-53401-4_12"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911), Snowbird, UT, USA. Lecture Notes in Computer Science, vol.\u00a06806, pp. 585\u2013591. Springer (Jul 2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: Specification and Analysis of Asynchronous Systems using CADP. In: Merz, S., Navet, N. (eds.) Modeling and Verification of Real-Time Systems \u2013 Formalisms and Software Tools, chap.\u00a05, pp. 141\u2013170. ISTE publishing \/ John Wiley (2008), http:\/\/hal.inria.fr\/inria-00264235","DOI":"10.1002\/9780470611012.ch5"},{"key":"2_CR48","unstructured":"Mateescu, R., Garavel, H.: XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In: Margaria, T. (ed.) Proceedings of the International Workshop on Software Tools for Technology Transfer (STTT\u201998), Aalborg, Denmark. pp. 33\u201342. BRICS (Jul 1998)"},{"issue":"7","key":"2_CR49","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1016\/j.scico.2012.01.003","volume":"78","author":"R Mateescu","year":"2013","unstructured":"Mateescu, R., Serwe, W.: Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols. Sci. Comput. Program. 78(7), 843\u2013861 (2013)","journal-title":"Sci. Comput. Program."},{"key":"2_CR50","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol.\u00a092. Springer (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"2_CR51","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. Ph.D. thesis, RWTH Aachen University, Germany (2010)"},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proceedings of the 5th International Symposium on Programming, Torino, Italy. Lecture Notes in Computer Science, vol.\u00a0137, pp. 337\u2013351. Springer (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"2_CR53","doi-asserted-by":"publisher","unstructured":"Zhang, L., Neuh\u00e4u\u00dfer, M.R.: Model Checking Interactive Markov Chains. In: Esparza, J., Majumdar, R. (eds.) Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201910), Paphos, Cyprus. Lecture Notes in Computer Science, vol.\u00a06015, pp. 53\u201368. Springer (Mar 2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_5","DOI":"10.1007\/978-3-642-12002-2_5"},{"key":"2_CR54","unstructured":"Zidouni, M.: Mod\u00e9lisation et analyse des performances de la biblioth\u00e8que MPI en tenant compte de l\u2019architecture mat\u00e9rielle. Ph.D. thesis, Universit\u00e9 de Grenoble (May 2010), http:\/\/hal.inria.fr\/tel-00526164\/en"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:31:47Z","timestamp":1777476707000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}