# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 5 Controlling Multi-Agent Systems by Strategies
This number of reachable networks can be further reduced by considering a more restraining way of applying the rules, namely, by using an approach similar to the one in [22] that forces the rule (Com) to always be applied before the rules (Put0) and (Get0), as follows:  
sd step2 := 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 (UpdatePrivate or-else  (Move or-else (Comm or-else (Output0 | Input0))))))))))))). sd mtestep2 := (step2 or-else tick )*. This application of rules leads to another reduction in the number of reachable networks, more exactly to 372. Note that all the defined strategies are not specific to the running example, but can be used with any iMAS system. The behavior of two parallel agents is typically understood to encompass all possible interleavings of their steps. The actions of both agents can be mixed together in any random sequence such that the order of actions is preserved for each agent. Just like in [23], we consider interleaving based on a specific strategy, as this more accurately reflects how multi-threading operates in modern programming languages. The above strategies show that reducing the quantity of disjunction strategies structured as \(\alpha|\beta\) results in a significant reduction in the state space due to the decrease in the number of applicable rules at **any** step of **any** evolution. For **any** given network \(N\), if we denote by \(\#(N,strat)=|\{M|N\xrightarrow{strat}^{*}M\}|\) the number of networks reached starting from \(N\) by applying the rules according of the strategy \(strat\), then the following result holds for the mentioned strategies:  
Proposition 1: \(\#(N,all^{*}){=}\#(N,mstep)\geq\#(N,mstep1)\geq\#(N,mstep2)\)Proof. : The motivation for the equality \(\#(N,all^{*})\)=\(\#(N,mstep)\) was provided previously before defining the mtestep strategy. For the inequality \(\#(N,mstep)\geq\#(N,mstep1)\), we use structural induction on \(N\) to prove our claim as follows:  
* \(N\) contains only one agent. This means that, at each step, at most one rule of iMASis applicable, and so \(\#(N,mstep)=\#(N,mstep1)\) regardless of which rule is applicable. * \(N\) contains at least two agents. Depending on the structure of the agents, there exist several cases. Assume that one agent can perform a movement between locations \(l\) and \(l^{\prime}\), and the other can perform an update. In this case, there exist two networks, \(N^{\prime}\) and \(N^{\prime\prime}\), with \(N\xrightarrow{\mathit{l}\mathit{l}\mathit{l}^{\prime}}N^{\prime}\) and \(N\xrightarrow{\mathit{u}\mathit{p}\mathit{d}\mathit{l}}N^{\prime\prime}\). Since these two rules can be applied in parallel, it means that there also exists \(N_{1}\) with \(N^{\prime}\xrightarrow{\mathit{u}\mathit{p}\mathit{d}\mathit{l}}N_{1}\) and \(N^{\prime\prime}\xrightarrow{\mathit{l}\mathit{l}^{\prime}}N_{1}\). This means that \(N^{\prime},N^{\prime\prime},N_{1}\in\{M|N\xrightarrow{\mathit{mtestep}}^{*}M\}\), and \(N^{\prime\prime},N_{1}\in\{M|N\xrightarrow{\mathit{mtestep1}}^{*}M\}\), while \(N^{\prime}\
ot\in\{M|N\xrightarrow{\mathit{mtestep1}}^{*}M\}\), and thus, it holds that \(\#(N,mstep)>\#(N,mstep1)\). The remaining cases can be handled analogously.