Strategies, Model Checking and Branching-Time Properties in Maude

Maude 3 includes as a new feature an object-level strategy language. Rewriting strategies can now be used to easily control how rules are applied, restricting the rewriting systems behavior. This new specification layer would not be useful if there were no tools to execute, analyze and verify its creatures. For that reason, we extended the Maude LTL model checker to systems controlled by strategies, after studying their model-checking problem. Now, we widen the range of properties that can be checked in Maude models, both strategy-aware and strategy-free, by implementing a module for the language-independent model checker LTSmin that supports logics like CTL* and \(\mu \)-calculus.