An Overview of the Maude Strategy Language and its Applications

Abstract

In the Maude specification language, the behavior of systems is modeled by nondeterministic rewrite rules, whose free application may not always be desirable. Hence, a strategy language has been introduced to control the application of rules at a high level, without the intricacies of metaprogramming. In this paper, we give an overview of the Maude strategy language, its applications, related verification tools, and extensions, illustrated with examples.

1 Introduction

Computation in rewriting logic [29, 30] is the succession of independent rule applications in any positions within the terms. This flexibility is the cornerstone of its natural representation of nondeterminism and concurrency, but it is sometimes useful to restrict or guide the evolution of rewriting. For example, a theorem prover does not blindly apply its inference rules, and the local reactions of a chemical system may be modulated by the environment. Strategies are the traditional resource to express these concerns, but specifying them in Maude involved the not so easy task of using its reflective capabilities. This has changed in Maude 3 with the inclusion of an object-level strategy language to explicitly control the application of rules [15]. Several operators resembling the usual programming language constructs and regular expressions allow combining the basic instruction of rule application to program arbitrarily complex strategies, which can be compositionally defined in strategy modules. The language was originally designed in the mid-2000s by Narciso Martí-Oliet, José Meseguer, Alberto Verdejo, and Steven Eker [27] based on previous experience with internal strategies at the metalevel [12, 14] and earlier strategy languages like ELAN [8], Stratego [10], and Tom [6]. Other similar strategy languages appeared later like $\rho$Log [26] and Porgy [18]. The first prototype was available as a Full Maude extension and it was already given several applications [16, 21, 40,41,42]. Now, since Maude 3.0, the language is efficiently implemented in C++ as part of the official interpreter [15].

As well as an executable specification language, Maude is also a verification tool and systems modeled with strategies need also be verified. Together with Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo, we have extended the Maude LTL model checker to work with strategy-controlled specifications [38] and established connections with external model checkers for evaluating CTL, CTL*, and $\mu$-calculus properties [36]. More recently, we have also developed a probabilistic extension of the Maude strategy language whose specifications can be analyzed using probabilistic and statistical model-checking techniques [32].

This paper is based on an invited tutorial on the Maude strategy language given at WRLA 2022 and explains the language and the aforementioned related topics. Section 2 starts with an introduction to the strategy language, Sect. 3 illustrates it with some more examples and includes references for others, Sect. 4 reviews some related tools and extensions, and Sect. 5 concludes with some remarks for future developments. More information about the strategy language, examples, and its related tools is available at maude.ucm.es/strategies.

2 A Brief Introduction to the Maude Strategy Language

In this section, we give an introduction to the Maude strategy language through an example, without claiming to be exhaustive or systematic. For a comprehensive informal reference about the language, we suggest its dedicated chapter in the Maude manual [13, §10]. Formal semantics, both denotational [32] and operational [28, 38], are also available [35].

Let us introduce the following system module WORDS as running example, where Words are defined as lists of Letters in the latin alphabet. Three rules, swap, remove, and append, are provided to manipulate words.

The swap rule permutates two letters in a word, removes removes one, and append attaches a new letter L to the end of the word. This latter rule is marked nonexec(utable), since it includes an unbound variable in the right-hand side. However, we will be able to execute it with the strategy language.

This rewrite system is nonterminating due to the idempotent swap rule. In fact, for every word with at least two letters, Maude’s rewrite command will loop.

However, we can obtain something useful from this module by controlling rewriting with the strategy language. The command for executing a strategy expression $\alpha$ on a term t is srewrite t using $\alpha$ and its output enumerates all terms that are obtained by this controlled rewriting. Multiple solutions are possible, since strategies are not required to completely remove nondeterminism. The elementary building block of the strategy language is the application of a rule, as cannot be otherwise, whose most basic form is the strategy that applies any rule in the module.

