Model Checking Strategy-Controlled Rewriting Systems (System Description)
Rubén Rubio, Narciso Martı́-Oliet, Isabel Pita, Alberto Verdejo · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2019
Strategies are widespread in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages, where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware LTL model checker for the Maude specification language, based on rewriting logic, and its strategy language.