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.
mod BLACKBOARD is pr NAT . sort Blackboard . subsort Nat < Blackboard . vars M 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  2 4 6 8 using play . srewrite  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
continuously applies the rewrite rule
play to the two
minimum values in the blackboard using some auxiliary operations:
smod BLACKBOARD-STRAT is protecting BLACKBOARD . strat minmin @ Blackboard . vars X Y M N : Nat . var B : Blackboard . sd minmin := (matchrew B s.t. X := minimum(B) /\ Y := minimum(remove(X,B)) by B using play[M <- X , N <- Y] ) ! . op minimum : Blackboard -> Nat . op remove : Nat Blackboard -> Blackboard . eq minimum(N) = N . eq minimum(N M) = if (N < M) then N else M fi . eq minimum(N M B) = if (N < M) then minimum(N B) else minimum(M B) fi . eq remove(X, X B) = B . eq remove(X, B) = B [owise] . endsmAnd then the defined strategies can also be used in the strategy commands:
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:
Formulae are written as terms of the sort
umaudemc check <Maude file> <initial term> <formula> [<strategy>]
Formulaextended 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.soin 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
umaudemctool is also available on PyPI and can be installed with
pip install umaudemc.
Some examples and documentation are available:
choice(w1: α1, ..., wn: αn)that randomly chooses of the strategies
αkaccording to the weights
sample X := distrib(args) in αthat samples the variable
Xaccording to the distribution
args. The sort of
Xand of the comma-separated arguments must be
Float. Available distributions are
dsrewritecommand in the version of the Maude interpreter distributed in this page, and the
Term.srewritemethod in the
simaudecommand 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>]
-ndetermines the number of simulations,
-jthe number of parallel jobs, and
-random-seedthe initial random seed.
mvmaudeis included to facilitate its usage with syntax
mvmaude <Maude file> <initial term> <MultiQuaTEx query> [<strategy>]
umaudemc. It allows calculating the probability of LTL, CTL, and PCTL formulae, expected values, and transient and steady-state probabilities.
Other alternatives for assigning probabilities are available. The tool alternatively relies on the PRISM or Storm model checkers.
umaudemc pcheck <Maude file> <initial term> <formula> <strategy> --assign strategy [--steps] [--reward <term>]
Here you can find some examples (and also here). Those using parameterization or the strategy-aware model checker are gathered together.
Moreover, the language has been applied by different authors to various interesting examples. Their source code has been updated to the current language version.
More recent applications of the strategy language and its strategy-aware model checker are the following:
A detailed discussion of the Maude LTL model checker for strategy-controlled systems, its theoretical foundations, and several examples.
An application of the strategy language and its model checker to build an interactive environment for membrane systems.
Examples of reflective transformation and generation of strategies, including some language extensions.
An extension of the model checker for strategy-controlled systems to branching-time logics (special issue of WRLA 2020).
A presentation of several new features of Maude 3 including a section on the strategy language.
See also: arXiV preprint
A presentation of the Maude LTL model checker for strategy-controlled systems and its fundamentals.
See also: Extended version
A presentation of the strategy parameterization features in the current version of the language, illustrated by various examples.
An operational semantics for the strategy language by means of a theory transformation, as described above.
An almost up-to-date description of the language and its implementation, with more examples related to automatic deduction.
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).