The previous fragment evaluates all on the term i t yielding three different solutions, one for swap and two for remove. This is equivalent to the command search t $\texttt {=>1}$ W:Word that looks for all terms reachable by a single rewrite from t, but the strategy language allows for more flexibility. For instance, if we want to apply only rules with a given label, say swap, we can simply write swap.

Rules are applied in any position of the term by default, as seen in the second and third solutions of the first srewrite command, or in application of swap to the word w o n with result $\{\texttt {\underline{o\,w}\,n}, \texttt {\underline{n}\,o\,\underline{w}}, \texttt {w\,\underline{n\,o}}\}$. If this is not desired, the modifier can be used to limit their application to the whole term, like in or , whose only result is n o w. For being more precise when applying rules anywhere, we can also specify an initial substitution to be applied to both sides of the rule and its condition before matching. For example, $\texttt {swap[L <- w]}$ would instantiate the rule $\texttt {L W R => R W L}$ to $\texttt {w W R => R W w}$ and yield n o w and o w n as solutions. Similarly, $\texttt {swap[L<- w, W <- nil]}$ would turn the rule into $\texttt {w R => R w}$ and produce the single solution o w n.

Substitutions are essential when dealing with nonexecutable rules, like append in the WORDS module, whose unbound variables can then be instantiated. We can execute on the word g o to turn it into a g o a t. In addition to using for ensuring that the letter is appended at the end of the word, the previous strategy introduced a new combinator ; that executes a strategy on the results of the previous one, like functional composition or concatenation. Its identity element is the strategy constant that returns the original term unchanged as only solution. Another pervasive combinator is the disjunction or nondeterministic choice of strategies $\alpha _1 \;\texttt {|}\; \cdots \;\texttt {|}\; \alpha _n$, whose results are the union of the results of its operands. For example, $\texttt {remove[L <- w] | remove[L - n]}$ evaluates on w o n to $\{\texttt {o\,n}, \texttt {w\,o}\}$. The identity element of the disjunction is , which does not produce any solution at all. In a broader sense, we say that a strategy fails when it does not produce any solution.

Suppose we want to calculate all permutations of a given word. This can be achieved by accumulating the words obtained by successive swaps,

swap | (swap ; swap) | (swap ; swap ; swap) | $\cdots$,

until no new words are obtained. The iteration combinator $\alpha \texttt {*}$, which can be inductively described as $\texttt {idle} \,\texttt {|}\, \alpha \,\texttt {;}\, \alpha \, \texttt {*}$, expresses this common pattern. Observe the correspondence between the last strategy combinators and the constructors of regular expressions:

Regular expressions	$\varepsilon$	$\emptyset$	$\alpha \mid \beta$	$\alpha \beta$	$\alpha ^{*}$
Strategy language	idle	fail	$\alpha \,\texttt {|}\,\beta$	$\alpha \,\texttt {;}\,\beta$	$\alpha \,\texttt {*}$

As formalized in [38], the full strategy language is able to describe any recursively enumerable subset of the executions of the original rewrite system, over both finite and infinite words, but regular languages are specially easily expressed with these constructs. Coming back to the example, the expression swap * gives all permutations of the original word, so 24 solutions for g o a t after a total of 81 rewrites. If we only need the solutions that start with g and finish with a letter other than a, we can execute the strategy where is an operator that filters the terms that match a pattern P and satisfy a condition C. Indeed, it works like an when the conditions hold and like a when they do not. Other test variants, and , exist for matching with extension for structural axioms (i.e. matching fragments of the flattened associative and/or commutative operators) or inside subterms, respectively.

In Spanish, the letter h is not pronounced except when preceded by c, so texters and tweeters sometimes obviate it against the criteria of the Royal Spanish Academy. If we do likewise, we would reduce h o l a to its homophone o l a with $\texttt {remove[L <- h]}$. However, we do not want to transform b r o c h a into b r o c a, because they are pronounced differently. We need a new tool to restrict the application to a specific context, and this is the subterm rewriting operators. Their syntax is similar to that of tests

