## 3 A Model of Deployment-Independent, Self-Organizing, Cyber-Physical Systems
### Cyber System
#### 3.1.1 Formalization: Device Semantics  
We formalize the main structure and behavioral elements of a cyber system by an operational semantics describing how the various components of a logical device interact with each other (and then how the whole logical network correspondingly evolves--Section 3.1.2). In doing so, we specifically identify how inner components are abstracted, hence clarifying their boundary, role and interactions. We adopt several mathematical conventions frequently used in works in process algebras [63] and core calculi for programming languages and concurrent systems [64], which we here briefly recap. To capture the behavior of interactive systems we use labelled transition systems [63] which are triples \(\langle\mathit{State},\rightarrow,\mathit{Label}\rangle\) of a set _State_ of states, a ternary relation \(\rightarrow\subseteq\mathit{State}\times\mathit{Label}\times\mathit{State}\), and a set _Label_ of labels. We write \(st\xrightarrow{\ell}st^{\prime}\) as a shorthand for \((st,\ell,st^{\prime})\in\rightarrow\), meaning that the modelled system moves from state \(st\) to \(st^{\prime}\) by an observable action \(\ell\). To describe interactive behavior we then give axioms and rules defining the triples in the relation \(\rightarrow\). We introduce meta-variables for the various element types of the model, which are used both as non-terminal symbols in grammars and in rules of the operational semantics: we let meta-variable \(s\) range over values produced by sensors, \(a\) over values sent to actuators, \(x\) over states, \(e\) over coordination messages (also called _exports_) providing an internal representation of the set of messages to send/receive, \(i\) over logical device identifiers, and \(v\) over message values exchanged with other devices. We abstract away the syntax of the elements that such meta-variables range over; on the other hand, when other elements need an abstract syntax, we introduce their meta-variables by non-terminal symbols of grammars instead. As additional notation, for any meta-variable, say \(v\), we let decorations (\(v^{\prime}\), \(v^{\prime\prime}\), \(v_{a}\), and so on) range over the same elements as \(v\), let \(\mathit{Set}(v)\) be the set of elements it ranges over, \(v_{\perp}\in\mathit{Set}(v)\) be used as default value for \(\mathit{Set}(v)\)--unless differently specified, it is assumed that different meta-variables have disjoint sets of elements they range over. To describe the components of a cyber system we introduce the following abstract grammar:  
\[C ::= \alpha\bigm{|}\sigma\bigm{|}\beta\bigm{|}\kappa\bigm{|}\chi\] component \[\kappa ::= \mathtt{pre}(x,e,s)\bigm{|}\mathtt{post}(x,e,a)\bigm{|}\mathtt{ emit}(x,e) \text{state}\] \[m ::= i:v\] message The five kinds of components, of which only \(\kappa\) has a defined structure, are modelled as follows:  
* Actuators define a labelled transition system \(\langle\mathit{Set}(\alpha),\rightarrow_{\mathbf{a}},\mathit{Set}(a)\rangle\): a transition \(\alpha\xrightarrow{a}\alpha^{\prime}\) models an actuator component (generally made of a set of physical actuators) that moves from state \(\alpha\) to \(\alpha^{\prime}\) receiving actuation value \(a\). * Sensors define a labelled transition system \(\langle\mathit{Set}(\sigma),\rightarrow_{\mathbf{s}},\mathit{Set}(s)\rangle\): a transition \(\sigma\xrightarrow{s}s\sigma^{\prime}\) models a sensor component (generally made of a set of physical sensors) that moves from state \(\sigma\) to \(\sigma^{\prime}\) emitting sensor value \(s\). * Behavior component \(\beta\) is a pure function of the kind \(\beta(x,e,\sigma)=(x^{\prime},e^{\prime},\alpha)\), namely it consumes a state, input export, and sensed value, producing a new state, output export, and actuation values.