# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 2 Syntax and Semantics of iMAS
If the field \(f\) does not exist in the \(p=public\) information, then the rule (CrtPu) is used to extend the _public_ information with \(\langle f;v\rangle\); otherwise, if the field \(f\) does exist in the _public_ information, then the rule (UpdPu) is used to update the _public_ information by replacing the value of the existing field \(f\) by \(v\). This does not lead in a change of the current location of the agent that will behave according to \(P\) from this point forward. An agent \(id(v)\rhd I\) can use the rule (Call) to unfold the recursive definition \(id(v)\). This does not lead in a change of the current location of the agent that will behave according to \(\{v/u\}P_{id}\) from this point forward. The rule (Par) is applied to obtain the behavior of large systems by putting in parallel the behavior of smaller ones, while the rule (Equiv) is used to re-arrange networks by means of the structural equivalence relation \(\equiv\). In Table 3, we use the relation \(N\overset{\iota}{\rightsquigarrow}N^{\prime}\) to denote the passing of \(t\) units of time in the network \(N\) in order to transform it into the network \(N^{\prime}\). In the rule (DStop), a network consisting of only a location \(l\) with _public_ information \(I_{l}\) and no agents will not be affected by the passage of time. If the timer of the active action of an agent \(a^{\Delta t}\;\text{\tt then}\;P\;\text{else}\;Q\rhd I\) (with \(*\in\{!\langle v\rangle,? (u)\}\)) is greater than \(0\), then the timer is decreased by using the rules (DPut) and (DGet). Similarly, if the timer of the active action of an agent \(\text{go}^{t}\,l^{\prime}\) then \(P\rhd I\) is greater than \(0\), then the timer is decreased by using the rule (DMove). This does not lead in a change of the current location of the agent or in its information \(I\). \begin{table}
\begin{tabular}{l l} \hline \hline (DStop) & \(\overline{l[[I_{l}\lhd\,\emptyset]]\overset{\iota}{\rightsquigarrow}l[[I_{l} \lhd\,\mathsf{0}]]\) \\ \multirow{2}{*}{(DPut)} & \(t\geq t^{\prime}\geq 0\) \\  & \(l[[I_{l}\lhd\,a^{\Delta t}\{v\}\,\text{then}\;P\;\text{else}\;Q\rhd I]]\overset{ \iota^{\prime}}{\rightsquigarrow}l[[I_{l}\lhd\,a^{\Delta t-l^{\prime}}\{v\}\, \text{then}\;P\;\text{else}\;Q\rhd I]]\) \\ \multirow{2}{*}{(DGet)} & \(t\geq t^{\prime}\geq 0\) \\  & \(l[[I_{l}\lhd\,a^{\Delta t}\{?(u)\;\text{then}\;P\;\text{else}\;Q\rhd I]]\overset{ \iota^{\prime}}{\rightsquigarrow}l[[I_{l}\lhd\,a^{\Delta t-l^{\prime}}\{?(u) \;\text{then}\;P\;\text{else}\;Q\rhd I]]\)} \\ \multirow{2}{*}{(DMove)} & \(t\geq t^{\prime}\geq 0\) \\  & \(l[[I_{l}\lhd\,\text{go}^{t}\,l^{\prime}\;\text{then}\;P\rhd I]]\overset{ \iota^{\prime}}{\rightsquigarrow}l[[I_{l}\lhd\,\text{go}^{t-l^{\prime}}\,l^{ \prime}\;\text{then}\;P\rhd I]]\) \\ \multirow{2}{*}{(DPar)} & \(\frac{N_{1}\overset{\iota}{\rightsquigarrow}N_{1}^{\prime}}{N_{2}\overset{ \iota}{\rightsquigarrow}N_{2}^{\prime}}{N_{1}\mid N_{2}\overset{\iota}{ \rightsquigarrow}}\) \\  & \(N_{1}\mid N_{2}\overset{\iota}{\rightsquigarrow}N_{1}^{\prime}\mid N_{2}^{ \prime}\) \\ \multirow{2}{*}{(DEquiv)} & \(N\equiv N^{\prime}\quad N^{\prime}\overset{\iota}{\rightsquigarrow}N^{\prime \prime}\quad N^{\prime\prime}\equiv N^{\prime\prime\prime}\) \\ \cline{2-2}  & \(N\overset{\iota}{\rightsquigarrow}N^{\prime\prime\prime}\) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Operational semantics of iMAS: time passing. The rule (DPar) is applied to obtain the behavior of large systems by putting in parallel the behavior of smaller ones, while the rule (DEequiv) is used to re-arrange networks by means of the structural equivalence relation \(\equiv\). In the rule (DPar), a network \(N_{1}\mid N_{2}\) that cannot execute any rule of Table 2 is denoted by \(N_{1}\mid N_{2}\
ot\to\); the use of negative premises is possible as they do not lead to inconsistencies.