Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Maude strategy language

Steven Eker, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Alberto Verdejo

TL;DR

The Maude strategy language addresses the challenge of controlling nondeterminism in rewriting logic specifications by introducing a distinct, object-level strategy language that separates rule definitions from control flow. It provides formal semantics (denotational and rewriting-based) and a high-performance C++ implementation, including strategy modules, parameterization, and metalevel reflection. The approach is demonstrated across diverse domains (e.g., 15-puzzle, RIP protocol, Knuth–Bendix completion) to illustrate modular, goal-directed, and efficient strategy-driven reasoning. This work advances practical verification, analysis, and executable modeling with reusable, strategy-driven control constructs embedded in Maude’s rewriting framework.

Abstract

Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-deterministic local transformations on the state. Sometimes a controlled application of these rules is required to reduce non-determinism, to capture global, goal-oriented or efficiency concerns, or to select specific executions for their analysis. That is what we call a strategy. In order to express them, respecting the separation of concerns principle, a Maude strategy language was proposed and developed. The first implementation of the strategy language was done in Maude itself using its reflective features. After ample experimentation, some more features have been added and, for greater efficiency, the strategy language has been implemented in C++ as an integral part of the Maude system. This paper describes the Maude strategy language along with its semantics, its implementation decisions, and several application examples from various fields.

The Maude strategy language

TL;DR

The Maude strategy language addresses the challenge of controlling nondeterminism in rewriting logic specifications by introducing a distinct, object-level strategy language that separates rule definitions from control flow. It provides formal semantics (denotational and rewriting-based) and a high-performance C++ implementation, including strategy modules, parameterization, and metalevel reflection. The approach is demonstrated across diverse domains (e.g., 15-puzzle, RIP protocol, Knuth–Bendix completion) to illustrate modular, goal-directed, and efficient strategy-driven reasoning. This work advances practical verification, analysis, and executable modeling with reusable, strategy-driven control constructs embedded in Maude’s rewriting framework.

Abstract

Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-deterministic local transformations on the state. Sometimes a controlled application of these rules is required to reduce non-determinism, to capture global, goal-oriented or efficiency concerns, or to select specific executions for their analysis. That is what we call a strategy. In order to express them, respecting the separation of concerns principle, a Maude strategy language was proposed and developed. The first implementation of the strategy language was done in Maude itself using its reflective features. After ample experimentation, some more features have been added and, for greater efficiency, the strategy language has been implemented in C++ as an integral part of the Maude system. This paper describes the Maude strategy language along with its semantics, its implementation decisions, and several application examples from various fields.
Paper Structure (13 sections, 3 equations, 2 figures)

This paper contains 13 sections, 3 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Rewriting logic and Maude
  3. Abstract reduction
  4. Membership equational logic
  5. Rewriting logic
  6. Maude
  7. Strategies
  8. The Maude strategy language
  9. Idle and fail
  10. Rule application
  11. Tests
  12. Regular expressions
  13. Conditional and derived operators

Figures (2)

  • Figure 1: The 15-puzzle in its goal position and in a shuffled one.
  • Figure 2: Schema for the operators of the regular expressions sublanguage.