RT Report
T1 Model checking strategy-controlled rewriting systems (extended version)
A1 Martí Oliet, Narciso
A1 Pita Andreu, María Isabel
A1 Verdejo López, José Alberto
A1 Rubio Cuéllar, Rubén Rafael
AB Strategies are widespread in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages, where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware LTL model checker for the Maude specification language, based on rewriting logic, and its strategy language.This extended version includes the proofs of the propositions in the conference paper, and a complete description of the small-step operational semantics used to define model checking for the Maude strategy language.
YR 2019
FD 2019-06-27
LK https://hdl.handle.net/20.500.14352/17476
UL https://hdl.handle.net/20.500.14352/17476
LA eng
NO Extended version of a paper presented at FSCD 2019 (DOI:  10.4230/LIPIcs.FSCD.2019.34).
NO Ministerio de Ciencia e Innovación (MICINN)
DS Docta Complutense
RD 5 abr 2025