# A Strategy-Based Formal Approach for Fog Systems Analysis
## 4 BiAgents* Model Specification
### BRS Overview  
A bigraph (Figure 4) is defined by a set of nodes, a set of hyperedges, an inner interface (inner names and sites), and an outer interface (outer name and region). The nodes have a relation of parent and a signature (a number of ports). A bigraph may be algebraic. The parallel product (noted \(\|\)) depicts the juxtaposition of two bigraphs; the fusion (noted \(\|\)) is the fusion of the elements of two bigraphs; the implication (noted.) is the insertion of a node into another; and the identity (noted \(id\)) is the elementary bigraph (i.e., a region and a site). More details about bigraphs can be found in [10].  
In bigraphs, sorts are used to classify controls and links. A sorting discipline is a triple \(\Sigma=\{\Theta,K,\Phi\}\), where \(\Theta\) is a non-empty set of sorts; \(K\) is a signature; and \(\Phi\) is a set of formation rules. A formation rule is a set of properties satisfied by a bigraph. Disjunctive sorts are written as \(\widehat{ab}\), expressing that a node can either be of sort \(a\) or sort \(b\).  
A Bigraphical Reactive System (BRS) is a set of bigraphs and a set of reaction rules. Each bigraph represents a state of a system. Reaction rules define the execution of a system (by going from one state to another). A reaction rule \(R_{i}\) is a pair \((R,R^{\prime})\), where \(R\) is called redex and \(R^{\prime}\), reactum. In this article, we consider that each reaction rule is labelled with a name, and a reaction rule \(R_{i}\) is noted: \(R_{i}\stackrel{{\mathrm{def}}}{{=}}R\to R^{\prime}\).  
The evolution of a system from the state \(St\) to \(St^{\prime}\) is made by checking if the redex \(R\) is present in the state bigraph \(St\) and by replacing it with \(R^{\prime}\) to reach to a new state bigraph of the system \(St^{\prime}\).  
There are many BRS extensions in the literature according to the need of each proposition as binding bigraphs [22], stochastic bigraphs [23], bigraphs with sharing [24], directed bigraphs [25], and BiAgents [11]. The BiAgents extension [11] is proposed to extend Bigraphs with agents that are able to observe, control, and migrate through a bigraph. Their purpose is to \"clearly separate the virtual and physical components of a model and limit the interaction of both by semantics.\"  
Figure 4: A bigraph anatomy.  
In the present work, we consider a BiAgents extension of [9]. We refine its definition noted as BiAgents* in order to maintain the separation between both bigraphs and agents concepts and to specify more accurately the behaviour of the agent part. Indeed, an agent observes its environment, analyses it, takes a decision, may communicate it to other agents, and controls the bigraphical part by triggering reaction rules, in addition to its capacity to migrate through different bigraphical nodes and regions.  
The formalism of BiAgents* is composed of two models:  
\[BiAgent^{*}=\mathcal{A}\bullet\mathcal{B}\]  
where \(\mathcal{B}\) models formally the physical aspect of any system and \(\mathcal{A}\) the virtual one.  
In our approach, we start by modelling the physical part of a fog system using the physical structure of a BiAgent*. After that, we model the virtual part using the virtual structure of a BiAgent*. Moreover, we specify how these structures behave in a smart way using concepts related to the BiAgents* formalism. Table 2 explains how we model the different concepts presented in the architecture CLA4 Fog.  
Obviously, each element of the CLA4 Fog architecture has a semantic interpretation in the context of BiAgents* model. In general, a region represents a layer in the architecture. Place graphs define physical entities of each layer. Link graphs materialise connexions between these entities, and agents represent virtual entities managing the functioning of a fog system.