# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 2 Syntax and Semantics of iMAS
\begin{table}
\begin{tabular}{l l} \hline (Stop) & \(\overline{l[[I\lhd\mathsf{0}]]\
ot\to}\) \\ (Com) & \(\overline{l[[I_{l}\lhd a^{M_{1}}!\langle v\rangle\text{ then }P_{1}\text{ else }Q_{1}\rhd I_{1}\mid\mid a^{M_{2}}?(u)\text{ then }P_{2}\text{ else }Q_{2}\rhd I_{2}\mid\mid\vec{A}]]}\) \\  & \(\xrightarrow{a^{\intercal 2\mathsf{P}}!}l[[I_{l}\lhd P_{1}\rhd I_{1}\mid\mid\{v/u\}P_{2} \rhd I_{2}\mid\mid\vec{A}]]\) \\ (Put0) & \(\overline{l[[I_{l}\lhd a^{\mathsf{A0}}!\langle v\rangle\text{ then }P\text{ else }Q\rhd I\mid\mid\vec{A}]]\xrightarrow{a^{\mathsf{A0}} \mathsf{A}}l[[I_{l}\lhd Q\rhd I\mid\mid\vec{A}]]}\) \\ (Get0) & \(\overline{l[[I_{l}\lhd a^{\mathsf{A0}}?(u)\text{ then }P\text{ else }Q\rhd I\mid\mid\vec{A}]] \xrightarrow{a^{\mathsf{A0}}\mathsf{A}}l[[I_{l}\lhd Q\rhd I\mid\mid\vec{A}]]}\) \\ (Move0) & \(\overline{l[[I_{l}\lhd\mathsf{g}^{\mathsf{0}}\,l^{\prime}\text{ then }P\rhd I\mid\mid\vec{A}]]\mid\mid l^{\prime}[[I_{l}^{\prime}\lhd\vec{B}]] \xrightarrow{b^{\mathsf{0}}}l[[I_{l}\lhd\vec{A}]]\mid l^{\prime}[[I_{l}^{ \prime}\lhd P\rhd I\mid\vec{B}]]}\) \\ (IfT) & \(\overline{l[[I_{l}\lhd\text{ if }\text{test then }P\text{ else }Q\rhd I\mid\mid\vec{A}]] \xrightarrow{\text{true}}l[[I_{l}\lhd P\rhd I\mid\mid\vec{A}]]}\) \\ (IfF) & \(\overline{l[[I_{l}\lhd\text{ if }\text{test then }P\text{ else }Q\rhd I\mid\mid\vec{A}]] \xrightarrow{\text{false}}l[[I_{l}\lhd Q\rhd I\mid\mid\vec{A}]]}\) \\ (CrtPu) & \(\overline{l[[I_{l}\lhd upd(public,f,v)\text{ then }P\rhd I\mid\mid\vec{A}]] \xrightarrow{\text{create}}l[[I_{l}\langle f;v\rangle\lhd P\rhd I\mid\mid \vec{A}]]}\) \\ (CrtPR) & \(\overline{\beta}\langle f;v^{\prime}\rangle\in I\) \\ (UpdPU) & \(\overline{l[[I_{l}\lhd upd(private,f,v)\text{ then }P\rhd I\mid\mid\vec{A}]] \xrightarrow{\text{create}}l[[I_{l}\langle f;v\rangle\lhd P\rhd I\mid \vec{A}]]}\) \\ (UpdPR) & \(\overline{l[[I_{l}\lhd upd(private,f,v)\text{ then }P\rhd I\mid\vec{A}]] \xrightarrow{\text{update}}l[[I_{l}\lhd P\rhd I\langle f;v\rangle\mid\vec{A}]]}\) \\ (Call) & \(\overline{l[[I_{l}\lhd id(v)\rhd I\mid\vec{A}]]\xrightarrow{\text{valid}}l[[I_{l} \lhd\{v/u\}P_{\l}\rhd I\mid\mid\vec{A}]]}\) \\ (Par) & \(\overline{N_{1}\xrightarrow{A_{1}}N_{1}^{\prime}\;\;N_{2}\xrightarrow{A_{2}}N _{2}^{\prime}}\) (Equiv) \(\overline{N\equiv N^{\prime}\;\;N^{\prime}\;\xrightarrow{A}N^{\prime\prime} \;\;N^{\prime\prime}\equiv N^{\prime\prime\prime}}\) \\ \(N_{1}\mid N_{2}\xrightarrow{A_{1}\mid A_{2}}N_{1}^{\prime}\;\;N_{2}^{ \prime}\) & \(\overline{N\xrightarrow{A}N^{\prime\prime\prime}}\) \\ \hline \end{tabular}
\end{table} 
Table 2: Operational semantics for our multi-agent systems. If an agent \(\text{go}^{0}\,l^{\prime}\) then \(P\;\rhd\;I\) is at the location \(l\), by using the rule (Move0), it is moving at the location \(l^{\prime}\), where it will behave according to \(P\). An agent _if test_ then \(P\;\text{else}\;Q\rhd I\) checks the truth value of _test_ by making use of the _public_ information available at the current location and of the _private_ information \(I\). Regardless of the truth value of _test_, the agent will remain at the current location; if \(test=true\), then by applying the rule (IfT), the agent will behave according to \(P\) from this point forward, while if \(test=false\), then by applying the rule (IfF), the agent will behave as \(Q\) from this point forward. Depending on the value of \(p\), one of the rules (CrtPr), (CrtPu), (UpdPr), and (UpdPu) will be used by an agent \(upd(p,f,v)\) then \(P\rhd I\). If the field \(f\) does not exist in the \(p=private\) information, then the rule (CrtPr) is used to extend the _private_ information with \(\langle f;v\rangle\); otherwise, if the field \(f\) does exist in the _private_ information, then the rule (UpdPr) is used to update the _private_ information by replacing the value of the existing field \(f\) by \(v\).