{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:34:48Z","timestamp":1742956488524,"version":"3.40.3"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757747"},{"type":"electronic","value":"9783031757754"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75775-4_3","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:02:41Z","timestamp":1731398561000},"page":"46-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Revisiting a Pioneering Concurrent Stochastic Problem: 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"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"issue":"1","key":"3_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 in System Design 15(1), 7\u201348 (1999). https:\/\/doi.org\/10.1023\/A:1008739929481","journal-title":"Formal Methods in System Design"},{"key":"3_CR2","unstructured":"ANSI: Ada Programming Language. Military Standard ANSI-MIL-STD-1815A, American National Standards Institute, New Year, USA (Jan 1983)"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying Continuous Time Markov Chains. In: Alur, R., Henzinger, T.A. (eds.) Proceedings of the 8th International Conference on Computer Aided Verification (CAV\u201996), New Brunswick, NJ, USA. Lecture Notes in Computer Science, vol.\u00a01102, pp. 269\u2013276. Springer (Jul 1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_75","DOI":"10.1007\/3-540-61474-5_75"},{"issue":"6","key":"3_CR4","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.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Transactions on Software Engineering 29(6), 524\u2013541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"9","key":"3_CR5","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Performance Evaluation and Model Checking Join Forces. Communications of the ACM 53(9), 76\u201385 (2010). https:\/\/doi.org\/10.1145\/1810891.1810912","journal-title":"Communications of the ACM"},{"key":"3_CR6","unstructured":"Barrett, G.: OCCAM 3 Reference Manual (Mar 1992), iNMOS Limited, Draft"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Cleaveland, R., Sims, S., Stewart, W.: TwoTowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems. In: Budkowski, S., Cavalli, A.R., Najm, E. (eds.) Proceedings of the IFIP TC6\/WG6.1 Joint 11th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and 18th International Workshop on Protocol Specification, Testing and Verification (FORTE\/PSTV\u201998), Paris, France. IFIP Conference Proceedings, vol.\u00a0135, pp. 457\u2013467. Kluwer (Nov 1998)","DOI":"10.1007\/978-0-387-35394-4_28"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Bohnenkamp, H., Pedro R. d\u2019Argenio, Hermanns, H., Katoen, J.P.: MoDeST: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE Transactions on Software Engineering 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","DOI":"10.1109\/TSE.2006.104"},{"issue":"5","key":"3_CR9","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/COMJNL\/BXQ024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, Dependability and Performance Analysis of Extended AADL Models. The Computer Journal 54(5), 754\u2013775 (2011). https:\/\/doi.org\/10.1093\/COMJNL\/BXQ024","journal-title":"The Computer Journal"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Bravetti, M., Bernardo, M.: Compositional Asymmetric Cooperations for Process Algebras with Probabilities, Priorities, and Time. In: Corradini, F., Inverardi, P. (eds.) Proceedings of the International Workshop on Models for Time-Critical Systems (MTCS\u201900), State College, PA, USA. Electronic Notes in Theoretical Computer Science, vol.\u00a039, pp. 197\u2013230. Elsevier (Aug 2000). https:\/\/doi.org\/10.1016\/S1571-0661(05)80749-2","DOI":"10.1016\/S1571-0661(05)80749-2"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Brinksma, E., Hermanns, H.: Process Algebra and Markov Chains. In: Brinksma, E., Hermanns, H., Katoen, J. (eds.) Revised Lectures on Formal Methods and Performance Analysis, First EEF\/Euro Summer School on Trends in Computer Science, Berg en Dal, The Netherlands. Lecture Notes in Computer Science, vol.\u00a02090, pp. 183\u2013231. Springer (Jul 2000). https:\/\/doi.org\/10.1007\/3-540-44667-2_5","DOI":"10.1007\/3-540-44667-2_5"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. J. ACM 31(3), 560\u2013599 (1984). https:\/\/doi.org\/10.1145\/828.833","journal-title":"J. ACM"},{"issue":"1","key":"3_CR13","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and Ordinary Lumpability in Finite Markov Chains. Journal of Applied Probability 31(1), 59\u201375 (1994). https:\/\/doi.org\/10.2307\/3215235","journal-title":"Journal of Applied Probability"},{"key":"3_CR14","unstructured":"Buchholz, P.: Markovian Process Algebra: Composition and Equivalence. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the 2nd Workshop on Process Algebras and Performance Modelling (PAPM\u201994), Regensberg\/Erlangen, Germany. pp. 11\u201330 (Jul 1994)"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Buchholz, P., Kemper, P.: Quantifying the Dynamic Behavior of Process Algebras. In: de\u00a0Alfaro, L., Gilmore, S. (eds.) Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV\u201901), Aachen, Germany. Lecture Notes in Computer Science, vol.\u00a02165, pp. 184\u2013199. Springer (Sep 2001). https:\/\/doi.org\/10.1007\/3-540-44804-7_12","DOI":"10.1007\/3-540-44804-7_12"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., K\u0159et\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: 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\u201920), Rhodes, Greece. Lecture Notes in Computer Science, vol. 12479, pp. 216\u2013241. Springer (Oct 2020). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"3_CR17","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.3) (May 2024), https:\/\/cadp.inria.fr\/publications\/Champelovier-Clerc-Garavel-et-al-10.html, INRIA, Grenoble, France"},{"key":"3_CR18","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-16561-0_18","DOI":"10.1007\/978-3-642-16561-0_18"},{"key":"3_CR19","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_18","DOI":"10.1007\/978-3-642-02658-4_18"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Katoen, J.: A Theory of Stochastic Systems, Part I: Stochastic Automata. Information and Computation 203(1), 1\u201338 (2005). https:\/\/doi.org\/10.1016\/J.IC.2005.07.001","DOI":"10.1016\/J.IC.2005.07.001"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Esteve, M., Katoen, J., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal Correctness, Safety, Dependability, and Performance Analysis of a Satellite. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) Proceedings of the 34th International Conference on Software Engineering, (ICSE\u201912), Zurich, Switzerland. pp. 1022\u20131031. IEEE Computer Society (Jun 2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227118","DOI":"10.1109\/ICSE.2012.6227118"},{"issue":"2","key":"3_CR22","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. Performance Evaluation 18(2), 149\u2013171 (1993). https:\/\/doi.org\/10.1016\/0166-5316(93)90035-S","journal-title":"Performance Evaluation"},{"key":"3_CR23","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/3-540-45614-7_23, full version available as INRIA Research Report 4492","DOI":"10.1007\/3-540-45614-7_23"},{"key":"3_CR24","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":"3_CR25","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 2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","DOI":"10.1007\/s10009-012-0244-z"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd \u2013 Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 10500, pp. 3\u201326. Springer (Oct 2017). https:\/\/doi.org\/10.1007\/978-3-319-68270-9_1","DOI":"10.1007\/978-3-319-68270-9_1"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Garavel, H., Serwe, W.: The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark. In: Hermanns, H., H\u00f6fner, P. (eds.) Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS\u201917), Uppsala, Sweden. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0244, pp. 230\u2013270 (Apr 2017). https:\/\/doi.org\/10.4204\/EPTCS.244.10","DOI":"10.4204\/EPTCS.244.10"},{"issue":"25","key":"3_CR28","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"DT Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact Stochastic Simulation of Coupled Chemical Reactions. The Journal of Physical Chemistry 81(25), 2340\u20132361 (1977). https:\/\/doi.org\/10.1021\/j100540a008","journal-title":"The Journal of Physical Chemistry"},{"issue":"2","key":"3_CR29","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10703-012-0167-Z","volume":"43","author":"E Hahn","year":"2013","unstructured":"Hahn, E., 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":"3_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2015.08.009","volume":"112","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: In the Quantitative Automata Zoo. Science of Computer Programming 112, 3\u201323 (2015). https:\/\/doi.org\/10.1016\/j.scico.2015.08.009","journal-title":"Science of Computer Programming"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The Quantitative Verification Benchmark Set. In: Vojnar, T., Zhang, L. (eds.) Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919), Prague, Czech Republic. Lecture Notes in Computer Science, vol. 11427, pp. 344\u2013350. Springer (Apr 2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"issue":"4","key":"3_CR32","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., Quatmann, T., Volk, M.: The Probabilistic Model Checker Storm. International Journal on Software Tools for Technology Transfer 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality, Lecture Notes in Computer Science, vol.\u00a02428. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45804-2","DOI":"10.1007\/3-540-45804-2"},{"issue":"1\u20134","key":"3_CR34","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. Performance Evaluation 39(1\u20134), 5\u201335 (2000). https:\/\/doi.org\/10.1016\/S0166-5316(99)00056-5","journal-title":"Performance Evaluation"},{"key":"3_CR35","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"},{"key":"3_CR36","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/3-540-36577-X_30","DOI":"10.1007\/3-540-36577-X_30"},{"key":"3_CR37","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":"3_CR38","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Ph.D. thesis, University of Edinburgh, Scotland, United Kingdom (Dec 1994), https:\/\/hdl.handle.net\/1842\/15027"},{"key":"3_CR39","unstructured":"Hillston, J.: The Nature of Synchronisation. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the 2nd Workshop on Process Algebras and Performance Modelling (PAPM\u201994), Regensberg\/Erlangen, Germany. pp. 143\u2013160 (Jul 1994), https:\/\/www.researchgate.net\/publication\/2311019"},{"issue":"8","key":"3_CR40","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"3_CR41","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ (1985)"},{"key":"3_CR42","unstructured":"INMOS Limited: OCCAM 2 Reference Manual. International Series in Computer Science, Prentice-Hall (1988)"},{"key":"3_CR43","unstructured":"ISO\/IEC: LOTOS \u2013 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard\u00a08807, International Organization for Standardization \u2013 Information Processing Systems \u2013 Open Systems Interconnection, Geneva (Sep 1989)"},{"key":"3_CR44","unstructured":"ISO\/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization \u2013 Information Technology, Geneva (Sep 2001)"},{"key":"3_CR45","doi-asserted-by":"publisher","unstructured":"Katoen, J.P.: Quantitative and Qualitative Extensions of Event Structures. Ph.D. thesis, University of Twente, The Netherlands (Apr 1996). https:\/\/doi.org\/10.3990\/1.9789036507998","DOI":"10.3990\/1.9789036507998"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Katoen, J.: The Probabilistic Model Checking Landscape. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, (LICS\u201916), New York, NY, USA. pp. 31\u201345. ACM (Jul 2016). https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Katoen, J., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. In: Grumberg, O., Huth, M. (eds.) Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907), Braga, Portugal. Lecture Notes in Computer Science, vol.\u00a04424, pp. 87\u2013101. Springer (Mar\u2013Apr 2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_9","DOI":"10.1007\/978-3-540-71209-1_9"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains, Graduate Texts in Mathematics, vol.\u00a040. Springer-Verlag, 2nd edn. (1976)","DOI":"10.1007\/978-1-4684-9455-6_2"},{"key":"3_CR49","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":"3_CR50","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM Benchmark Suite. In: Proceedings of the 9th International Conference on Quantitative Evaluation of Systems (QEST\u201912), London, UK. pp. 203\u2013204. IEEE Computer Society (Sep 2012). https:\/\/doi.org\/10.1109\/QEST.2012.14, https:\/\/prismmodelchecker.org\/benchmarks","DOI":"10.1109\/QEST.2012.14"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Lang, F.: Compositional Verification using SVL Scripts. In: Katoen, J.P., Stevens, P. (eds.) Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), Grenoble, France. Lecture Notes in Computer Science, vol.\u00a02280, pp. 465\u2013469. Springer (Apr 2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_33","DOI":"10.1007\/3-540-46002-0_33"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Lindemann, C.: Employing the Randomization Technique for Solving Stochastic Petri Net Models. In: Lehmann, A., Lehmann, F. (eds.) Proceedings of the 6th GI\/ITG Conference on Modelling, Measurement and Evaluation of Computing Systems (MMB\u201991), Neubiberg, Germany. Informatik-Fachberichte, vol.\u00a0286, pp. 306\u2013319. Springer (Sep 1991). https:\/\/doi.org\/10.1007\/978-3-642-76934-4_21","DOI":"10.1007\/978-3-642-76934-4_21"},{"issue":"7","key":"3_CR53","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. Science of Computer Programming 78(7), 843\u2013861 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.01.003","journal-title":"Science of Computer Programming"},{"issue":"4","key":"3_CR54","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/948176.948183","volume":"18","author":"D May","year":"1983","unstructured":"May, D.: OCCAM. SIGPLAN Notices 18(4), 69\u201379 (1983). https:\/\/doi.org\/10.1145\/948176.948183","journal-title":"OCCAM. SIGPLAN Notices"},{"key":"3_CR55","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":"3_CR56","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1989)"},{"key":"3_CR57","unstructured":"Sighireanu, M., Catry, A., Champelovier, D., Garavel, H., Lang, F., Schaeffer, G., Serwe, W., Stoecker, J.: LOTOS NT User\u2019s Manual (Version 3.14) (Jun 2024), INRIA\/CONVECS, Grenoble, France, https:\/\/vasy.inria.fr\/ftp\/traian\/manual.pdf, 88 pages"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75775-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:02:51Z","timestamp":1731398571000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75775-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757747","9783031757754"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75775-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}