## 3 A Model of Deployment-Independent, Self-Organizing, Cyber-Physical Systems
### Platform System and Deployment as a Cyber-Physical Mapping
#### 3.2.1 Formalization: Deployed Network Semantics  
We now incrementally formalize the semantics of a network deployed on a platform system. Let meta-variable \(h\) range over host identifiers (uniquely identifying physical or virtual devices being targets for deployment). A deployed network is a composition of terms \([h]L\), modelling a (complete or incomplete) logical network \(L\) located at a host with identifier \(h\). Although evolving due to the interaction of logical components, deployed networks will then exhibit so-called _global labels_, providing information on both the logical and physical links. As in previous sections, we introduce syntax  
\[D ::= 0\big{|}[h]L\big{|}\big{(}D|D\big{)}\] deployed network \[g ::= (h,i)\rhd l\rhd(h,i)\] global labels  
and corresponding congruence:  
\[D|D^{\prime}\equiv D^{\prime}|D,\quad 0|D\equiv D,\quad D|(D^{ \prime}|D^{\prime\prime})\equiv(D|D^{\prime})|D^{\prime\prime}\] \[[h](L|L^{\prime})\equiv[h]L|[h]L^{\prime},\quad[h]0\equiv 0\]  
We then introduce a non-deterministic operational semantics for deployed networks, by the transition system \(\langle Set(D),\rightarrow_{\mathbf{D}},Set(g)\rangle\). Write \(D\xrightarrow{(h,i)\rhd l\rhd(H^{\prime},i^{\prime})}_{\mathbf{D}}D^{\prime}\) to mean that deployed network \(D\) moves to \(D^{\prime}\) by executing action \(l\) from device \(i\) at host \(h\) to \(i^{\prime}\) at host \(h^{\prime}\  
**Definition 1**. : _Define a deployment mapping any function \(\mu:\text{Set}(L)\mapsto\text{Set}(D)\) such that_ (i)_\(\mu(L|L^{\prime})=\mu(L)|\mu(L^{\prime})\) and_ (ii)_\(\mu(\langle i,N\rangle)=[h]\langle i,N\rangle\) _for some \(h\). Please note that any deployment mapping_\(\mu\) _is such that for any logical network_ \(L\) _then_ \(\mathcal{L}(\mu(L))=L\)_._  
Then, the following correspondence result holds. **Theorem 1**. : _Cyber-Physical correspondence. Given a complete deployed network \(D_{0}\), for any evolution trace_  
\[D_{0}\xrightarrow{g_{0}}_{\boldsymbol{D}}D_{1}\xrightarrow{g_{1}}_{ \boldsymbol{D}}D_{2}\ldots\]  
_there exists an equivalent evolution trace in the corresponding logical network_  
\[L_{0}\xrightarrow{\alpha_{0}}_{\boldsymbol{L}}L_{1}\xrightarrow{\alpha_{1}} _{\boldsymbol{L}}L_{2}\ldots\]  
_and vice-versa, such that for all \(k\), \(L_{k}=\mathcal{L}(D_{k})\) and \(o_{k}=\mathcal{L}(g_{k})\)._  
Proof. : The thesis is straightforwardly proved by the way \(\rightarrow_{\boldsymbol{L}}\) and \(\rightarrow_{\boldsymbol{D}}\) have been constructed, noting that rules D-INT and L-INT share the same premises, and hence, if  
\[D|[h_{a}]L_{a}|[h_{b}]L_{b}\xrightarrow{(h_{a},i_{a})\rhd\rhd\rhd(h_{b},j_{ b})}_{\boldsymbol{D}}D|[h_{a}]L^{\prime}_{a}|[h_{b}]L^{\prime}_{b}\]  
then  
\[\mathcal{L}(D|[h_{a}]L_{a}|[h_{b}]L_{b})\xrightarrow{\mathcal{L}((h_{a},i_{a })\rhd\rhd\rhd(h_{b},i_{b}))}_{\boldsymbol{L}}\mathcal{L}(D|[h_{a}]L^{\prime}_ {a}|[h_{b}]L^{\prime}_{b})\]  
and vice-versa. **Lemma 1**. : _Deployment independence. Given a logical network \(L\) and deployment mappings \(\mu_{a}\) and \(\mu_{b}\), then the deployed networks \(D^{a}=\mu_{a}(L)\) and \(D^{b}=\mu_{b}(L)\) are such that for any evolution trace_  
\[D^{a}_{0}\xrightarrow{g_{0}^{a}}_{\boldsymbol{D}}D^{a}_{1}\xrightarrow{g_{1 }^{a}}_{\boldsymbol{D}}D^{a}_{2}\ldots\]  
_there exists an equivalent evolution trace_  
\[D^{b}_{0}\xrightarrow{g_{0}^{b}}_{\boldsymbol{D}}D^{b}_{1}\xrightarrow{g_{1 }^{b}}_{\boldsymbol{D}}D^{b}_{2}\ldots\]  
_and vice-versa, such that the corresponding logical evolutions are the same, namely for all \(k\), \(\mathcal{L}(D^{a}_{k})=\mathcal{L}(D^{b}_{k})\) and \(\mathcal{L}(g^{a}_{k})=\mathcal{L}(g^{b}_{k})\)._  
Proof. : Straightforward. In this framework, the examples of mappings from Figure 4 can be formalized as follows:  
* _Peer-to-peer (Figure_ 4_a)._ There is a bijection \(i\mapsto h_{i}\) such that for each \(C\), \(\mu(\langle i,N\rangle)=[h_{i}]\langle i,N\rangle\).