{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T19:13:18Z","timestamp":1760728398030,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032052902"},{"type":"electronic","value":"9783032052919"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"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-032-05291-9_20","type":"book-chapter","created":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T14:08:24Z","timestamp":1758722904000},"page":"475-493","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["PMaude Revisited Through Probabilistic Strategies"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2983-3404","authenticated-orcid":false,"given":"Rub\u00e9n","family":"Rubio","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9716-4612","authenticated-orcid":false,"given":"Adri\u00e1n","family":"Riesco","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-762X","authenticated-orcid":false,"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. In: Cerone, A., Wiklicky, H. (eds.) QAPL 2005. Electronic Notes in Theoretical Computer Science, vol. 153, no. 2, pp. 213\u2013239. Elsevier (2005). https:\/\/doi.org\/10.1016\/J.ENTCS.2005.10.040","DOI":"10.1016\/J.ENTCS.2005.10.040"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_28"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Bentea, L., \u00d6lveczky, P.C.: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing. In: Mart\u00ed-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol.\u00a07841, pp. 77\u201394. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-37635-1_5","DOI":"10.1007\/978-3-642-37635-1_5"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236, 35\u2013132 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00206-6","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"20_CR7","unstructured":"Clavel, M., et al.: Maude Manual (version 3.5) (2024), https:\/\/maude.lcc.uma.es\/maude-manual\/"},{"key":"20_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2025.101048","volume":"144","author":"F Dur\u00e1n","year":"2025","unstructured":"Dur\u00e1n, F., Ram\u00edrez, C., Rocha, C., Pozas, N.: A rewriting logic semantics for the analysis of P programs. J. Logical Algebraic Methods Program. 144, 101048 (2025). https:\/\/doi.org\/10.1016\/j.jlamp.2025.101048","journal-title":"J. Logical Algebraic Methods Program."},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Rocha, C., Sala\u00fcn, G.: Stochastic analysis of BPMN with time in rewriting logic. Sci. Comput. Program. 168, 1\u201317 (2018). https:\/\/doi.org\/10.1016\/j.scico.2018.08.007","DOI":"10.1016\/j.scico.2018.08.007"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Verdejo, A.: The Maude strategy language. J. Log. Algebraic Methods Program. 134, 100887 (2023). https:\/\/doi.org\/10.1016\/J.JLAMP.2023.100887","DOI":"10.1016\/J.JLAMP.2023.100887"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-319-10431-7_12","volume-title":"Software Engineering and Formal Methods","author":"J Grov","year":"2014","unstructured":"Grov, J., \u00d6lveczky, P.C.: Increasing consistency in multi-site data stores: megastore-CGC and its formal analysis. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 159\u2013174. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_12"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","DOI":"10.1007\/S10009-021-00633-Z"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-68863-1_10","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M Katelman","year":"2008","unstructured":"Katelman, M., Meseguer, J., Hou, J.: Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 150\u2013169. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_10"},{"key":"20_CR14","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":"20_CR15","doi-asserted-by":"publisher","unstructured":"Liu, S., Ganhotra, J., Rahman, M.R., Nguyen, S., Gupta, I., Meseguer, J.: Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Trans. Embed. Syst. 4(1), 03:1\u201303:26 (2017). https:\/\/doi.org\/10.4230\/LITES-V004-I001-A003","DOI":"10.4230\/LITES-V004-I001-A003"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563299","DOI":"10.1145\/3563299"},{"issue":"1","key":"20_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11730637_35","volume-title":"Hybrid Systems: Computation and Control","author":"J Meseguer","year":"2006","unstructured":"Meseguer, J., Sharykin, R.: Specification and analysis of distributed object-based stochastic hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 460\u2013475. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_35"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The real-time maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Rubio, R.: Maude as a library: an efficient all-purpose programming interface. In: Bae, K. (ed.) WRLA@ETAPS 2022. LNCS, vol. 13252, pp. 274\u2013294. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_14","DOI":"10.1007\/978-3-031-12441-9_14"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. J. Log. Algebraic Methods Program. 123, 100700 (2021). https:\/\/doi.org\/10.1016\/J.JLAMP.2021.100700","DOI":"10.1016\/J.JLAMP.2021.100700"},{"key":"20_CR22","unstructured":"Rubio, R.: Unified Maude model-checking tool (umaudemc) (2020\u20132025), https:\/\/github.com\/fadoss\/umaudemc"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: QMaude: quantitative specification and verification in rewriting logic. In: Chechik, M., Katoen, J., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 240\u2013259. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_15","DOI":"10.1007\/978-3-031-27481-7_15"},{"key":"20_CR24","unstructured":"Rubio, R., et\u00a0al.: Repository of examples of the Maude strategy language (2021\u20132025), https:\/\/github.com\/fadoss\/strat-examples"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Horv\u00e1th, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) ValueTools 2013, pp. 310\u2013315. ICST\/ACM (2013). https:\/\/doi.org\/10.4108\/ICST.VALUETOOLS.2013.254377","DOI":"10.4108\/ICST.VALUETOOLS.2013.254377"}],"container-title":["Lecture Notes in Computer Science","Concurrent Programming, Open Systems and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05291-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T18:32:25Z","timestamp":1760725945000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05291-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032052902","9783032052919"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05291-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the contents of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}