# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 2 Syntax and Semantics of iMAS
\begin{table}
\begin{tabular}{c c c c c} \hline _Processes_ & _P,Q_ & \(::=\) & \(\text{go}^{t}\)_l_ then \(P\) & (move) \\  & & \(\mid\) & \(a^{\Delta t}!\langle v\rangle\) then \(P\) else \(Q\) & (output) \\  & & \(\mid\) & \(a^{\Delta t}?(u)\) then \(P\) else \(Q\) & (input) \\  & & \(\mid\) & _if test_ then \(P\) else \(Q\) & (branch) \\  & & \(\mid\) & _stop_ & (termination) \\  & & \(\mid\) & \(id(v)\) & (recursive definition) \\  & & \(\mid\) & \(\mid\) & \(upd(p,f,v)\) then \(P\) & (update) \\ _Information_ & \(I\) & \(::=\) & \(\mathcal{Q}\rhd\langle f;v\rangle\mid I\) \(I\) & \(I\) \\ _Tests_ & _test_ & \(::=\) & _true_ \(\mid\) \(\
eg\)_test_ \(\mid\) _test_\(\wedge\)_test_ \\  & & \(\mid\) & \(get(p,f)>k\) \(\mid\) _get_\((p,f)=k\) \\  & & \(\mid\) & \(get(p,f)>get(p^{\prime},f^{\prime})\) \\  & & \(\mid\) & \(get(p,f)=get(p^{\prime},f^{\prime})\)\(\mid\) & \(\ldots\) & \(p,p^{\prime}\in\{private,public\}\) \\ _Agents_ & _A,B_ & \(::=\) & \(P\rhd I\) \\ _Set of Agents_ & _\(\tilde{A}\)_ & \(::=\) & **0**\(\mid\) & \(\tilde{A}\mid\mid A\) \\ _Networks_ & \(N\) & \(::=\) & _void_ \(\mid\) & \(I[[I\triangle\tilde{A}]]\) \(\mid\) & \(N\mid N\) \\ \hline \end{tabular}
\end{table} 
Table 1: Syntax of our multi-agent systems. by their timers (e.g., because they are at different locations), then the two agents remain at their current locations, and they will behave according to \(Q\) and \(Q^{\prime}\) afterwards. An agent if _test_ then \(P\) 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; it will behave as \(P\) if _test_\(=\)_true_ or as \(Q\) if _test_\(=\)_false_. The agent \(\mathit{upd}(p,f,v)\) then \(P\rhd I\), regardless of whether \(p\) is _private_ or _public_, updates the information \(I\), and remains at the current location, where it will behave according to \(P\). The update of \(I\) depends on whether or not the field \(f\) already exists in \(I\): if \(f\) does not exist, then the information \(\langle f;v\rangle\) is created near \(I\), while if \(f\) exists, then the value stored in \(f\) is updated to \(v\). The agent \(0\rhd I\) stays at the current location doing nothing regardless of its _private_ information \(I\). The information consists of pairs \(\langle f;v\rangle\), where \(f\) is a field and \(v\) is the value assigned to \(f\). When we have the _public_ information \(\langle f;v\rangle\) and the _private_ information \(\langle f;v^{\prime}\rangle\), they are treated as different pieces of information (even if they have the same field \(f\)). The stored information, either _private_ (accessed only by the agent to which it belongs) or _public_ (accessed by any agent located where the information is available), is used by agents to perform tests in order to decide how to behave afterwards. For example, the agent if \(\mathit{get}(\mathit{private},f)>k\) then \(P\) else \(Q\rhd I\) checks if the _private_ information associated with the field \(f\) is strictly greater than \(k\), before continuing its execution as \(P\) or \(Q\) at the current location, depending on the returned value. For checking the _public_ information, the agent is only slightly different from the one checking _private_ information, namely, if \(\mathit{get}(\mathit{public},f)>k\) then \(P\) else \(Q\rhd I\). Note that the tests can only _get_ information from the _private_ and _public_ information, while the update of information is performed only by the _upd_ action. In Table 1, all variables are free, except for the variable \(u\) appearing in the agent \(a^{\Delta t}? (u)\) then \(P\) else \(Q\rhd I\) that is bound within \(P\), but not in \(Q\). The sets of free variables appearing in \(P\) and \(N\) are denoted by \(\mathit{fp}(P)\) and \(\mathit{fp}(N)\). For \(Q\in Id\) such that its process definition is \(Q(u_{1},\ldots,u_{n})=P\), we have that \(\mathit{fp}(P)\subseteq\{u_{1},\ldots,u_{m_{it}}\}\).