but the subterms matched by the variables $x_1, \ldots , x_n$ in its pattern P are rewritten with strategies $\alpha _1, \ldots , \alpha _n$. The solutions of this operator are the combinations of all solutions obtained for every subterm, which are rewritten independently. For example, will safely remove the first letter of the word if it is an h. For removing h in the middle of the word, we write to ensure that the previous letter is not a c. Notice that we have used instead of , because we do not want to match the whole term but a fragment of the associative list of letters. These two strategies can be combined with a nondeterminsitic choice $\alpha \,\texttt {|}\, \beta$ to remove any silent h letters in a word. For example, applying this strategy to h e c h o yields e c h o but not h e c o. Unfortunately, the word h i p o c l o r h i d r i a is not rewritten to i p o c l o r i d r i a, because only one h is removed at a time. In order to normalize a term with respect to a strategy, i.e. to apply a strategy until it cannot be executed further, the language includes the $\alpha \, \texttt {!}$ combinator. Putting the previous strategy under this normalization operator we obtain an expression that removes all silent h from a word.

Writing strategies as standalone expressions becomes unmanageable as they grow in size. Strategy modules are available to give them name and define them modularly. For example, the following strategy module WORDS-STRAT extends the system module WORDS with two new strategies, rmh and rmh-one, declared with the statement.

The sort after the @ sign indicates which terms are intended to be rewritten by the strategy, although it does not have any practical effect. Each named strategy is assigned zero or more strategy expressions with definitions that start by the keyword or by if they are conditional. In the module above, rmh is the strategy that removes every silent h in a word, while the two definitions of rmh-one remove a single h at initial and inner position, respectively. When the strategy rmh-one is called in rmh, the two definitions for rmh-one are executed nondeterministically, as if their expressions where joined by the disjunction | operator.

One of the greatest advantages of strategy modules is the possibility of defining recursive strategies. For example, the following strategy module WORDS-REPEAT declares a single recursive strategy remove(l, n) with two parameters that removes exactly n occurrences of the letter l in the subject term.

Its semantics is given by two definitions with disjoint matching patterns. For removing zero letters, we simply do nothing with idle.

Otherwise, one occurrence of the letter L is deleted with the remove rule and the strategy itself is called recursively with a decremented counter.

For example, rewriting b a z a a r with remove(a, 2) gives b z a r and b a z r. However, rewrite(a, 4) would fail because of the attempt to call remove for the fourth time. We can make remove(l, n) erase as many occurrences of l as possible but no more than n with the following change on the second definition:

We have used the conditional operator $\alpha \,\texttt {?}\, \beta \,\texttt {:}\, \gamma$ that evaluates $\beta$ on the results of $\alpha$ or $\gamma$ on the original term if $\alpha$ yields no solution. This way, we only invoke the recursive strategy if the remove rule succeeds, and the execution is finished when it fails. Conditional operators are quite general since its condition is an arbitrary strategy and recurrent conditional patterns are given dedicated syntax. For example, $\alpha$ or-else $\beta$ executes $\beta$ only if $\alpha$ fails, and it is equivalent to $\alpha$ ? idle : $\beta$.

3 Some Examples

In this section, we further illustrate the language with three examples. At the same time, we cite other published works where applications of the language have been presented.

3.1 Deduction Procedures

In deductive reasoning, inference rules should be carefully applied to reach the desired conclusions in an efficient way. A free or inadequate application of the rules may loop or lead to a poor performance in many examples of inference systems. For instance, the Davis-Putnam-Logemann-Loveland (DPLL) system for deciding the satisfiability of a Boolean formula has a natural brute-force split rule that generates two subproblems, where the variable x is respectively assumed true and false.

Of course, repeatedly applying this rule will solve the satisfiability problem, but at an exponential cost in the best case. The inference system includes other rules that are better applied first. For example, subsume removes pending clauses with a satisfied atom.

