2026-06-29T03:12:44Zhttps://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

Specifying fairness constraints and model checking with non-intensional strategies Rubio Cuéllar, Rubén Rafael Martí Oliet, Narciso Pita Andreu, María Isabel Verdejo López, José Alberto Ogata, Kazuhiro Martí Oliet, Narciso 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. 2025-07-30T09:52:48Z 2025-07-30T09:52:48Z 2024-08-02 conference paper 10.1007/978-3-031-65941-6_8 https://hdl.handle.net/20.500.14352/122895 eng info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/PID2019-108528RB-C22/ES/METODOS RIGUROSOS PARA EL DESARROLLO DE SISTEMAS SOFTWARE DE CALIDAD Y FIABILIDAD CERTIFICADAS/ http://creativecommons.org/licenses/by-nc-nd/4.0/ embargoed access Attribution-NonCommercial-NoDerivatives 4.0 International