We have developed a basic
strategy language for Maude, to be used *at the
object level*, rather than at the metalevel. The strategy language
allows the definition of strategy expressions that control the way a
term is rewritten.
Our design is based on a strict separation between the rewrite rules
in *system modules* and the strategy expressions, that are
specified in separate *strategy modules*. Thus, in our proposal
it is not possible to use strategy expressions in the rewrite rules of
a system module: they can only be specified in a separate strategy
module. In fact, this separation makes possible defining different
strategy modules to control in different ways the rewrites of a single
system module.

A strategy is described as an operation that, when applied to a given
term, produces a *set* of terms as a result, given that the process is
nondeterministic in general.
The basic strategies consist of the application of a rule (identified
by the corresponding rule label) to a given term, and allowing
variables in a rule to be instantiated before its application by means
of a substitution. For conditional rules (which may contain rewrite
conditions) such rewrite conditions can also be controlled by means
of strategies. Basic strategies are combined by means of several
combinators, including: regular expression constructions (concatenation,
union, and iteration), if-then-else, combinators to control the way
subterms of a given term are rewritten, and recursion.

The strategy language is fully available in Maude 3, which can be downloaded from the official page. Its manual is the most updated and complete reference of the language. An extended version including a strategy-aware model checker can also be downloaded from here.

We can see how to use the language with an example. The following system module defines a blackboard as a multiset of natural numbers, and a rule selecting two numbers in the blackboard and replacing them by their arithmetic mean.

modBLACKBOARDisprNAT .sortBlackboard .subsortNat < Blackboard .varsM N : Nat .op__ : Blackboard Blackboard -> Blackboard [assoc comm] .rl[play] : M N => (M + N) quo 2 .endm

With this module loaded we can already use the command for rewriting using a strategy.

Maude> srew 2 4 6 8 using play . srewrite in BLACKBOARD : 2 4 6 8 using play . Solution 1 result Blackboard: 3 6 8 Solution 2 result Blackboard: 4 4 8 Solution 3 result Blackboard: 4 5 6 Solution 4 result Blackboard: 2 5 8 Solution 5 result Blackboard: 2 6 6 Solution 6 result Blackboard: 2 4 7 No more solutions.

If we were not interested in all solutions, we can limit the number of answers:

Maude> srew [1] 2 4 6 8 using play . srewrite [1] in BLACKBOARD : 2 4 6 8 using play . Solution 1 result Blackboard: 3 6 8and then we could ask for more solutions

Maude> cont 1 . Solution 2 result Blackboard: 4 4 8

We can also introduce *strategy modules* where strategies can be defined.
The following module defines a strategy `minmin`

that
continuously applies the rewrite rule `play`

to the two
minimum values in the blackboard using some auxiliary operations:

And then the defined strategies can also be used in the strategy commands:smodBLACKBOARD-STRATisprotectingBLACKBOARD .stratminmin @ Blackboard .varsX Y M N : Nat .varB : Blackboard .sdminmin := (matchrew B s.t. X := minimum(B) /\ Y := minimum(remove(X,B)) by B using play[M <- X , N <- Y] ) ! .opminimum : Blackboard -> Nat .opremove : Nat Blackboard -> Blackboard .eqminimum(N) = N .eqminimum(N M) = if (N < M) then N else M fi .eqminimum(N M B) = if (N < M) then minimum(N B) else minimum(M B) fi .eqremove(X, X B) = B .eqremove(X, B) = B [owise] .endsm

Maude> srew 2000 20 2 200 10 50 using minmin . srewrite in BLACKBOARD-STRAT : 2000 20 2 200 10 50 using minmin . Solution 1 result NzNat: 1057 No more solutions.

In order to advance the
*semantic foundations* of the Maude strategy language, we have developed
a detailed *operational semantics* by rewriting to Maude's
strategy language. This is most fitting, since rewriting logic is a
general semantic framework in which strategies themselves should not
be thought of as extra-logical constructs, but should instead be
expressed *inside the logic*. This idea of giving an operational,
rewriting semantics to the strategy
language is achieved in this paper
by means of a theory transformation.

By taking advantage of the reflective properties of rewriting logic, which allow to consider
metalevel entities such as theories as usual data, the transformation
could be implemented as an operation from rewrite theories
to rewrite theories, specified itself in rewriting logic.
Instead of doing this, we have written a
*parameterized* module
that extends the metalevel with the rewriting semantics of the strategy language in
a generic and quite efficient way.