Hopefully, this may remove some variables in C that do not appear elsewhere, avoiding some superfluous case distinctions. A first rudimentary strategy for SAT solving with these rules would be where the dots are occupied by the other simplification rules. A second one can be more selective and apply split to the variable that cancels the most possible clauses. More serious strategies for the DPLL rules are programmed in the Maude strategy language in [20].

Implementations of deduction procedures do not usually individualize the rules in their code, but rule-based systems like Maude can easily separate the basic logic and its control using strategies. In the literature, this has been encouraged by the Kowalski’s motto Algorithm = Logic + Control [22] or Lescanne’s Rule + Control approach [24]. This latter work implements in Caml four equational completion procedures on top of the inference rules by Bachmair and Dershowitz [5], decoupling at some extent the rules from their control. These same completion procedures have also been specified using the initial prototype of the Maude strategy language in [42] and an improved redesign of this specification is available in [32]. In this latter version, we have clearly separated the inference rules in a system module COMPLETION and the four deduction procedures in four strategy modules being protected extensions of COMPLETION, as depicted in Fig. 1. Each procedure is a recursive strategy that maintains the inference state in its call arguments without modifying the term or adding more rules.

Fig. 1.

Equational procedure specification with clear separation of concerns.

Following similar ideas, other examples of deduction procedures are programmed using the Maude strategy language like congruence closure [16], the Martelli-Montanari unification procedure [1], and a Sudoku solver [40].

3.2 Semantics of Programming Languages

Strategies are also meaningful when dealing with semantics of programming languages. Structural operational semantics define the small-step behavior of programs through inference rules whose premises are steps for the constituents of the program. In this sense, they are not much different to the deduction procedures seen in the previous section, and the Maude strategy language can be useful to describe them [9]. Strategies are particularly useful to generalize semantic rules with negative premises or rule precedence, which are not easily captured otherwise. For example, negation in Prolog is described by the following rule

that removes the negated goal $\mathtt {\backslash +} \, g$ from the goal list if g cannot be solved. This premise can be expressed with the strategy combinator . Indeed, we have specified an executable Prolog interpreter in [13] where negation and cuts are described with strategies.

Let us illustrate the relation between strategies and programming with two simple strategies for the untyped $\lambda$-calculus. We specify the basics of this formalism in the following module LAMBDA.

As usual, there are only two constructors of $\lambda$-terms, abstraction $\lambda x. M$ and application $M \, N$, and we consider a single reduction rule beta that transforms $(\lambda x. M) N$ into M[x/N] where every occurrence of x is replaced by N in M. There may be multiple positions where to apply the $\beta$ rule in a $\lambda$-term, called $\beta$-redexes, but the Church-Rosser theorem tells that the calculus is confluent, i.e. if we can reduce $t \rightarrow ^* t_1$ and $t \rightarrow ^* t_2$, there exists a $t'$ such that $t_1 \rightarrow ^* t'$ and $t_2 \rightarrow ^* t'$. Nevertheless, how rules are applied still matters, since some reductions may lead to a normal form while others may diverge for the same term (see Fig. 2). Another classical result of the $\lambda$-calculus tells that repeatedly reducing the outer leftmost redex always leads to a normal form in case it exists, and this can be expressed as a strategy.

Fig. 2.

Two reduction paths from the $\lambda$-term $(\mathbf{K }\mathbf{I}) \, \varOmega$.

In the strategy module LAMBDA-STRAT, we extend LAMBDA with two strategies normal and applicative for reducing $\lambda$-terms, but more variants can be defined like call-by-value and call-by-name. These are covered in an extended specification of this example [32, 34].

The definition of normal describes a single reduction step of the normalization strategy mentioned in the previous paragraph, i.e. applying beta on the outer leftmost redex.

