Strategies, model checking and branching-time properties in Maude | Publicación