RT Conference Proceedings
T1 Specifying fairness constraints and model checking with non-intensional strategies
A1 Rubio Cuéllar, Rubén Rafael
A1 Martí Oliet, Narciso
A1 Pita Andreu, María Isabel
A1 Verdejo López, José Alberto
A2 Ogata, Kazuhiro
A2 Martí Oliet, Narciso
AB 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.
YR 2024
FD 2024-08-02
LK https://hdl.handle.net/20.500.14352/122895
UL https://hdl.handle.net/20.500.14352/122895
LA eng
NO Agencia Estatal de Investigación
DS Docta Complutense
RD 30 mar 2026