2026-06-29T07:51:17Zhttps://docta.ucm.es/rest/oai/requestoai:docta.ucm.es:20.500.14352/872182023-08-26T04:35:24Zcom_20.500.14352_14col_20.500.14352_15
Docta Complutense
author
Verdejo López, José Alberto
author
Eker, Steven
author
Martí Oliet, Narciso
author
Meseguer, José
author
Rubio Cuéllar, Rubén Rafael
2023-07-10T11:46:04Z
2023-07-10T11:46:04Z
2023-06-06
2352-2208
10.1016/j.jlamp.2023.100887
https://hdl.handle.net/20.500.14352/87218
2352-2216
Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-deterministic local transformations on the state. Sometimes a controlled application of these rules is required to reduce non-determinism, to capture global, goal-oriented or efficiency concerns, or to select specific executions for their analysis. That is what we call a strategy. In order to express them, respecting the separation of concerns principle, a Maude strategy language was proposed and developed. The first implementation of the strategy language was done in Maude itself using its reflective features. After ample experimentation, some more features have been added and, for greater efficiency, the strategy language has been implemented in C++ as an integral part of the Maude system. This paper describes the Maude strategy language along with its semantics, its implementation decisions, and several application examples from various fields.
eng
Attribution-NonCommercial-NoDerivatives 4.0 International
The Maude strategy language
journal article
UGFyYSBxdWUgZWwgcmVwb3NpdG9yaW8gaW5zdGl0dWNpb25hbCBkZSBsYSBVbml2ZXJzaWRhZCBkZSBNYWRyaWQgcHVlZGEgYWxtYWNlbmFyIHkgZGlzdHJpYnVpciBlbCBvYmpldG8gZGlnaXRhbCBkZXBvc2l0YWRvLCBlcyBuZWNlc2FyaW8gcXVlIGxhIHBlcnNvbmEgcXVlIGhhZ2EgZWwgZGVww7NzaXRvIGxlYSB5IGFjZXB0ZSBsYXMgY29uZGljaW9uZXMgZXN0YWJsZWNpZGFzIGVuIGVzdGEgbGljZW5jaWE6CuKAoiBBY2VwdGFuZG8gZXN0YSBsaWNlbmNpYSwgdXN0ZWQgY29tbyBhdXRvci9yZXMgeS9vIHByb3BpZXRhcmlvL3MgZGUgbG9zIGRlcmVjaG9zIGRlIHByb3BpZWRhZCBpbnRlbGVjdHVhbCwgb3RvcmdhIGFsIHJlcG9zaXRvcmlvIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCBlbCBkZXJlY2hvIG5vIGV4Y2x1c2l2byBkZSByZXByb2R1Y2Npw7NuIHkgZGlzdHJpYnVjacOzbiBkZSBzdSBvYnJhIGVuIGN1YWxxdWllciBmb3JtYXRvIHkgbWVkaW8uCuKAoiBFbCBkZXBvc2l0YW50ZSwgZW4gY2FzbyBkZSB1bmEgb2JyYSBjb24gbcOhcyBkZSB1biBhdXRvciwgZ2FyYW50aXphIHF1ZSBsbyBoYWNlIHJlc3BvbnNhYmxlbWVudGUgZW4gbm9tYnJlIHkgY29uIGNvbnNlbnRpbWllbnRvIGRlIGxvcyBkZW3DoXMgYXV0b3Jlcy4K4oCiIEFjZXB0YSBxdWUgZWwgcmVwb3NpdG9yaW8gZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIHB1ZWRhIGNvbnNlcnZhciBtw6FzIGRlIHVuYSBjb3BpYSBkZSBlc3RlIGRvY3VtZW50byB5LCBzaW4gYWx0ZXJhciBzdSBjb250ZW5pZG8sIGNvbnZlcnRpcmxvIGEgY3VhbHF1aWVyIGZvcm1hdG8gZGUgZmljaGVybywgbWVkaW8gbyBzb3BvcnRlLCBwYXJhIHByb3DDs3NpdG9zIGRlIHNlZ3VyaWRhZCB5IHByZXNlcnZhY2nDs24uCuKAoiBEZWNsYXJhIHF1ZSBlbCBkb2N1bWVudG8gZXMgdW4gdHJhYmFqbyBvcmlnaW5hbCBzdXlvIHkgcXVlIGN1ZW50YSBjb24gbGEgcG9zdGVzdGFkIHBhcmEgb3RvcmdhciBsb3MgZGVyZWNob3MgY29udGVuaWRvcyBlbiBlc3RhIGxpY2VuY2lhLiBUYW1iacOpbiBkZWNsYXJhIHF1ZSBzdSBkb2N1bWVudG8gbm8gaW5mcmluZ2UgbG8gZXN0YWJsZWNpZG8gZW4gbGEgdmlnZW50ZSBsZWdpc2xhY2nDs24gZGUgcHJvcGllZGFkIGludGVsZWN0dWFsLgrigKIgU2kgZWwgZG9jdW1lbnRvIGNvbnRpZW5lIG1hdGVyaWFsZXMgZGUgbG9zIGN1YWxlcyBubyB0aWVuZSBsb3MgZGVyZWNob3MgZGUgYXV0b3IsIGRlY2xhcmEgcXVlIGhhIG9idGVuaWRvIGVsIHBlcm1pc28gc2luIHJlc3RyaWNjacOzbiBkZWwgcHJvcGlldGFyaW8gcGFyYSBvdG9yZ2FyIGEgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIGxvcyBkZXJlY2hvcyByZXF1ZXJpZG9zIHBvciBlc3RhIGxpY2VuY2lhLCB5IHF1ZSBlc2UgbWF0ZXJpYWwsIGN1eW9zIGRlcmVjaG9zIHNvbiBkZSB0ZXJjZXJvcywgZXN0w6EgY2xhcmFtZW50ZSBpZGVudGlmaWNhZG8geSByZWNvbm9jaWRvIGRlbnRybyBkZWwgY2NvbnRlbmlkbyBkZWwgZG9jdW1lbnRvLgrigKIgU2kgZWwgZG9jdW1lbnRvIHNlIGJhc2EgZW4gdW5hIG9icmEgcXVlIGhhIHNpZG8gcGF0cm9jaW5hZGEgbyBhcG95YWRhIHBvciB1bmEgYWdlbmNpYSB1IG9yZ2FuaXphY2nDs24gZGlmZXJlbnRlIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCwgdXN0ZWQgZGVjbGFyYSBxdWUgaGEgY3VtcGxpZG8gY29uIGxhcyBvYmxpZ2FjaW9uZXMgcmVxdWVyaWRhcyBwb3IgZXN0ZSBjb250cmF0byBvIGFjdWVyZG8uCuKAoiBMYSBVbml2ZXJzaWRhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQgaWRlbnRpZmljYXLDoSBjbGFyYW1lbnRlIHN1L3Mgbm9tYnJlL3MgY29tbyBlbC9sb3MgYXV0b3IvZXMgbyBwcm9waWV0YXJpby9zIGRlIGxvcyBkZXJlY2hvcyBkZWwgZG9jdW1lbnRvLCB5IG5vIGhhcsOhIG5pbmd1bmEgYWx0ZXJhY2nDs24gZGUgc3UgZG9jdW1lbnRvIGRpZmVyZW50ZSBhIGxhcyBwZXJtaXRpZGFzIGVuIGVzdGEgbGljZW5jaWEuCuKAoiBUcmFiYWpvcyBkZXBvc2l0YWRvcyBwb3Igc3UgcHJvcGlvIGF1dG9yOiBhbCBhdXRvLWFyY2hpdmFyIGVzdGEgY29sZWNjacOzbiBkZSBmaWNoZXJvcyB5IG1ldGFkYXRvcyBiaWJsaW9ncsOhZmljb3MgYXNvY2lhZG9zLCBvdHJvZ28sIGFsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkIGVsIGRlcmVjaG8gcGFyYSBhbG1hY2VuYXJsb3MgeSBkaXN0cmlidWlybG9zLiBEZWNsYXJvIHF1ZSBlc3RlIG1hdGVyaWFsIGVzIGRlIG1pIHByb3BpZWRhZCBpbnRlbGVjdHVhbCB5IHF1ZSBlbCByZXBvc2l0b3JpbyBpbnN0aXR1dGljaW9uYWwgZGUgbGEgVW5pdmVyc2lkYWQgQ29tcGx1dGVuc2UgZGUgTWFkcmlkLCBubyBhc3VtZSByZXNwb25zYWJpbGlkYWQgYWxndW5hIGVuIGNhc28gZGUgcXVlIHNlIHByb2R1emNhIHVuYSB2aW9sYWNpw7NuIGRlIGRlcmVjaG9zIGRlIHByb3BpZWRhZCBhbCBkaXN0cmlidWlyIGVzdG9zIGZpY2hlcm9zIG8gbWV0YWRhdG9zLgrigKIgVHJhYmFqb3MgZGVzcG9zaXRhZG9zIHBvciBvdHJvcyBxdWUgbm8gc2VhbiBzdSBhdXRvcjpkZWNsYXJvIHF1ZSBsb3MgbWV0YWRhdG9zIGJpYmxpb2dyw6FmaWNvcyBxdWUgZXN0b3kgYXJjaGl2YW5kbyBlbiBlbCByZXBvc3RvcmlvIGluc3RpdHVjaW9uYWwgZGUgbGEgVW5pdmVyc2lhZCBDb21wbHV0ZW5zZSBkZSBNYWRyaWQsIHNvbiBkZSBkb21pbmlvIHDDumJsaWNvLiBTaSBubyBmdWVzZSBlbCBjYXNvLCBhY2VwdG8gcGxlbmEgcmVzcG9uc2FiaWxpZGFkIHBvciBjdWFscXVpZXIgaW5mcmFjY2nDs24gZGUgZGVyZWNob3MgZGUgYXR1b3IgcXVlIGNvbmxsZXZlIGxhIGRpc3RyaWJ1Y2nDs24gZGUgZXN0b3MgZmljaGVyb3MgbyBtZXRhZGF0b3MuCuKAoiBQb3IgdGFudG8sIHRvZG9zIGxvcyBtZXRhZGF0b3MgcHVibGljYWRvcyBlbiBlbCByZXBvc2l0b3JpbyBpbnN0aXR1Y2lvbmFsIGRlIGxhIFVuaXZlcnNpZGFkIENvbXBsdXRlbnNlIGRlIE1hZHJpZCwgZXN0w6FuIGRpc3BvbmlibGVzIGNvbiBsYSBsaWNlbmNpYSBDcmVhdGl2ZSBDb21tb25zIENDMCAxLjAgVW5pdmVyc2FsIE9mcmVjaW1pZW50byBhbCBEb21pbmlvIFDDumJsaWNvIChDQzAgMS4wKS4gRXN0YSBsaWNlbmNpYSBwZXJtaXRlIGNvcGlhciwgbW9kaWZpY2FyLCBkaXN0cmlidWlyLCByZXV0aWxpemFyIHkgY29tcGFydGlyIHDDumJsaWNhIHkgbGlicmVtZW50ZSBsb3MgbWV0YWRhdG9zIChpbmNsdXllbmRvIHN1IHVzbyBjb21lcmNpYWwpLCBzaW4gdGVuZXIgcXVlIHBlZGlyIHBlcm1pc28uIFNpIHRlcmNlcmFzIHBhcnRlcyB1c2FuIGVzdG9zIG1ldGFkYXRvcywgZGViZW4gaGFjZXIgdW4gcmVjb25vY2ltaWVudG8geSB1bmEgYXRyaWJ1Y2Npw7NuIGEgbGFzIGZ1ZW50ZXMgZGUgbG9zIG1pc21vcy4gTGEgcmV1dGlsaXphY2nDs24gZGUgZXN0b3MgbWV0YWRhdG9zIHRhbWJpw6luIGVzIGxpYnJlLCB0YWwgeSBjb21vIGVzdGFibGVjZSBsYSBsaWNlbmNpYSBkZSB1c28gQ0MwLgo=
URL
https://docta.ucm.es/bitstreams/035d21c8-d9ce-4ef2-bdf5-863e71d37b5f/download
File
MD5
04c23820030505909d9f63bd52814e0b
1003365
application/pdf
1-s2.0-S235222082300041X-main.pdf