RT Journal Article
T1 Model checking strategy-controlled systems in rewriting logic
A1 Rubio Cuéllar, Rubén Rafael
A1 Martí Oliet, Narciso
A1 Pita Andreu, María Isabel
A1 Verdejo López, José Alberto
AB Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive.In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared.
PB Springer
SN 0928-8910
SN 1573-7535
YR 2021
FD 2021-12-08
LK https://hdl.handle.net/20.500.14352/91464
UL https://hdl.handle.net/20.500.14352/91464
LA eng
NO Agencia Estatal de Investigación
NO Ministerio de Ciencia, Innovación y Universidades
DS Docta Complutense
RD 27 abr 2025