# A Strategy-Based Formal Approach for Fog Systems Analysis
## 4 BiAgents* Model Specification
### Virtual Part Modelling
: _The virtual part of a fog system \(F\) is defined by \(\mathcal{A}_{F}\), which is a set of \(a_{i}\) agents such that \(a_{i}=(\mathcal{O},obs,host,mgrt,an,\mathcal{D},int,\mathbb{M},ctr,\mathcal{U})\) where each element is responsible of the definition of an agent's state:_  
* \(\mathcal{O}\) _is the set of the different system's states (bigraphs) that the agent_ \(a_{i}\) _observes_ \((\mathcal{O}\subseteq\mathbb{B})\)_._
* _obs is the function of observing a system's state using the observed bigraph and_ \(a_{i}\) _host,_ \(obs:\mathbb{B}\times V_{\mathbb{B}}\rightarrow\mathcal{O}\)_._  
* _host is the host of the agent (a bigraphical node or region)._
* _mgrt is the function of migration._ \(a_{i}\) _agent can move from any part of the system to another, and even though the layers_ \(mgrt:V_{\mathbb{B}}\times\mathcal{O}\to V_{\mathbb{B}}\)_._  
* _an is the function of analysing an information an_ \(:\mathcal{O}\times V_{\mathbb{B}}\rightarrow\mathcal{D}\)_._  
* \(\mathcal{D}\) _is the set of decisions that the agent_ \(a_{i}\) _can take after an analysis (_\(\mathcal{D}\subseteq\mathbb{L}\)_) with_ \(\mathbb{L}\) _the set of reaction rules labels._  
* \(int\) _is the function of interaction between agents, using the receiver agent_ \(a\subset\mathcal{A}\)_, the actual agent_ \(a_{i}\) _sends a message after analysis._ \(int:\mathcal{A}\times\mathcal{D}\rightarrow\mathbb{M}^{a}\)_._
* \(\mathbb{M}\) _is the set of messages received by the agent_ \(a_{i}\)__  
* \(ctr\) _is the application of a decision taken by an agent after analysis or reception of a message by another agent_ \(ctr:\mathcal{D}\uplus\mathbb{M}\rightarrow\mathcal{P}(\mathcal{U})\) _with_ \(\mathcal{P}(\mathcal{U})\) _the subsets set of_ \(\mathcal{U}\)_._
* \(\mathcal{U}\) _is the set of reaction rules that_ \(a_{i}\) _can apply according to a node of the current bigraph; it represents the set of actions that_ \(a_{i}\) _can do in a specific part of the system_ \((\mathcal{U}\subseteq\mathbb{U})\)_._  
Example 2  
In the LIS example, there are four types of agents: Sensor control, fog control, communication control, and cloud control. According to the specified fog system, there can be many instantiations of each type of agent to make each one focus on a specific task. The virtual part of the BiAgent* modelling the LIS example is \(\mathcal{A}_{F}=a_{s1},a_{s2},a_{s3},a_{FC},a_{ICom},a_{EC}\): Three sensor agents, one fog control agent, two communication control agents, and one cloud control agent. The initial configuration of the considered system is materialised by: the different sensors containing captured data; the different formats relied to the protocols of communications and eventual actions generated in the fog nodes and cloud  
Figure 6: Agent’s possible states. applications; and the multiple agents defined in the fog layer. The algebraic form of the fog system F modelling the LIS system focusing on its locality (i.e., place graph) is given by: \(F\stackrel{{\text{def}}}{{=}}((s_{1}.o_{1})|(s_{2}.o_{2})|(s_{3}.o_{3 })|ac_{1})\parallel(fn_{1}.k_{1})|(fn_{2}.k_{2})|a_{s1}|a_{s2}|a_{s3}|a_{FC}|a_{ ICCom}|a_{ECCom}|a_{CC})\parallel(p_{1}.f_{1})|(p_{2}.f_{2})\parallel(c_{s1}.(k_{3}|d0))\).