Invariant-Driven Strategies for Maude

We propose generic invariant-driven strategies that control the execution of systems by guaranteeing that the given invariants are satisfied. Our strategies are generic in the sense that they are parameterized by the system whose execution they control, by the logic in which the invariants are expressed, and by the invariants themselves. We illustrate the use of the strategies in the case of invariants expressed in propositional logic. However, the good properties of Maude as a logical and semantic framework, in which many different logics and formalisms can be expressed and executed allow us to use other logics as parameter of our strategies.