# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 4 Implementing Multi-Agent Systems with Information Sharing  
We supply an implementation to check that the evolutions of the systems described by our prototyping language iMASare performed correctly. Moreover, we emphasize the use of strategies to control the rule application in order to guide the evolution of such a highly nondeterministic and concurrent system. This control is achievable due to the new strategy language of the rewriting engine Maude 3. Maude 3 is a robust software system that supports the efficient execution of specifications based on rewriting logic. Rewriting logic [17] is a computational logic combining term rewriting and equational logic. Starting from the semantic of our language iMAS we define a rewriting theory. Note that the syntax of the rewriting theory is that of Maude [18] for the untimed aspects, and also that of Real-Time Maude [19] for the time aspects. Just like in [20], we use a typed setting that includes sorts, together with the _subsort_ inclusion relationship among types. Considering a given rewrite theory \(\mathcal{R}\), we use \(\mathcal{R}\vdash t\Rightarrow t^{\prime}\) to indicate that \(t\Rightarrow t^{\prime}\) is derivable in \(\mathcal{R}\) by using its rewrite rules. To implement the multi-agent systems defined by iMAS, we utilize sorts that correspond to the sets in our language. For example, the set _Chan_ of channels is represented by the sort Channel, while the sort MValue is utilized to handle multisets of values within the system. For convenience, the iMASterms are decomposed in parts using the sorts AGuard, MGuard, and IGuard. The sort AGuard consists of the prefixes \(a^{A\dagger}!\langle v\rangle\) and \(a^{A\dagger}? (u)\) of all agents \(a^{A\dagger}!\langle v\rangle\) then \(P\) else \(Q\rhd I\) and \(a^{A\dagger}? (u)\) then \(P\) else \(Q\rhd I^{\prime}\), the sort MGuard consists of the prefix go\({}^{\dagger}I\) of all agents go\({}^{\dagger}I\) then \(P\rhd I\), while the sort IGuard consists of the prefix \(upd(p,f,v)\) of all agents \(upd(p,f,v)\) then \(P\rhd I\). The prefixes contained in the sorts AGuard, MGuard, and IGuard are crucial for defining the behavior of agents in a sequential manner. The subsort declaration subsorts Var < Location Channel Nat demonstrates that variables can be instantiated using location names, channel names, or natural numbers. This relationship is part of the broader subsorting hierarchy defined within the system. sorts PId Agent Inf Field MField Test Location Channel Value  VarL VarC VarN Var MValue Process  AGuard MGuard IGuard Guard System GlobalSystem. subsorts Var < Location Channel Nat < Value < MYValue. For each operator in the iMA syntax (as shown in Table 1), we assign two attributes: the ctor attribute, which designates the operator as a data constructor, and the prec attribute, followed by a numerical value, which establishes the operator's precedence in relation to other operators. To accurately represent the parallel operators \(|\) and \(|\) in (Real-Time) Maude, we include the attributes comm and assoc. These attributes signify that the operators are commutative and associative constructors, respectively. This encoding reflects the structural congruence rules of the system. In fact, the majority of the structural rules are implemented through the use of these comm and assoc attributes. op empty : -> Inf [ctor]. ops private public : -> PId [ctor]. op __ : Inf Inf -> Inf [ctor comm assoc id: empty]. op < _ ; _ > : Field Nat -> Inf. op _ _ _ <_> : Channel TimeInf Value -> AGuard [ctor prec 2]. op _ _ _? (_) : Channel TimeInf Var -> AGuard [ctor prec 2]. op go ~_ : Time Location -> MGuard [ctor prec 2]. ops update : PId Field Nat -> IGuard [ctor]. op _then _ else _ : AGuard Process Process -> Process [ctor prec 1]. op _then _ : MGuard Process -> Process [ctor prec 1]. op _ then _ : IGuard Process -> Process [ctor prec 1]. op if _ then _ else _ : Test Process Process -> Process [ctor prec 1]. op stop : -> Process [ctor]. op _ |> - : Process Inf -> Agent [ctor]. op Zero : -> Agent [ctor].