The Maude version that can be downloaded in this page includes a model checker capable of verifying systems controlled by the strategy language. To invoke the model checker, the user has to prepare the model and atomic propositions as if it were the standard model checker, but also define the relevant strategies in a strategy module. The `STRATEGY-MODEL-CHECKER`

module in `model-checker.maude`

includes the operator

```
```**op** modelCheck : State Formula Qid -> ModelCheckerResult [special (...)] .

that additionally receives a third argument for the name of the strategy that will control the model behavior.

Moreover, CTL* and μ-calculus properties can also be checked using the `umaudemc`

tool included in the release packages, which relies in several alternative backends like LTSmin, NuSMV, Spot, pyModelChecking and our own implementations. The syntax of the command is:

```
````umaudemc check <Maude file> <initial term> <formula> [<strategy>]`

Formulae are written as terms of the sort `Formula`

extended with additional operators for the new logics, as explained in the user manual. Any strategy expression can be passed to the strategy argument, and strategy-free models are also supported. The LTSmin integration requires a Maude language module included as `libmaudemc.so`

in the release packages. Since the current version of LTSmin does not support both edge and state labels in μ-calculus formulae, a modified version ready to use can be downloaded from the download section. The `umaudemc`

tool is also available on PyPI and can be installed with `pip install umaudemc`

.
Some examples and documentation are available:

*Model checking strategy-controlled rewriting systems*(FSCD 2019) and its extended version.*Strategies, model checking and branching-time properties in Maude*(JLAMP, special issue of WRLA 2020) and its related material.**NEW**- Complete semantics for the Maude strategy language.
- The model checker user manual.

`choice(w`

that randomly chooses of the strategies_{1}: α_{1}, ..., w_{n}: α_{n})`α`

according to the weights_{k}`w`

(of sort_{i}`Nat`

or`Float`

).`sample X := distrib(args) in α`

that samples the variable`X`

according to the distribution`distrib`

with arguments`args`

. The sort of`X`

and of the comma-separated arguments must be`Float`

. Available distributions are`bernouilli`

,`uniform`

,`norm`

,`gamma`

, and`exp`

.- An extension of the standard
`matchrew`

,`xmatchrew`

, and`amatchrew`

operators (see §10.1.2 of the Maude manual) that allows specifying a weight for each match and selects one of them at random obeying these weights. Their syntax is (/`x`

/`a`

)`matchrew P s.t. C with weight w by x`

, where_{1}using α_{1}, ..., x_{n}using α_{n}`w`

is a term (of sort`Nat`

or`Float`

) that may contain variables from the context and the matching substitution.

- the
`srewrite`

and`dsrewrite`

command in the version of the Maude interpreter distributed in this page, and the`Term.srewrite`

method in the`maude`

Python library. - the
`simaude`

command for performing Monte Carlo simulations included in the release packages. Its basic syntax is`simaude <Maude file> <initial term> <strategy> [-n <n>] [-j <n>] [-random-seed <n>]`

`-n`

determines the number of simulations,`-j`

the number of parallel jobs, and`-random-seed`

the initial random seed. - a simulator for the statistical model-checking tool MultiVeSta. A script
`mvmaude`

is included to facilitate its usage with syntax`mvmaude <Maude file> <initial term> <MultiQuaTEx query> [<strategy>]`

- the probabilistic model-checking command
`pcheck`

of`umaudemc`

. It allows calculating the probability of LTL, CTL, and PCTL formulae, expected values, and transient and steady-state probabilities.`umaudemc pcheck <Maude file> <initial term> <formula> <strategy> --assign strategy [--steps] [--reward <term>]`

- the statistical model-checking command
`scheck`

of`umaudemc`

. Like the MultiVeSta plugin, it allows evaluating QuaTEx expressions using Monte Carlo simulations for a given statistical confidence level.`umaudemc scheck <Maude file> <initial term> <QuaTEx file> <strategy> [--assign step|strategy|strategy-full] [...]`

`pcheck`

are also available with`scheck`

.

Here you can find some examples (and also here). Those using parameterization or the strategy-aware model checker are gathered together.

- Blackboard example
- Crossing the river
- Insertion sort
- CCS operational semantics
- Abstract congruence closure
- Completion procedures
- Telecommunication networks
- Towers of Hanoi
- 15-puzzle
- Logic programming with negation and cut

