Bibliography¶
The most relevant articles regarding umaudemc are the following:
Strategies, model checking and branching-time properties in Maude [RMOPV21] (arXiv, BibTeX) for branching-time model checking and the architecture of the tool.
Model checking of strategy-controlled systems in rewriting logic [RMOPV22b] (arXiv, BibTeX) for LTL model checking of strategy-controlled models.
QMaude: quantitative specification and verification in rewriting logic [RMOPV23] (archived, BibTeX) for the quantitative extensions.
PMaude revisited through probabilistic strategies [RRMO26] (archived, BibTeX) as an illustrative example of probability assignment methods.
References¶
Gul A. Agha, José Meseguer, and Koushik Sen. PMaude: rewrite-based specification language for probabilistic object systems. In Antonio Cerone and Herbert Wiklicky, editors, Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005, Edinburgh, UK, April 2-3, 2005, volume 153(2) of Electronic Notes in Theoretical Computer Science, 213–239. Elsevier, 2006. doi:10.1016/j.entcs.2005.10.040.
Olivier Bournez and Claude Kirchner. Probabilistic rewrite strategies. Applications to ELAN. In Sophie Tison, editor, Rewriting Techniques and Applications, 13th International Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings, volume 2378 of Lecture Notes in Computer Science, 252–266. Springer, 2002. doi:10.1007/3-540-45610-4_18.
Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mcrl2 toolset for analysing concurrent systems - improvements in expressivity and usability. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, volume 11428 of Lecture Notes in Computer Science, 21–39. Springer, 2019. doi:10.1007/978-3-030-17465-1_2.
Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn Talcott. Maude Manual v3.5.1. 7 2025. URL: https://maude.cs.illinois.edu/manual/.
Steven Eker, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Alberto Verdejo. The maude strategy language. J. Log. Algebraic Methods Program., 2023. doi:10.1016/j.jlamp.2023.100887.
Steven Eker, José Meseguer, and Ambarish Sridharanarayanan. The Maude LTL model checker. In Fabio Gadducci and Ugo Montanari, editors, Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, volume 71 of Electronic Notes in Theoretical Computer Science, 162–187. Elsevier, 2004. doi:10.1016/S1571-0661(05)82534-4.
Maribel Fernández, Hélène Kirchner, and Bruno Pinaud. Strategic port graph rewriting: an interactive modelling framework. Math. Struct. Comput. Sci., 29(5):615–662, 2019. doi:10.1017/S0960129518000270.
José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci., 96(1):73–155, 1992. doi:10.1016/0304-3975(92)90182-F.
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Model checking strategy-controlled rewriting systems (system description). In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, 34:1–34:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.FSCD.2019.34.
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Strategies, model checking and branching-time properties in maude. J. Log. Algebraic Methods Program., 123:100700, 2021. doi:10.1016/j.jlamp.2021.100700.
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Model checking strategy-controlled systems in rewriting logic. Autom. Softw. Eng., 29(1):7, 2022. doi:10.1007/s10515-021-00307-9.
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Model checking strategy-controlled systems in rewriting logic. Autom. Softw. Eng., 29(1):7, 2022. doi:10.1007/s10515-021-00307-9.
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. QMaude: quantitative specification and verification in rewriting logic. In Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker, editors, Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings, Lecture Notes in Computer Science, 240–259. Springer, 2023. doi:10.1007/978-3-031-27481-7_15.
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Specifying fairness constraints and model checking with non-intensional strategies. In Kazuhiro Ogata and Narciso Martí-Oliet, editors, Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Revised Selected Papers, volume 14953 of Lecture Notes in Computer Science, 145–162. Springer, 2024. doi:10.1007/978-3-031-65941-6_8.
Rubén Rubio, Adrián Riesco, and Narciso Martí-Oliet. Pmaude revisited through probabilistic strategies. In José Meseguer, Carlos A. Varela, and Nalini Venkatasubramanian, editors, Concurrent Programming, Open Systems and Formal Methods - Essays Dedicated to Gul Agha to Celebrate His Scientific Career, Lecture Notes in Computer Science, 475–493. Springer, 2026. doi:10.1007/978-3-032-05291-9_20.
Stefano Sebastio and Andrea Vandin. MultiVeStA: statistical model checking for discrete event simulators. In András Horváth, Peter Buchholz, Vittorio Cortellessa, Luca Muscariello, and Mark S. Squillante, editors, 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13, Torino, Italy, December 10-12, 2013, 310–315. ICST/ACM, 2013. doi:10.4108/icst.valuetools.2013.254377.