{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T01:55:55Z","timestamp":1790474155542,"version":"4.1.0"},"reference-count":67,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,12,8]],"date-time":"2021-12-08T00:00:00Z","timestamp":1638921600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,12,8]],"date-time":"2021-12-08T00:00:00Z","timestamp":1638921600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004837","name":"Ministerio de Ciencia e Innovaci\u00f3n","doi-asserted-by":"publisher","award":["PID2019-108528RB-C22"],"award-info":[{"award-number":["PID2019-108528RB-C22"]}],"id":[{"id":"10.13039\/501100004837","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014440","name":"Ministerio de Ciencia, Innovaci\u00f3n y Universidades","doi-asserted-by":"publisher","award":["FPU17\/02319"],"award-info":[{"award-number":["FPU17\/02319"]}],"id":[{"id":"10.13039\/100014440","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1007\/s10515-021-00307-9","type":"journal-article","created":{"date-parts":[[2021,12,8]],"date-time":"2021-12-08T16:03:57Z","timestamp":1638979437000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Model checking strategy-controlled systems in rewriting logic"],"prefix":"10.1007","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2983-3404","authenticated-orcid":false,"given":"Rub\u00e9n","family":"Rubio","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6576-762X","authenticated-orcid":false,"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4915-5452","authenticated-orcid":false,"given":"Isabel","family":"Pita","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7374-3214","authenticated-orcid":false,"given":"Alberto","family":"Verdejo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,12,8]]},"reference":[{"key":"307_CR1","doi-asserted-by":"publisher","unstructured":"Andrei, O., Lucanu, D.: Strategy-based proof calculus for membrane systems. In: Ro\u015fu, G. (ed), Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 238(3), pp. 23\u201343 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.05.011","DOI":"10.1016\/j.entcs.2009.05.011"},{"key":"307_CR2","doi-asserted-by":"publisher","unstructured":"Andrei, O., Ibanescu, L., Kirchner, H.: Non-intrusive formal methods and strategic rewriting for a chemical application. In: Futatsugi, K., Jouannaud, J., Meseguer, J. (eds), Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, Springer, Lecture Notes in Computer Science, vol. 4060, pp. 194\u2013215 (2006). https:\/\/doi.org\/10.1007\/11780274_11","DOI":"10.1007\/11780274_11"},{"issue":"3","key":"307_CR3","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.tcs.2006.12.016","volume":"373","author":"O Andrei","year":"2007","unstructured":"Andrei, O., Ciobanu, G., Lucanu, D.: A rewriting logic framework for operational semantics of membrane systems. Theor. Comput. Sci. 373(3), 163\u2013181 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.016","journal-title":"Theor. Comput. Sci."},{"key":"307_CR4","doi-asserted-by":"publisher","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S. (eds), Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October 1994, Springer, Lecture Notes in Computer Science, vol. 999, pp. 1\u201320 (1995). https:\/\/doi.org\/10.1007\/3-540-60472-3_1","DOI":"10.1007\/3-540-60472-3_1"},{"key":"307_CR5","doi-asserted-by":"publisher","unstructured":"Atzei, N., Bartoletti, M., Lande, S., Yoshida, N., Zunino, R.: Developing secure bitcoin contracts with BitML. In: Dumas, M., Pfahl, D., Apel, S., Russo, A. (eds), Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2019, Tallinn, Estonia, August 26-30, 2019, ACM, pp 1124\u20131128 (2019), https:\/\/doi.org\/10.1145\/3338906.3341173","DOI":"10.1145\/3338906.3341173"},{"key":"307_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752"},{"key":"307_CR7","doi-asserted-by":"publisher","unstructured":"Balland, E., Brauner, P., Kopetz, R., Moreau, P., Reilles, A.: Tom: Piggybacking rewriting on Java. In: Baader, F. (ed) Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26\u201328, 2007, Proceedings, Springer, Lecture Notes in Computer Science, vol. 4533, pp. 36\u201347 (2007).https:\/\/doi.org\/10.1007\/978-3-540-73449-9_5","DOI":"10.1007\/978-3-540-73449-9_5"},{"key":"307_CR8","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, vol. 131, 2nd edn. North Holland (2014)"},{"issue":"1","key":"307_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1142\/S0129054101000412","volume":"12","author":"P Borovansk\u00fd","year":"2001","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: a functional semantics. Int. J. Found. Comput. Sci. 12(1), 69\u201395 (2001). https:\/\/doi.org\/10.1142\/S0129054101000412","journal-title":"Int. J. Found. Comput. Sci."},{"key":"307_CR10","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds), CONCUR \u201997: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1243, pp. 135\u2013150 (1997). https:\/\/doi.org\/10.1007\/3-540-63141-0_10","DOI":"10.1007\/3-540-63141-0_10"},{"key":"307_CR11","doi-asserted-by":"publisher","unstructured":"Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. In: Bidoit, M., Dauchet, M. (eds), TAPSOFT\u201997: Theory and Practice of Software Development, 7th International Joint Conference CAAP\/FASE, Lille, France, April 14-18, 1997, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1214, pp. 67\u201392 (1997). https:\/\/doi.org\/10.1007\/BFb0030589","DOI":"10.1007\/BFb0030589"},{"key":"307_CR12","doi-asserted-by":"publisher","unstructured":"Bourdier, T., Cirstea, H., Dougherty, D.J., Kirchner, H.: Extensional and intensional strategies. In: Fern\u00e1ndez, M. (ed) Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009, Brasilia, Brazil, 28th June 2009, EPTCS, vol.\u00a015, pp. 1\u201319 (2009). https:\/\/doi.org\/10.4204\/EPTCS.15.1","DOI":"10.4204\/EPTCS.15.1"},{"key":"307_CR13","doi-asserted-by":"publisher","unstructured":"Braga, C., Verdejo, A.: Modular structural operational semantics with strategies. In: van Glabbeek, R., Mosses, P.D. (eds) Proceedings of the Third Workshop on Structural Operational Semantics, SOS 2006, Bonn, Germany, August 26, 2006, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 175(1), pp. 3\u201317 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.10.024","DOI":"10.1016\/j.entcs.2006.10.024"},{"issue":"1\u20132","key":"307_CR14","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.scico.2007.11.003","volume":"72","author":"M Bravenboer","year":"2008","unstructured":"Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego\/XT 0.17. A language and toolset for program transformation. Science of Computer Programming 72(1\u20132), 52\u201370 (2008). https:\/\/doi.org\/10.1016\/j.scico.2007.11.003","journal-title":"Science of Computer Programming"},{"key":"307_CR15","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed), Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, Springer, Lecture Notes in Computer Science, vol. 131, pp. 52\u201371 (1981). https:\/\/doi.org\/10.1007\/BFb0025774","DOI":"10.1007\/BFb0025774"},{"key":"307_CR16","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"307_CR17","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): : Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"307_CR18","doi-asserted-by":"publisher","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude...A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"307_CR19","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: (2020) Maude Manual v3.1. http:\/\/maude.lcc.uma.es\/maude31-manual-html\/maude-manual.html"},{"key":"307_CR20","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds), Tools and Algorithms for the Construction and Analysis of Systems, 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, Springer, Lecture Notes in Computer Science, vol. 9035, pp. 206\u2013211 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"307_CR21","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W.: On the Role of Scientific Thought, Springer, pp 60\u201366. Texts and Monographs in Computer Science (1982). https:\/\/doi.org\/10.1007\/978-1-4612-5695-3_12","DOI":"10.1007\/978-1-4612-5695-3_12"},{"key":"307_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlamp.2019.100497","volume":"110","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: Programming and symbolic computation in Maude. J. Logical Algebra. Methods Comput. Program. 110, 1\u201358 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100497","journal-title":"J. Logical Algebra. Methods Comput. Program."},{"key":"307_CR23","doi-asserted-by":"publisher","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds) Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19\u201321, 2002. Elsevier, Electronic Notes in Theoretical Computer Science, vol.\u00a071, pp. 162\u2013187 (2004). https:\/\/doi.org\/10.1016\/S1571-0661(05)82534-4","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"307_CR24","doi-asserted-by":"publisher","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. In: Archer, M., de\u00a0la Tour, T.B., Mu\u00f1oz, C. (eds) Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, August 16, 2006, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 174(11), pp. 3\u201325 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.03.017","DOI":"10.1016\/j.entcs.2006.03.017"},{"key":"307_CR25","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Pita, I., Rubio, R., Verdejo, A.: Strategy language for Maude (2021). https:\/\/maude.ucm.es\/strategies"},{"key":"307_CR26","doi-asserted-by":"publisher","unstructured":"Ene, N.C., Fern\u00e1ndez, M., Pinaud, B.: A strategic graph rewriting model of rational negligence in financial markets. In: Jaiani, G., Natroshvili, D. (eds), Applications of Mathematics and Informatics in Natural Sciences and Engineering, Springer, Springer Proceedings in Mathematics and Statistics, vol. 334, pp. 117\u2013134 (2020). https:\/\/doi.org\/10.1007\/978-3-030-56356-1_8","DOI":"10.1007\/978-3-030-56356-1_8"},{"key":"307_CR27","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M., Varga, J.: Finding candidate keys and 3nf via strategic port graph rewriting. In: PPDP \u201920: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9\u201310 September, 2020, ACM, pp. 10:1\u201310:14 (2020). https:\/\/doi.org\/10.1145\/3414080.3414090","DOI":"10.1145\/3414080.3414090"},{"key":"307_CR28","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/j.jlamp.2017.12.005","volume":"96","author":"M Fern\u00e1ndez","year":"2018","unstructured":"Fern\u00e1ndez, M., Kirchner, H., Pinaud, B., Vallet, J.: Labelled graph strategic rewriting for social networks. J. Log. Algebra. Methods Program. 96, 12\u201340 (2018). https:\/\/doi.org\/10.1016\/j.jlamp.2017.12.005","journal-title":"J. Log. Algebra. Methods Program."},{"issue":"5","key":"307_CR29","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1017\/S0960129518000270","volume":"29","author":"M Fern\u00e1ndez","year":"2019","unstructured":"Fern\u00e1ndez, M., Kirchner, H., Pinaud, B.: Strategic port graph rewriting: an interactive modelling framework. Math. Struct. Comput. Sci. 29(5), 615\u2013662 (2019). https:\/\/doi.org\/10.1017\/S0960129518000270","journal-title":"Math. Struct. Comput. Sci."},{"key":"307_CR30","doi-asserted-by":"publisher","unstructured":"Finkel, O.: Ambiguity of omega-languages of Turing machines. Logical Methods in Computer Science 10(3), (2014). https:\/\/doi.org\/10.2168\/LMCS-10(3:12)2014","DOI":"10.2168\/LMCS-10(3:12)2014"},{"key":"307_CR31","doi-asserted-by":"publisher","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds), Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, Springer, Lecture Notes in Computer Science, vol. 2102, pp. 53\u201365 (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_6","DOI":"10.1007\/3-540-44585-4_6"},{"key":"307_CR32","doi-asserted-by":"publisher","unstructured":"Hidalgo-Herrero, M., Verdejo, A., Ortega-Mall\u00e9n, Y.: Using Maude and its strategies for defining a framework for analyzing Eden semantics. In: Antoy, S. (ed), Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2006, Seattle, WA, USA, August 11, 2006, Elsevier, Electronic Notes in Theoretical Computer Science, vo. 174(10), pp. 119\u2013137 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.02.051","DOI":"10.1016\/j.entcs.2007.02.051"},{"key":"307_CR33","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, London (1985)"},{"key":"307_CR34","unstructured":"Holzmann, G., et\u00a0al.: Spin - Formal verification (2021). https:\/\/spinroot.com"},{"key":"307_CR35","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: Gr\u00e9goire, J.C., Holzmann, G.J., Peled, D.A. (eds), The Spin Verification System, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, August, 1996, DIMACS\/AMS, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a032, pp. 23\u201331 (1997). https:\/\/doi.org\/10.1090\/dimacs\/032\/03","DOI":"10.1090\/dimacs\/032\/03"},{"key":"307_CR36","unstructured":"Kirchner, C., Kirchner, F., Kirchner, H.:) Strategic computation and deduction. In: Benzm\u00fcller, C., Brown, C.E., Siekmann, J., Statman, R. (eds), Reasoning in Simple Type Theory. Festchrift in Honour of Peter B. Andrews on His 70th Birthday, Studies in Logic and the Foundations of Mathematics, vol.\u00a017, College Publications, pp. 339\u2013364 (2008). https:\/\/hal.inria.fr\/inria-00433745"},{"issue":"7","key":"307_CR37","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1145\/359131.359136","volume":"22","author":"RA Kowalski","year":"1979","unstructured":"Kowalski, R.A.: Algorithm = logic + control. Commun. ACM 22(7), 424\u2013436 (1979). https:\/\/doi.org\/10.1145\/359131.359136","journal-title":"Commun. ACM"},{"key":"307_CR38","doi-asserted-by":"publisher","unstructured":"Lamport, L.: \u201cSometime\u201d is sometimes \u201cnot never\u201d - on the temporal logic of programs. In: Abrahams, P.W., Lipton, R.J., Bourne, S.R. (eds), Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980, ACM Press, pp. 174\u2013185 (1980). https:\/\/doi.org\/10.1145\/567446.567463","DOI":"10.1145\/567446.567463"},{"key":"307_CR39","doi-asserted-by":"publisher","unstructured":"Lescanne, P.: Implementations of completion by transition rules + control: ORME. In: Kirchner, H., Wechler, W. (eds). Algebraic and Logic Programming, Second International Conference, Nancy, France, October 1-3, 1990, Proceedings, Springer, Lecture Notes in Computer Science, vol. 463, pp. 262\u2013269 (1990). https:\/\/doi.org\/10.1007\/3-540-53162-9_44","DOI":"10.1007\/3-540-53162-9_44"},{"key":"307_CR40","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Tollk\u00f6tter, A.: Transformation between regular expressions and $$\\omega$$-automata. In: Faliszewski, P., Muscholl, A., Niedermeier, R. (eds), 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016 - Krak\u00f3w, Poland, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, LIPIcs, vol.\u00a058, pp. 88:1\u201388:13 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2016.88","DOI":"10.4230\/LIPIcs.MFCS.2016.88"},{"issue":"1\u20132","key":"307_CR41","doi-asserted-by":"publisher","first-page":"151","DOI":"10.3166\/jancl.16.151-168","volume":"16","author":"M Marin","year":"2006","unstructured":"Marin, M., Kutsia, T.: Foundations of the rule-based system $$\\rho$$log. J. Appl. Non Class Logics 16(1\u20132), 151\u2013168 (2006). https:\/\/doi.org\/10.3166\/jancl.16.151-168","journal-title":"J. Appl. Non Class Logics"},{"key":"307_CR42","doi-asserted-by":"publisher","unstructured":"Marin, M., Kutsia, T., Dundua, B.: A rule-based approach to the decidability of safety of abac$$\\alpha$$. In: Kerschbaum, F., Mashatan, A., Niu, J., Lee, A.J. (eds), Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019, Toronto, ON, Canada, June 03\u201306, 2019, ACM, pp. 173\u2013178 (2019). https:\/\/doi.org\/10.1145\/3322431.3325416, https:\/\/dl.acm.org\/citation.cfm?id=3322431","DOI":"10.1145\/3322431.3325416"},{"key":"307_CR43","doi-asserted-by":"publisher","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. In: Mart\u00ed-Oliet, N. (ed), Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 117, pp. 417\u2013441 (2004). https:\/\/doi.org\/10.1016\/j.entcs.2004.06.020","DOI":"10.1016\/j.entcs.2004.06.020"},{"key":"307_CR44","doi-asserted-by":"publisher","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for Maude strategies. In: Ro\u015fu, G. (ed.), Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29\u201330, 2008, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 238(3), pp. 227\u2013247 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.05.022","DOI":"10.1016\/j.entcs.2009.05.022"},{"issue":"1","key":"307_CR45","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. Theor. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theor. Comput. Sci."},{"issue":"7\u20138","key":"307_CR46","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log Algebr. Program. 81(7\u20138), 721\u2013781 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2012.06.003","journal-title":"J. Log Algebr. Program."},{"issue":"4","key":"307_CR47","doi-asserted-by":"publisher","first-page":"34:1","DOI":"10.1145\/2631917","volume":"15","author":"F Mogavero","year":"2014","unstructured":"Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1-34:47 (2014). https:\/\/doi.org\/10.1145\/2631917","journal-title":"ACM Trans. Comput. Log."},{"issue":"6","key":"307_CR48","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"J. ACM"},{"key":"307_CR49","unstructured":"Pearl, J.: Heuristics. Addison-Wesley series in artificial intelligence, Addison-Wesley (1984)"},{"key":"307_CR50","doi-asserted-by":"publisher","DOI":"10.1016\/S0079-8169(04)80002-3","volume-title":"Infinite words, Pure and Applied Mathematics Series","author":"D Perrin","year":"2004","unstructured":"Perrin, D., Pin, J.E.: Infinite words, Pure and Applied Mathematics Series, vol. 141. Elsevier Morgan Kaufmann, Burlington (2004). https:\/\/doi.org\/10.1016\/S0079-8169(04)80002-3"},{"key":"307_CR51","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, IEEE Computer Society, pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"307_CR52","doi-asserted-by":"publisher","unstructured":"Rosa-Velardo, F., Segura, C., Verdejo, A.: Typed mobile ambients in Maude. In: Cirstea, H., Mart\u00ed-Oliet, N. (eds), Proceedings of the 6th International Workshop on Rule-Based Programming, RULE 2005, Nara, Japan, April 23, 2005, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 147(1), pp. 135\u2013161 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.06.041","DOI":"10.1016\/j.entcs.2005.06.041"},{"key":"307_CR53","unstructured":"Rubio, R.: Unified Maude model-checking tool (umaudemc) (2020). https:\/\/github.com\/fadoss\/umaudemc"},{"key":"307_CR54","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled rewriting systems. In: Geuvers, H. (ed.), 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, LIPIcs, vol. 131, pp. 34:1\u201334:18 (2019a). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.31","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"307_CR55","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Parameterized strategies specification in Maude. In: Fiadeiro, J., \u0162u\u0163u, I. (eds.), Recent Trends in Algebraic Development Techniques, Springer, Lecture Notes in Computer Science, vol. 11563, pp. 27\u201344 (2019b). https:\/\/doi.org\/10.1007\/978-3-030-23220-7_2","DOI":"10.1007\/978-3-030-23220-7_2"},{"key":"307_CR56","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Metalevel transformation of strategies. J. Logical Algebra. Methods Comput. Program. 124, pp. 1\u201321 (2021a). https:\/\/doi.org\/10.1016\/j.jlamp.2021.100728","DOI":"10.1016\/j.jlamp.2021.100728"},{"key":"307_CR57","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Simulating and model checking membrane systems using strategies in Maude. J. Logical Algebra. Methods Comput. Program. 124, pp. 1\u201325 (2021b). https:\/\/doi.org\/10.1016\/j.jlamp.2021.100727","DOI":"10.1016\/j.jlamp.2021.100727"},{"key":"307_CR58","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. Logical Algebra. Methods Comput. Program. 123, pp. 1\u201328 (2021c). https:\/\/doi.org\/10.1016\/j.jlamp.2021.100700","DOI":"10.1016\/j.jlamp.2021.100700"},{"key":"307_CR59","doi-asserted-by":"publisher","unstructured":"Santos-Garc\u00eda, G., Palomino, M.: Solving Sudoku puzzles with rewriting rules. In: Denker, G., Talcott, C. (eds.), Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 176, pp. 79\u201393 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.06.009","DOI":"10.1016\/j.entcs.2007.06.009"},{"key":"307_CR60","doi-asserted-by":"publisher","unstructured":"Santos-Garc\u00eda, G., Palomino, M., Verdejo, A.: Rewriting logic using strategies for neural networks: An implementation in Maude. In: Corchado, J.M., Rodr\u00edguez, S., Llinas, J., Molina, J.M. (eds.), International Symposium on Distributed Computing and Artificial Intelligence, DCAI 2008, University of Salamanca, Spain, 22th-24th October 2008, Springer, Advances in Soft Computing, vol.\u00a050, pp. 424\u2013433 (2009). https:\/\/doi.org\/10.1007\/978-3-540-85863-8_50","DOI":"10.1007\/978-3-540-85863-8_50"},{"key":"307_CR61","doi-asserted-by":"publisher","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.), Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1855, pp. 248\u2013263 (2000). https:\/\/doi.org\/10.1007\/10722167_21","DOI":"10.1007\/10722167_21"},{"key":"307_CR62","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-59126-6_6","volume-title":"Handbook of Formal Languages","author":"L Staiger","year":"1997","unstructured":"Staiger, L.: $$\\omega$$-languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, 339th edn., p. 387. Springer, Berlin (1997). https:\/\/doi.org\/10.1007\/978-3-642-59126-6_6","edition":"339"},{"key":"307_CR63","unstructured":"Straffin, P.D.: Game Theory and Strategy, Anneli Lax New Mathematical Library, vol.\u00a036. American Mathematical Society (1993)"},{"key":"307_CR64","volume-title":"Modern operating systems","author":"AS Tanenbaum","year":"2018","unstructured":"Tanenbaum, A.S., Bos, H.: Modern operating systems, 4th edn. Pearson, New York (2018)","edition":"4"},{"issue":"2","key":"307_CR65","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972). https:\/\/doi.org\/10.1137\/0201010","journal-title":"SIAM J. Comput."},{"key":"307_CR66","unstructured":"Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"307_CR67","doi-asserted-by":"publisher","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Basic completion strategies as another application of the Maude strategy language. In: Escobar, S. (ed.), Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2011, Novi Sad, Serbia, 29 May 2011, EPTCS, vol.\u00a082, pp. 17\u201336 (2011). https:\/\/doi.org\/10.4204\/EPTCS.82.2","DOI":"10.4204\/EPTCS.82.2"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-021-00307-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10515-021-00307-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-021-00307-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T15:34:32Z","timestamp":1650900872000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10515-021-00307-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,8]]},"references-count":67,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["307"],"URL":"https:\/\/doi.org\/10.1007\/s10515-021-00307-9","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,8]]},"assertion":[{"value":"8 February 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 November 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that there is no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}],"article-number":"7"}}