- Generic backtracking applied to the labyrinth, queens, and some graph problems.
- Simplex algorithm (examples and analysis of iterations)
- λ-calculus
- REC language
- Word wrap algorithm (sample texts)
- Flat map and fractals (drawing program)
- Generic Branch and bound with the travelling salesperson instance.

- Strategy language extension skeleton with congruence operators and generic traversals
- Context-sensitive rewriting
- Operational semantics of the strategy language with additional intersection and until operators.
- Specifying strategies by Turing machines.

- Mutual exclusion
- The philosophers problem.
- Semaphores and process scheduling policies.
- A cycle finder for the simplex algorithm.
- The river crossing and the bridge and torch puzzles.
- Train crossing
- RIP protocol
- Model checking for CCS
- Model checking for REC
- Membrane systems
- Operational semantics of the strategy language.
- Multistrategies
- Lamport's bakery
- Zune's lap year bug

Moreover, the language has been applied by different authors to various interesting examples. Their source code has been updated to the current language version.

- A parameterized operational semantics for the Eden language, by Mercedes Hidalgo-Herrero, Alberto Verdejo, and Yolanda Ortega-Mallén (code).
- Two semantics for Cardelli and Gordon's Ambient Calculus, by Fernando Rosa-Velardo, Clara Segura, and Alberto Verdejo (code).
- Proof calculus for membrane systems, by Oana Andrei and Dorel Lucanu (original code, new version).
- A Sudoku solver, by Gustavo Santos-García and Miguel Palomino (code).
- Neural networks, by Gustavo Santos-García, Miguel Palomino, and Alberto Verdejo (code, data).

More recent applications of the strategy language and its strategy-aware model checker are the following:

- Developing secure bitcoin contracts with BitML by Nicola Atzei, Massimo Bartoletti, Stefano Lande, Nabuko Yoshida, and Roberto Zunino (code).
- Strategies for implementing SAT algorithms in rewriting logic by Alejandro Hernández Cerezo, directed by Narciso Martí-Oliet and Alberto Verdejo (code).

*An overview of the Maude strategy language and its applications*(WRLA 2022)NEWAn informal and updated description of the Maude strategy language and its applications, based on an invited tutorial given at WRLA 2022.

See also: View-only link

*Model checking of strategy-controlled systems in rewriting logic*(PhD thesis)This dissertation covers in depth the Maude strategy language and its probabilistic extension, as well as the problem that gives it its title.

See also: Material

*Model checking strategy-controlled systems in rewriting logic*(AUSE)A detailed discussion of the Maude LTL model checker for strategy-controlled systems, its theoretical foundations, and several examples.

See also: View-only link · Material

*Simulating and model checking membrane systems using strategies in Maude*(JLAMP, WPTE 2020)An application of the strategy language and its model checker to build an interactive environment for membrane systems.

See also: Conference version · Maude files

*Metalevel transformation of strategies*(JLAMP, WPTE 2020)Examples of reflective transformation and generation of strategies, including some language extensions.

See also: Conference version · Maude files

*Strategies, model checking and branching-time properties in Maude*(JLAMP, WRLA 2020)An extension of the model checker for strategy-controlled systems to branching-time logics (special issue of WRLA 2020).

See also: Conference version · Material

*Programming and symbolic computation in Maude*(JLAMP)A presentation of several new features of Maude 3 including a section on the strategy language.

See also: arXiV preprint

*Model checking strategy-controlled rewriting systems*(FSCD 2019)A presentation of the Maude LTL model checker for strategy-controlled systems and its fundamentals.

See also: Extended version

*Parameterized strategies specification in Maude*(WADT 2018)A presentation of the strategy parameterization features in the current version of the language, illustrated by various examples.

See also: Open archive · Maude files

*A rewriting semantics for Maude strategies*(WRLA 2008)An operational semantics for the strategy language by means of a theory transformation, as described above.

*Deduction, strategies and rewriting*(Strategies 2006)An almost up-to-date description of the language and its implementation, with more examples related to automatic deduction.

*Towards a strategy language for Maude*(WRLA 2004)The initial proposal of the language, together with some examples. The

*search syntax*and related features are not included in the current language design.

While the strategy language is completely implemented in Maude 3, the extension including the model checker for strategy-controlled systems can be downloaded from the following links:

The initial prototype of the strategy language (updated January 12 2021) is also available. It is implemented on top of Full Maude, and lacks strategy module importation and parameterization support. For model checking branching-time properties, some external tools from the projects LTSmin and mCRL2 are required, which can be downloaded directly from here for Linux and macOS (or compiled from source).