For completely reducing a term, we can simply write normal ! with the normalization operator. Alternatively, $\lambda$-terms can be reduced in the usual applicative order, by selecting the inner rightmost redex.

However, this new strategy does not ensure that a normal form is reached if it exists. We can see it by running the K I Omega term of Fig. 2 under both strategies.

The normal form $\mathbf{I }\equiv \lambda x. x$ is reached with normal, but it is not with applicative. Notice that the srewrite command finishes even though the strategy does not terminate.

This is because the srewrite infrastructure is able to detect execution cycles and interrupt the evaluation of the strategy, but the absence of solutions is the evidence that applicative reduction does not terminate for this term.

The semantics of other programming languages have been addressed with the Maude strategy language like Eden [21], the REC language of Glynn Winskel’s textbook [34], the ambient calculus [31], CCS [27], and the Maude strategy language itself [38].

3.3 Games

Strategies are pervasive in games, most usually for specifying how players can solve or win them. Besides the Sudoku solver [40], already mentioned, the strategy language has been used to work out the 15-puzzle [32], the Hanoi tower’s puzzle [15], to compare different player strategies for Tic-Tac-Toe by model checking [37], and to solve other smaller games [1].

In addition to expressing procedures for solving a game, strategies can also specify intrinsic restrictions that are rather difficult to express with rules. For example, in the river-crossing problem formalization in [36], we use strategies to enforce a precedence that is part of the rules of the game. Here, we briefly describe this example without going into details about the data representation, which are available in the referenced article and in the repository of examples [1]. In the classical river-crossing puzzle, a shepherd needs to cross a river with a wolf, a goat, and a cabbage using a boat with room for two passengers, the shepherd included. The problem is that the wolf would eat the goat and the goat would eat the cabbage as soon as they are left alone without the shepherd in any side of the river. Our representation of the river is left L | right R where L and R are sets of characters and left shepherd wolf goat cabbage | right is the initial state. Four rewrite rules, alone, wolf, goat, and cabbage, let the shepherd cross alone or with the corresponding passenger to the other side. Two more rules, wolf-eats and goat-eats, carry out the threat of the mentioned animal over its “prey”. Moreover, a key restriction is that the wolf and the goat will never miss the opportunity to eat, so eating must happen eagerly before moving. For instance, the wolf rule rewrites the initial state to left goat cabbage | right shepherd wolf, where the goat and the cabbage are left alone. In this situation, the goat-eats rule must be applied to yield left goat| right shepherd wolf, but moving alone is also allowed in the uncontrolled rewrite system. Indeed, we can try to use the search command to solve the problem, by looking for the final state.

This answer would make us think that the problem is solvable. It is indeed, but this command is not an evidence, since recovering the path to this solution gives an invalid sequence of moves.

In the second state the goat-eats rule should be applied, but alone is applied instead.

In order to enforce the precedence of eating over moving we can use the Maude strategy language. The following recursive strategy eagerEating applies rules under this restriction until the final state is reached.

Notice that nonterminating executions are also admitted by the strategy, but they are not a problem for the strategy execution engine because of its cycle detector. We can use the experimental search command controlled by a strategy¹ to find a valid solution for the problem.

3.4 Other Examples

Beyond the examples already cited in the previous sections, other applications of the Maude strategy language have been published like specifications of the Routing Information Protocol [38], membrane systems with several extensions and model checking [39], the simplex algorithm and a parameterized backtracking scheme with instances for finding solutions to the labyrinth, 8-queens, graph m-coloring, and Hamiltonian cycle problems [34], semaphores and processor scheduling policies [38], a branch and bound scheme [1], Bitcoin smart contracts [4], neural networks [41], and more [27].

4 Related Tools and Extensions

In this section, we briefly describe three extensions and related tools for the strategy language: an extended model checker for strategy-controlled systems, the support for reflective manipulation of strategies with some applications, and a probabilistic extension of the language.

4.1 Model Checking

