# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 5 Controlling Multi-Agent Systems by Strategies  
In programming, strategies have been used to evaluate expressions (according to certain rules); we know several evaluation strategies: call by value, call by need, etc. In rewriting systems, strategies establish the sequence of rewrite rules to be applied, and outline the available choices for making decisions. The outcome of implementing a strategy is the subset of computations produced according to the strategy. In what follows, we emphasize the use of strategies to significantly decrease the possible evolutions of multi-agent systems with information sharing. The precise control over the application of rules in Maude 3 was possible after the inclusion of a strategy language [21]. The Maude 3 command srew explores all possible execution paths starting from a given term and produces a set of solutions. The command for rewriting a system t using the strategy alpha is  srew t using alpha, and the output presents the solutions generated; several solutions can be generated because the nondeterminism is not always eliminated by using strategies. The fundamental component of the strategy language is the application of a rule, with the simplest form being the strategy all, which applies the rules without any restrictions. The strategy (all)* repeats the strategy all any positive number of times, including zero times. For example, running the system _TravelSystem_ using the strategy (all)* is performed by using the following command:  
srew {TravelSystem} using (all)*. Since there is no restriction on applying the rules, the number of reachable networks is \(56,400\). In the remainder of this section, we will also examine several other strategies in addition to the iteration strategy \(\alpha^{*}\), as follows:  
* The strategy idle outputs the input system. * The disjunction strategy \(\alpha\mid\beta\) performs either the strategy \(\alpha\) or the strategy \(\beta\). * The conditional strategy \(\alpha\beta\) : \(\gamma\) executes first the strategy \(\alpha\) and then uses its output as input for the strategy \(\beta\); if the strategy \(\alpha\) yields no output, it instead executes the strategy \(\gamma\) on the initial input system (if the strategy \(\beta\) is defined as idle, then the strategy \(\alpha\gamma\beta\) : \(\gamma\) is the same as the strategy \(\alpha\)or-else \(\gamma\)). Note that, in the definitions of the mte function and tick rule, we enforce the passage of time to take place only when no communication, unfolding, updating, or testing can be performed, namely, when the value returned by the mte function is not 0. This means that the strategy (all)* is in fact equivalent to the next strategy called mtestep, which formally describes the order in which the iMASrules from Tables 2 and 3 are applied, as follows:sd step := ( Iff | Iff | Move | Comm | Input0 | Output0  | UnfoldBus | UnfoldCab | UnfoldStudent | UnfoldScheduleBus  | UpdatePrivate | UpdatePublic | CreatePrivate | CreatePublic ). sd mtestep := (step or-else tick )*. However, the number of solutions can be decreased by establishing a priority among the rules. Since in iMAS the unfolds, tests, creations, updates, and moves could be performed in parallel, one strategy to consider is to keep one of the sequences out of all possible sequences, to apply the Comm, Input0, and Output0 rules afterwards, and the time rule tick last. Formally, this can be described in Maude 3 by the following two strategies:  
sd step1 := UnfoldBus or-else (UnfoldCab or-else (UnfoldStudent  or-else (UnfoldScheduleBus or-else (If or-else (If or-else  (CreatePublic or-else (CreatePrivate or-else  (UpdatePublic or-else (UpdatePublic or-else  (Move or-else (Comm | Output0 | Input0))))))))))). sd mtestep1 := (step1 or-else tick )*. In this instance, applying the strategy mtestep1 to run the system _TravelSystem_ is performed using the following command:  
srew {TravelSystem} using mstep1. Using mtestep1, the number of reachable networks is decreasing to 13424.