# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 6 Model Checking Multi-Agent Systems with Information Sharing  
Since the temporal aspects of iMASsystems together with the private and public information lead to a large number of possible interactions, the verification should be much easier by using software tools. For the iMASnetworks controlled by strategies, we can examine and validate multiple properties by employing the model-checking tool umaudemc of the unified Maude 3 [24]. The command-line syntax for invoking the umaudemc tool is as follows:  
umaudemc check <file name> <initial term> <formula> [ <strategy> ]  
The umaudemc tool analyzes the input formula, determines the most general logic that the formula fits into, and subsequently invokes corresponding model checkers like NuSMV [25] and Spot [26]. To show how it works, we verify a few CTL\({}^{*}\) properties of the multi-agent system presented in Section 3. The branching-time logic CTL\({}^{*}\)[27] is an extension of both the LTL [28] and CTL [29] logics. Formulas in CTL\({}^{*}\) are formulated using the atomic propositions of a Kripke structure, along with a set of temporal operators and path quantifiers  
\(\Phi:=\bot\ |\ \top\ |\ p\ |\ \
eg\Phi\ |\ \Phi\wedge\Phi\ |\ \Phi\vee\Phi\ |\ \Delta\phi\ |\ \ E\phi\)  
\(\phi:=\Phi\ |\ \
eg\phi\ |\ \phi\wedge\phi\ |\ \phi\vee\phi\ |\ \Diamond\phi\ |\ \Di  
\[||student(univ,home)\rhd(AID;301)\langle WT(univ);2\rangle\langle WT(home);2 \rangle\langle STT;0\rangle\] \[||schedule\rhd\langle AID;401\rangle\langle BTT;8\rangle]]\] \[|home[|(BAT;4)\lhd schedule\rhd\langle AID;402\rangle\langle BTT;8 \rangle]]\]  
The CTL* formula A \(\sqcap\)E\(\circ\)AIDInLocation(\(\langle AID;201\rangle\), \(univ\)) in which the expression \(AIDInLocation(\langle AID;id\rangle,loc)\) checks if an agent with \(id\) is in location \(loc\) describes that every state of _TravelSystem_ can be continued to one where the \(cab\) is located at the location \(univ\). Interestingly, this formula is not satisfied under the mtestep strategy, but it is satisfied under the mtestep2 strategy. $ unaudemc check iMASSpecStrat.maude {TravelSystem}  'A [] E \(\rhd\) AIDInLocation( < AID ; 201 >, univ)' mtestep  The property is not satisfied in the initial state (112800 system  states, 1097608 rewrites, holds in 34565/112800 states)  
$ unaudemc check iMASSpecStrat.maude {TravelSystem}  'A [] E \(\rhd\) AIDInLocation( < AID ; 201 >, univ)' mtestep2  The property is satisfied in the initial state (744 system states, 3719 rewrites, holds in 744/744 states) The reason is that, in the mtestep2 strategy, we enforce communication to happen before communication capabilities expire (if this is possible). We can also verify the next LTL formula that checks if always both the \(bus\) and the \(student\) are infinitely often located at \(univ\). This is not satisfied because the \(bus\) always moves between locations, regardless if anyone boards it or not, while the \(student\) gets stuck at \(home\) after the first trip with the \(bus\). The fact that the \(student\) remains stuck at the location \(home\) once it reaches it is because there is no \(cab\) available at \(home\) and the timeouts assigned to the \(bus\) and \(student\) prevent them from interacting in the future.