2026-06-28T20:40:54Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/1228952025-07-31T00:00:24Zcom_20.500.14352_14col_20.500.14352_15

00925njm 22002777a 4500 dc Rubio Cuéllar, Rubén Rafael author Martí Oliet, Narciso author Pita Andreu, María Isabel author Verdejo López, José Alberto author 2024-08-02 Strategies 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. 10.1007/978-3-031-65941-6_8 https://hdl.handle.net/20.500.14352/122895 Specifying fairness constraints and model checking with non-intensional strategies