RT Journal Article
T1 Strategies, model checking and branching-time properties in Maude
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 a natural and expressive framework for the specification of concurrent systems and logics. Its nondeterministic local transformations are described by rewriting rules, which can be controlled at a higher level using a builtin strategy language added to Maude 3. This specification resource would not be of much interest without tools to analyze their models, so in a previous work, we extended the Maude LTL model checker to verify strategy-controlled systems.In this paper, CTL* and μ-calculus are added to the repertoire of supported logics, after discussing which adaptations are needed for branching-time properties. The new extension relies on some external model checkers that are exposed the Maude models through general and efficient connections, profitable for future extensions and further applications. The performance of these model checkers is compared.
PB Elsevier
SN 2352-2208
YR 2021
FD 2021-06-24
LK https://hdl.handle.net/20.500.14352/91463
UL https://hdl.handle.net/20.500.14352/91463
LA eng
NO Agencia Estatal de Investigación
NO Ministerio de Ciencia, Innovación y Universidades
DS Docta Complutense
RD 12 abr 2025