Rubio Cuéllar, Rubén RafaelMartí Oliet, NarcisoPita Andreu, María IsabelVerdejo López, José AlbertoOgata, KazuhiroMartí Oliet, Narciso2025-07-302025-07-302024-08-0210.1007/978-3-031-65941-6_8https://hdl.handle.net/20.500.14352/122895Strategies are a natural way of specifying constraints in a rewriting-based model. They are often expressed as executable programs in some strategy language that intensionally filter the possible next rewrites. Hence, they cannot capture restrictions of the model involving unbounded delays, like fairness, which are useful in many verification scenarios. In this paper, we propose a variation to the semantics of the Maude strategy language that allows expressing non-intensional strategies without recursion, in a way amenable for verification. Then we present an LTL model checker for this kind of strategies and discuss the corresponding problem for other logics.engAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/conference paperembargoed accessRewriting strategiesModel checkingFairnessKleene starLenguajes de programaciónLógica simbólica y matemática (Matemáticas)1203.23 Lenguajes de Programación1102.14 Lógica Simbólica