## 3 A Model of Deployment-Independent, Self-Organizing, Cyber-Physical Systems
### Cyber System
#### 3.1.2 Formalization: Logical Network Semantics  
On top of the formalization of interactions between pairs of situated components as presented in the previous subsection, we now define the model of a whole logical network, starting from the following grammar:  
\[N ::= 0\left|\right.C\left|\right.(N|N)\] node configuration \[L ::= 0\left|\right.(i,N)\left|\right.(L|L)\] logical network  
A node configuration \(N\) is defined as a composition of components \(C\) by operator \"\(|\)\", and a logical network is defined as a composition of terms of the kind \(\left\langle i,N\right\rangle\), describing a configuration \(N\) situated at a logical device with identifier \(i\). As common in process algebraic approaches [63], we find it useful to define the network semantics first by introducing a congruence relation (i.e., an equivalence relation applicable at any level of depth), equating network configurations defined to be equivalent. This is used to define symbol \"\(|\)\" as multiset composition operator (associative, commutative, and absorbing configuration 0), and to allow blocks \(\left\langle i,N\right\rangle\) to freely break by splitting \(N\); namely:\[N|N^{\prime}\equiv N^{\prime}|N,\quad 0|N\equiv N,\quad N|(N^{ \prime}|N^{\prime\prime})\equiv(N|N^{\prime})|N^{\prime\prime}\] \[L|L^{\prime}\equiv L^{\prime}|L,\quad 0|L\equiv L,\quad L|(L^{ \prime}|L^{\prime\prime})\equiv(L|L^{\prime})|L^{\prime\prime}\] \[\langle i,N|N^{\prime}\rangle\equiv\langle i,N\rangle|\langle i,N ^{\prime}\rangle,\quad\langle i,0\rangle\equiv 0\]  
We then introduce a non-deterministic operational semantics for logical networks by the transition system \(\langle Set(L),\rightarrow_{\mathbf{L}},Set(o)\rangle\). As with transition \(\rightarrow_{\mathbf{N}}\) described in Section 3.1.1, we write \(L\xrightarrow{i\rhd\rhd^{\prime}}_{\mathbf{L}}L^{\prime}\) to mean that logical network \(L\) moves to \(L^{\prime}\) by executing action \(l\) from device \(i\) to \(i^{\prime}\). As already discussed, actions of the kind \(i\rhd l\rhd i\) represent interaction localized inside device \(i\), while \(i\rhd l\rhd i^{\prime}\) with \(i\
eq i^{\prime}\) represents an interaction through the neighboring link connecting \(i\) to \(i^{\prime}\). The transition relation is defined by the following rules:  
\[ \begin{array}{llllll}\text{(L-CONG)}&L_{a}&\xrightarrow{o}_{\mathbf{L}}L_{ b}&\text{if}&L_{a}\equiv L^{\prime}_{a^{\prime}},\quad L^{\prime}_{a} \xrightarrow{o}_{\mathbf{L}}L^{\prime}_{b},\quad L_{b}\equiv L^{\prime}_{b}\\ \text{(L-PAR)}&L_{a}|L&\xrightarrow{o}_{\mathbf{L}}L^{\prime}_{a}|L&\text{if} &L_{a}\xrightarrow{o}_{\mathbf{L}}L^{\prime}_{a}\\ \text{(L-INT)}&L_{a}|L_{b}&\xrightarrow{o}_{\mathbf{L}}L^{\prime}_{a}|L^{ \prime}_{b}&\text{if}&L_{a}:L_{b}\xrightarrow{o}_{\mathbf{N}}L^{\prime}_{a} :L^{\prime}_{b}\end{array} \]  
The former two rules are standard: the first simply states that transitions work modulo the congruence relation; the second states that transitions can be applied to a network sub-part. The key rule is the third one: it selects two logical network pieces \(L_{a}\) and \(L_{b}\) which can interact by transition \(\rightarrow_{\mathbf{N}}\) and action \(o\), and then derives their new states \(L^{\prime}_{a}\) and \(L^{\prime}_{b}\). A logical network \(L\) is said _complete_ if it is congruent to a network of the kind:  
\[L\equiv\langle i_{1},\alpha_{1}|\sigma_{1}|\chi_{1}|\kappa_{1}|\beta_{1} \rangle|\langle i_{2},\alpha_{2}|\sigma_{2}|\chi_{2}|\kappa_{2}|\beta_{2} \rangle|\dots|\langle i_{n},\alpha_{n}|\sigma_{n}|\chi_{n}|\kappa_{n}|\beta_{n}\rangle\]  
namely if every logical device \(i_{k}\) in the network has associated precisely five components, one per kind: \(\alpha_{k}\), \(\sigma_{k}\), \(\chi_{k}\), \(\kappa_{k}\), and \(\beta_{k}\). A network evolution is then defined as a sequence of transitions of the kind:  
\[L_{0}\xrightarrow{o_{0}}_{\mathbf{L}}L_{1}\xrightarrow{o_{1}}_{\mathbf{L}}L_ {2}\xrightarrow{o_{2}}_{\mathbf{L}}\dots\]  
where \(L_{0}\) is complete.