Model checking [11] is an automated verification technique based on the exhaustive exploration of the execution space of the model. The properties to be checked are usually expressed in temporal logics like Linear-Time Temporal Logic (LTL) or Computation Tree Logic (CTL). Its integrated model checker for LTL is one of the most widely used features of Maude [17]. However, it cannot be applied to strategy-controlled specifications, since it does not know anything about strategies. In order to solve this, we implemented a strategy-aware extension [33, 38] of this LTL model checker, which has been extended for branching-time temporal logics in subsequent works [36].

Intuitively, a strategy describes a subset of the executions of the original model or a subtree of the original computation tree, so the satisfaction of a linear-time or branching-time temporal property in a strategy-controlled system should be evaluated on these representations of its restricted behavior. For example, in the river-crossing puzzle of Sect. 3.3, the LTL formula $\square \,( risky \rightarrow \square \,\lnot \, goal )$ (once a risky state –where an animal is able to eat– is visited, the goal is no longer reachable) does not hold in the uncontrolled system

but it does hold when the system is controlled by the eagerEating strategy.

However, the property $\diamond \, goal$ (the goal is eventually reached) does not hold in any case, since the shepherd may keep moving in cycles, for example.

Counterexamples returned by the strategy-aware model checker are executions allowed by the strategy, which are often shorter or easier to understand. The usage of the strategy-aware model checker is documented in [38] and it can be downloaded from maude.ucm.es/strategies, along with examples and documentation. Branching-time properties in CTL, CTL*, and the $\mu$-calculus can also be checked with the umaudemc tool [36], also available at this website. For example, we can check the CTL* property $\mathbf{A }(\square \, \lnot \, risky \rightarrow \mathbf{E }\,\diamond \, goal )$, saying that we can eventually reach the goal by avoiding risky states, which holds both with and without strategy.

4.2 Reflective Manipulation of Strategies

Even though the strategy language was introduced to avoid the complications of the metalevel when controlling rewriting, reflection is still useful in the context of strategies. Like any other Maude feature, the strategy language, strategy modules, and the associated operations are reflected at the metalevel [13, §17.3]. First, every combinator of the language is declared as a term of sort Strategy or its subsorts in the META-STRATEGY module of the Maude prelude.

Then, strategy modules and their statements are defined as data in META-MODULE.

Finally, the srewrite and dsrewrite² commands are metarepresented in the META-LEVEL module.

Strategies can be reflectively generated and transformed using these tools with interesting applications. In [37], we explain metaprogramming of strategies with several examples, from a theory-dependent normalization strategy for context-sensitive rewriting [25] to extensions of the strategy language itself. For instance, the similar strategy languages ELAN [8] and Stratego [10] include some constructs that are not available in Maude, like congruence operators $f(\alpha _1, \ldots , \alpha _n)$ for applying strategies to every argument of a symbol f. However, these absences are not substantial, since most can be easily expressed using the combinators of the Maude strategy language, for which an automated translation can be programmed at the metalevel.

Multistrategies is another more complex extension that allows distributing the control of the system in multiple strategies $\alpha _1, \ldots , \alpha _n$ orchestrated by another one $\gamma$. Typically, each strategy $\alpha _k$ describes the behavior of a component, agent, or player of the system, while $\gamma$ specifies how their executions are interleaved. Namely, $\gamma$ can make them execute concurrently at almost rule-application granularity, by turns, or in other arbitrary ways. Systems controlled by multistrategies can be executed and model checked with an implementation that relies on the metarepresentation of the strategy language.

Yet another example is an extensible small-step operational semantics of the Maude strategy language, already mentioned in Sect. 3.2. It is specified with rules and strategies that manipulate terms and strategies at the metalevel [38]. Of course, running strategies or model checking under this semantics is not useful in practice, since the builtin implementation of the language is much more efficient. However, experimentation is easier with this specification. For instance, a synchronized rewrite or intersection operator $\alpha \wedge \beta$ denotes the rewriting paths allowed by both $\alpha$ and $\beta$, which cannot be expressed in terms of the original combinators. Nevertheless, $\alpha \wedge \beta$ can be implemented with a pair of two execution states of the semantics that are advanced in parallel as long as they represent the same term.

4.3 A Probabilistic Extension

In addition to qualitative properties, quantitative aspects like time, cost, and probabilities are relevant when analyzing the behavior of systems. Statistical methods are often used to estimate them by simulation, that is, by evaluating the measures on many executions generated at random. However, for this analysis to be sound, all sources of nondeterminism must be quantified. We argued before that strategies are a useful resource to restrict nondeterminism, but they are also suitable for quantifying it. Indeed, probabilistic choice operators have been proposed for ELAN [7] and are available in Porgy [18]. In the context of Maude, PSMaude [7] proposes a restricted strategy language for quantifying the choice of positions, rules, and substitutions. These latter specifications can be simulated and model checked against PCTL properties.

For the specification of probabilities in the Maude strategy language, new combinators have been added. The first one is equivalent to those of ELAN and Porgy.

• A quantified version of non-deterministic choice $\alpha _1 \mid \cdots \mid \alpha _n$ where each alternative is associated a weight

  

  Weights $w_k$ are terms of sort Nat or Float that are evaluated in the context where the strategy is executed. The probability of choosing the alternative $\alpha _k$ is $\sigma (w_k) / \sum _{i=1}^n \sigma (w_i)$ where $\sigma$ is the current variable context.

• A sampling operator from a probabilistic distribution $\pi$ to a variable X that can be used in a nested strategy $\alpha$

  

  The repertory of available distributions includes bernoulli(p), uniform(a, b), norm($\mu$, $\sigma$), exp($\lambda$) (for the exponential distribution), and gamma($\alpha$, $\lambda$). Their parameters are also evaluated in the current variable context.

These operators are not currently available in the official version of Maude, but in the extended version including the strategy-aware model checker in Sect. 4.1. They can be used in the usual srewrite and dsrewrite commands, and in the metaSrewrite function. When a operator is evaluated, a variable is sampled at random and the nested $\alpha$ is executed with this random value. When a is executed, one of the strategies is chosen at random according to their probabilities.

Fig. 3.

Coin toss module.

We can apply both statistical and probabilistic model-checking methods on these specifications enhanced with probabilities. For instance, suppose we model tossing a coin like in Fig. 3, with two constants head and tail, two homonym rules, and two homonym atomic propositions. A fair coin can then be modeled with the strategy choice(1 : head, 1 : tail). The expected number of steps until the first tail is obtained can be estimated with the scheck subcommand of umaudemc.

The simulation is driven by an expression in the QuaTEx language of PMaude [2] specified in the firstTail.quatex file, where # means in the next step.

However, statistical model checking is more useful when continuous-time aspects are involved, i.e., when using the sample operator. For discrete models like this one, we can also use probabilistic model-checking techniques. This is available through the pcheck subcommand of umaudemc and relies on either the PRISM [23] or Storm [19] model checkers. The following command is equivalent to the previous one but using probabilistic methods.

As well as obtaining expected values, pcheck allows calculating the probabilities that a temporal formula in LTL, CTL, PCTL, and other logics holds.

For complementing this haphazard appetizer, more information on the probabilistic extensions can be found in [32] and the strategy language website.

5 Conclusions

In this tutorial, we have provided an overview of the Maude strategy language, illustrated with several examples, and explained some extensions and associated tools. We refer the interested reader to the works cited in the paper and to the maude.ucm.es/strategies website to complete the information about the strategy language and those tools.

As future work, we plan extending the probabilistic strategy language in Sect. 4.3 with an operator to quantify the choice of matches

and new verification features. Another natural and interesting extension of the strategy language is its application to narrowing [3].