We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber
and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations.
We introduce algebraic operations on such sequences to model different kinds of component composition.
These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors.  Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behavior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.

§ INTRODUCTION

Compositional approaches in software engineering reduce the complexity of
specification, analysis, verification, and construction of software by decomposing it into (a) smaller parts, and (b) their interactions. Applied recursively, compositional methods reduce software complexity by breaking the software and its parts into ultimately simple modules, each with a description, properties, and interactions of manageable size. The natural tendency to regard each physical entity as a separate module in a Cyber-Physical System (CPS) makes compositional methods particularly appealing for specification, analysis, verification, and construction of CPSs. However, the distinction between discrete versus continuous transformations in modules representing cyber versus physical processes complicates the semantics of their specification and their treatment by requiring: (1) distinct formalisms to model discrete and continuous phenomena; (2) distinct formalisms to express composition and interactions of cyber-cyber, cyber-physical, and physical-physical pairs of modules; and (3) when to use which formalism to express composition and interactions of hybrid cyber-physical modules.
Our work is distinguished from existing work in the following sense.

First, we make coordination mechanisms explicit and exogenous to components.
Components are standalone entities that exhibit a behavior (which may be described by a finite state automaton, hybrid automaton, or a set of differential equations), and the interaction between component is given by a set of constraints on behaviors of each component. One such composition operation, also widely used in the design of modular systems <cit.> is set intersection: each component interacts with other component by producing a behavior that is consistent with shared events. We generalize such composition operations to ease the specification of interaction between cyber-physical components. We also show the benefit in modeling interaction exogenously when it comes to reasoning about, say asymmetric product operations, or proving some algebraic properties.

Then, we unify cyber and physical aspects within the same semantic model. While this feature is present in some other works (e.g., signal semantics for cyber-physical systems <cit.>, time data streams for connectors <cit.>), we add a structural constraint by imposing an observable to be a set of events that happen at the same time. As a result, we abstract the underlying data flow (e.g., causality rules, input-output mechanism, structural ports) that must be implemented for such observable to happen in other models. We believe that this abstraction is different from traditional approaches to design cyber-physical systems and, for instance, may naturally compose a set of observations occurring at the same time to a new observation formed by the union of their observables. The TES model proposed in this paper differs from the trace semantics in <cit.> in that it explicitly and directly expresses synchronous occurrences of events. Like the one in <cit.> but unlike many other trace semantics that effectively assume a discrete model of time, the TES model is based on a dense model of time. These distinctions become significant in enabling a compositional semantic model where the sequences of actions of individual components/agents are specified locally, not necessarily in lock-step with those of other entities. It is on this basis that we can define our expressive generic composition operators with interesting algebraic properties. The advantages of this compositional semantics include not just modular, reusable specification of components, but also modular abstractions that allow reasoning and verification following the assume/guarantee methodology.

Finally, we give an alternative view on satisfaction of trace and behavioral properties of cyber-physical systems. We expose properties as components and show how to express coordination as a satisfaction problem (i.e., adding to the system of components a coordinator that restricts each component to a subset of their behavior to comply with a trace property).
We show that trace properties are not adequate to capture all important properties.
We introduce behavioral properties, which are analogous to hyperproperties <cit.>.
We show, for instance, how the energy adequacy property in a cyber-physical system requires both a behavioral property and a trace property.

* we propose a semantic model of interacting cyber and physical processes based on sequences of observations,

* we define an algebraic framework to express interactions between time sensitive components,

* we give a general mechanism, using a co-inductive construction, to define algebraic operations on components as a lifting of some constraints on observations,

* we introduce two classes of properties on components, trace properties and behavior properties, and demonstrate their application in an example.

Our approach differs from more concrete approaches (e.g., operational models, executable specifications, etc.) in the sense that our operations on components model operations of composition at the semantic level.

We first intuitively introduce some key concepts and an example in Section <ref>. We provide in Section <ref> formal definitions for components, their composition, and their properties.
We describe a detailed example in Section <ref>.
We present some related and our future work in Section <ref>,
and conclude the paper in Section <ref>.

§ COORDINATION OF ENERGY-CONSTRAINED ROBOTS ON A FIELD

In this work, we consider a cyber-physical system as a set of interacting processes.
Whether a process consists of a physical phenomenon (sun rising, electro-chemical reaction, etc.) or a cyber phenomenon (computation of a function, message exchanges, etc.), it exhibits an externally observable behavior resulting from some internal non-visible actions.
Instead of a unified way to describe internals of cyber and physical processes, we propose a uniform description of what we can externally observe of their behavior and interactions.

In this section, we introduce some concepts that we will formalize later.
An event may describe something like the sun-rise or the temperature reading of 5$^{\circ}C$.
An event occurs at a point in time, yielding an event occurrence (e.g., the sun-rise event occurred at 6:28 am today), and the same event can occur repeatedly at different times (the sun-rise event occurs every day).
Typically, multiple events may occur at “the same time" as measured within a measurement tolerance (e.g., the bird vacated the space at the same time as the bullet arrived there; the red car arrived at the middle of the intersection at the same time as the blue car did).
We call a set of events that occur together at the same time an observable.
A pair $(O, t)$ of a set of observable events $O$ together with its time-stamp $t$ represents an observation.
An observation $(O,t)$ in fact consists of a set of event occurrences: occurrences of events in $O$ at the same time $t$.
We call an infinite sequence of observations a Timed-Event Stream (TES).
A behavior is a set of TESs.
A component is a behavior  with an interface.

Consider two robot components, each interacting with its own local battery component, sharing a field resource.
The fact that the robots share the field through which they roam, forces them to somehow coordinate their (move) actions. Coordination is a set of constraints imposed on the otherwise possible observable behavior of components. In the case of our robots, if nothing else, at least physics prevents the two robots from occupying the same field space at the same time. More sophisticated coordination may be imposed (by the robots themselves or by some other external entity) to restrict the behavior of the robots and circumvent some undesirable outcomes, including hard constraints imposed by the physics of the field.
The behaviors of components consist of timed-event streams, where events may include some measures of physical quantities.
We give in the sequel a detailed description of three components, a robot (R), a battery (B), and a field (F), and of their interactions.
We use SI system units to quantify physical values, with time in seconds (), charging status in Watt hour (Wh), distance in meters (), force in newton (), speed in meters per second ().

A robot component, with identifier $R$,performs some measurements on its environment and takes decisions as to where to move. We distinguish two kinds of events in the behavior of a robot component has two kinds of events: a read event $(\rread(\bat,R);b)$ that measures the level $b$ of its battery or $(\rread(\loc,R);l)$ that obtains its position $l$, and a move event $(\move(R);(d, \alpha))$ when the robot moves in the direction $d$ with energy $\alpha$ (in ).
The TES in the Robot column in Table <ref> shows a scenario where robot $R$ reads its location and gets the value $(0;0)$ at time $1 \ssec$, then moves north with 20 at time $2 \ssec$, reads its location and gets $(0;1)$ at time $3 \ssec$, and reads its battery value and gets $2000\si{Wh}$ at time $4\ssec$, ....

A battery component, with identifier $B$,encapsulates some physical phenomenon that we use three kinds of events to describe its observables has three kinds of events: a charge event $(\charge(B);\eta_c)$, a discharge event $(\discharge(B);\eta_d)$, and a read event $(\rread(B);s)$,  where $\eta_d$ and $\eta_c$ are respectively the discharge and charge rates of the battery, and $s$ is the current charge status.
The TES in the Battery column in Table <ref>
shows a scenario where the battery discharged at a rate of $20 \si{\watt}$ at time $2 \ssec$, and reported its charge-level of $2000\si{Wh}$ at time $4 \ssec$, ....

Each column displays a segment of a timed-event stream for a robot, a battery, and a field component, where observables are singleton events. For $t \in \Rp$, we use $R(t), B(t)$, and $F(t)$ to respectively denote the observable at time $t$ for the  in the Robot, the Battery, and the Field column. An explicit empty set is not mandatory if no event is observed.
Robot ($R$)            Battery ($B$)                            Field ($F$)                   Robot-Battery-

$1\si{\second}$       $\{(\rread(\loc,R);(0;0))\}$                    $                   $                          $\{(\loc(I);(0;0))\}    $     $R(1) \cup F(1)$

$2\si{\second}$       $\makecell{\{(\move(R); (N,20\si{\watt}))\}}$        $\{(\discharge(B);20\si{\watt})\}$       $\{(\move(I);(N,40\si{\newton}))\}$    $R(2) \cup B(2) \cup F(2)$

$3\si{\second}$       $\{(\rread(\loc,R);(0;1))\}$        $                   $          $\{(\loc(I);(0;1))\}    $     $R(3) \cup F(3)$

$4\si{\second}$       $\{(\rread(\bat,R);2000\si{Wh}) \}$        $\{(\rread(B);2000\si{Wh})\}   $                                    $R(4) \cup B(4)$

$...$                1c$...$            1c$...$      0c$...$      0c$...$

A field component, with identifier $F$,
encapsulates some physical aspects and we use two kinds of events to describe its observables
has two kinds of events: a position event $(\loc(I);p)$ that obtains the position $p$ of an object $I$, and a move event $(\move(I);(d, F))$ of the object $I$ in the direction $d$ with traction force $F$ (in ).
The TES in the Field column in Table <ref>
shows a scenario where the field has the object $I$ at location $(0;0)$ at time $1\ssec$, then the object $I$ moves in the north direction with a traction force of 40  at time $2\ssec$, subsequently to which the object $I$ is at location $(0;1)$ at time $3\ssec$, ....

When components interact with each other,
in a shared environment, behaviors in their composition must also compose with a behavior of the environment.
For instance, a battery component may constrain how many amperes it delivers, and therefore restrict the speed of the robot that interacts with it.
We specify interaction explicitly as an exogenous binary operation that constrains the composable behaviors of its operand components.

The robot-battery interaction imposes that a move event in the behavior of a robot coincides with a discharge event in the behavior of the robot's battery, such that the discharge rate of the battery is proportional to the energy needed by the robot.
The physicality of the battery prevents the robot from moving if the energy level of the battery is not sufficient
(i.e., such an anomalous TES would not exist in the battery's behavior, and therefore cannot compose with a robot's behavior).
Moreover, a read event in the behavior of a robot component should also coincide with a read event in the behavior of its corresponding battery component, such that the two events contain the same charge value.

The robot-field interaction imposes that a move event in the behavior of a robot coincides with a move event of an object on the field, such that the traction force on the field is proportional to the energy that the robot put in the move. A read event in the behavior of a robot coincides with a position event of the corresponding robot object on the field, such that the two events contain the same position value.
Additional interaction constraints may be imposed by the physics of the field.
For instance, the constraint “no two robots can be observed at the same location” would rule out every behavior where the two robots are observed at the same location.

A  for the composite Robot-Battery-Field system collects, in sequence, all observations from a  in a Robot, a Battery, and a Field component behavior, such that at any moment the interaction constraints are satisfied. The column Robot-Battery-Field in Table <ref> displays the first elements of such a .

§ COMPONENTS, COMPOSITION, AND PROPERTIES

Each lemma of the section has its proof in the technical report <cit.>.

§.§ Notations

An event is a simplex (the most primitive form of an) observable element. An event may or may not have internal structure. For instance, the successive ticks of a clock are occurrences of a tick event that has no internal structure; successive readings of a thermometer, on the other hand, constitute occurrences of a temperature-reading event
, each of which has the internal structure of a name-value pair
. Similarly, we can consider successive transmissions by a mobile sensor as occurrences of a structured event, each instance of which includes geolocation coordinates, barometric pressure, temperature, humidity, etc. Regardless of whether or not events have internal structures, in the sequel, we regard events as uninterpreted simplex observable elements.
We use $\mathbb{E}$ to denote the universal set of events.

An observable is a set of event occurrences that happen together and
an observation is a pair $(O,t)$ of an observable $O$ and a time-stamp $t \in \Rp$.[Any totally ordered dense set would be suitable as the domain for time (e.g., positive rationals $\mathbb{Q}_+$). For simplicity, we use $\Rp$, the set of real numbers $r\geq 0$ for this purpose.] An observation $(O,t)$ represents an act of atomically observing occurrences of events in $O$ at time $t$. Atomically observing occurrences of events in $O$ at time $t$ means there exists a small $\epsilon \in \Rp$ such that during the time interval $[t-\epsilon, t+ \epsilon]$:

* every event $e \in O$ is observed exactly once[A finer time granularity may reveal some ordering relation on the occurrence of events in the same set of observation.], and

* no event $e \not \in O$ is observed.

We write $\langle s_0, s_1, ..., s_{n-1}\rangle$ to denote a finite sequence of size $n$ of elements over an arbitrary set $S$, where $s_i \in S$ for $0 \leq i \leq n-1$. The set of all finite sequences of elements in $S$ is denoted as $S^*$.
A stream[The set $\N$ denotes the set of natural numbers $n \geq 0$.] over a domain $S$ is
a function $\sigma : \N \rightarrow S$.
We use
$\sigma(i)$ to represent the $i+1^{st}$ element of $\sigma$, and given  a finite sequence $s = \langle s_0, ..., s_{n-1}\rangle$, we write $s \cdot \sigma$ to denote the stream $\tau \in \N \rightarrow S$ such that $\tau(i) = s_i$ for $0 \leq i \leq n-1$ and $\tau(i) = \sigma(i-n)$ for $n\leq i$. We use $\sigma'$ to denote the derivative of $\sigma$, such that $\sigma'(i) = \sigma(i+1)$ for all $i \in \mathbb{N}$.

A Timed-Event Stream (TES) over a set of events $E$ and a set of time-stamps $\Rp$ is a stream $\sigma \in \N \rightarrow (\mathcal{P}(E) \times \Rp)$ where, for $\sigma(i) = (O_i,t_i)$:

* for every $i\in \mathbb{N}, t_i<t_{i+1}$, [i.e., time monotonically increases] and

* for every $n \in \N$, there exists $i \in \N$ such that $t_i > n$ [i.e., time is non-Zeno progressive].

[Time stream]
We use $OS(\Rp)$ to refer to the set of all monotonically increasing and non-Zeno infinite sequences of elements in $\Rp$.

[Timed-Event Stream]
We use $\TES{E}{T}$ to denote the set of all TESs whose observables are subsets of the event set $E$ with elements in $\Rp$ as their time-stamps.

Given a sequence $\sigma = \langle(O_0,t_0), (O_1,t_1), (O_2,t_2), ...\rangle \in \TES{E}{T}$, we use the projections $\pr_1(\sigma) \in \N \rightarrow \mathcal{P}(E)$ and $\pr_2(\sigma) \in \N \rightarrow\Rp$ to denote respectively the sequence  of observables $\langle O_0, O_1, O_2, ...\rangle$ and the sequence of time stamps $\langle t_0, t_1, t_2, ...\rangle$.

§.§ Components

The design of complex systems becomes simpler if such systems can be decomposed into smaller sub-systems that interact with each other.
In order to simplify the design of cyber-physical systems,
we abstract from the internal details of both cyber and physical processes, to expose a uniform semantic model.
As a first class entity, a component encapsulates a behavior (set of s) and an interface (set of events).

Like existing semantic models, such as time-data streams <cit.>, time signal <cit.>, or discrete clock <cit.>, we use a dense model of time.
However, we allow for arbitrary but finite interleavings of observations.
In addition, our structure of an observation imposes atomicity of event occurrences within an observation.
Such constraints abstract from the precise timing of each event in the set, and turn an observation into an all-or-nothing transaction.

A component is a tuple $C = (E, L)$ where $E \subseteq \E$ is a set of events, and $L \subseteq \TES{E}{\Rp}$ is a set of s.
We call $E$ the interface and $L$ the externally observable behavior of $C$.

More particularly, Definition <ref> makes no distinction between cyber and physical components.
We use the following examples to describe some cyber and physical aspects of components.

Consider a set of two events $E = \{0,1\}$, and restrict our observations to $\{1\}$ and $\{0\}$.
A component whose behavior contains s with alternating observations of $\{1\}$ and $\{0\}$ is defined by the tuple $(E, L)$ where

\begin{array}{cc}
L = \{ \sigma \in \TES{E}{\Rp} \mid \forall i \in \mathbb{N}. &(\pr_1(\sigma)(i) = \{0\} \implies \pr_1(\sigma)(i+1) = \{1\}) \land \\
&(\pr_1(\sigma)(i) = \{1\} \implies \pr_1(\sigma)(i+1) = \{0\}) \}
\end{array}

Note that this component is oblivious to time, and any stream of monotonically increasing non-Zeno real numbers would serve as a valid stream of time stamps for any such sequence of observations.

Consider a component encapsulating a continuous function $f: (D_0 \times \Rp) \rightarrow D$, where $D_0$ is a set of initial values, and $D$ is the codomain of values for $f$.
Such a function can describe the evolution of a physical system over time, where $f(d_0, t) = d$ means that at time $t$ the state of the system is described by the value $d \in D$  if initialized with $d_0$.
We define the set of all events for this component as the range of function $f$ given an initial parameter $d_0 \in D_0$.
The component is then defined as the pair $(D, L_f)$ such that:

L_f = \{ \sigma \in \TES{D}{\Rp} \mid \exists d_0 \in D_0.\ \forall i \in \N.\ \pr_1(\sigma)(i) = \{f(d_0,\pr_2(\sigma)(i))\} \}

Observe that the behavior of this component contains all possible discrete samplings of the function $f$ at monotonically increasing and non-Zeno sequences of time stamp.  Different instances of $f$ would account for various cyber and physical aspects of components.

§.§ Composition

A complex system typically consists of multiple components that interact with each other.
The example in Section <ref> shows three components, a $\robot$, a $\battery$, and a $\field$, where:
a move observable of a robot must coincide with a move observable of the field and a discharge observable of its battery.
The design challenge is to faithfully represent the interactions among involved components, while keeping the description modular, i.e., specify the robot, the battery, and the field as separate, independent, but interacting components. We present in this section a mechanism to describe composability constraints on behavior, and composition operators to construct complex components out of simpler ones.
Such construction opens possibilities for modular reasoning both about the interaction among components and about their resulting composite behavior.

We express composability constraints on behaviors using relations[Also non binary relations could be considered, i.e., constraints imposed on two components.].
we introduce a generalized notion of a composability relation to capture the allowed interaction among two components.
By modeling composability constraints explicitly, we expose the logic of the interaction that governs the formation of a composite behavior between two components.

A composability relation is a parametrized relation $R$ such that for all $E_1, E_2 \subseteq \E$, we have $R(E_1,E_2) \subseteq \TES{E_1}{R} \times \TES{E_2}{R}$.

A parametrized relation $Q$ is symmetric if, for all $(x_1,x_2)$ and for all $(X_1, X_2)$:  $(x_1,x_2) \in Q(X_1,X_2) \iff (x_2,x_1) \in Q(X_2,X_1)$.

A composability relation on s serves as a necessary constraint for two s to compose.
We give in Section <ref> some examples of useful composability relations on s that, e.g., enforce synchronization or mutual exclusion of observables.
We define composition of s as the act of forming a new  out of two s.

A composition function $\oplus$ on   is a function $\oplus: \TES{\E}_\times \TES{\E}_ \rightarrow\TES{\E}{}$.

We define a binary product operation on components, parametrized by a composability relation and a composition function on s, that forms a new component. Intuitively, the newly formed component describes, by its behavior, the evolution of the joint system under the constraint that the interactions in the system satisfy the composability relation.
Formally, the product operation returns another component, whose set of events is the union of sets of events of its operands, and its behavior is obtained by composing all pairs of s in the behavior of its operands deemed composable by the composability relation.

Let $(R,\oplus)$ be a pair of a  composition function and a composability relation on s, and $C_i = (E_i, L_i)$, $i \in \{1,2\}$, two components.
The product of $C_1$ and $C_2$, under $R$ and $\oplus$, denoted as $C_1 \times_{(R,\oplus)} C_2$, is the component $(E, L)$ where $E = E_1 \cup E_2$ and $L$ is defined by

L = \{ \sigma_1 \oplus \sigma_2 \mid \sigma_1 \in L_1,\ \sigma_2 \in L_2,\  (\sigma_1, \sigma_2) \in R(E_1,E_2)\}

Definition <ref> presents a generic composition operator, where composition is parametrized over a composability relation and a composition function.

Let  $\oplus_1$ and $\oplus_2$ be two composition functions on s, and let $R_1$ and $R_2$ be two composability relations on s.

* if $R_1$ is symmetric, then $\times_{(R_1, \oplus_1)}$ is commutative if and only if $\oplus_1$ is commutative;

* if, for all $E_i \subseteq \E$ and $\sigma_i\in \TES{E_i}{\Rp}$ with $i \in \{1,2,3\}$, we have

\begin{align*}
&(\sigma_1, \sigma_2 \oplus_2 \sigma_3) \in R_1(E_1, E_2 \cup E_3) \land (\sigma_2, \sigma_3)\in R_2(E_2, E_3) \iff \\
&(\sigma_1, \sigma_2) \in R_1 (E_1, E_2) \land (\sigma_1 \oplus_1 \sigma_2, \sigma_3) \in R_2 (E_1 \cup E_2, E_3)
\end{align*}

then $\times_{(R_1,\oplus_1)}$ and $\times_{(R_2,\oplus_2)}$ are associative if and only if $\sigma_1 \oplus_1 (\sigma_2 \oplus_2 \sigma_2) = (\sigma_1 \oplus_1 \sigma_2)\oplus_2 \sigma_3$

* if for all $E \subseteq \E$ and $\sigma,\tau \in \TES{E}{\Rp}$, we have $(\sigma, \tau) \in R_1 (E, E) \implies \sigma = \tau$, then $\times_{(R_1,\oplus_1)}$ is idempotent if and only if $\oplus_1$ is idempotent.

The generality of our formalism allows exploration of other kinds of operations on components, such as division.
Intuitively, the division of a component $C_1$ by a component $C_2$ yields a component $C_3$ whose behavior contains all s that can compose with s in the behavior of $C_2$ to yield the s in the behavior of $C_1$.

Let $R$ be a composability relation on s, and $\oplus$ a composition function on s.
The division of two components $C_1 =(E_1, L_1)$ and $C_2 = (E_2, L_2)$ under $R$ and $\oplus$, denoted as $C_1 /_{(R,\oplus)} C_2$, is the component $C = (E_1, L)$ such that:

$$ L = \{ \sigma \in \TES{E_1}{\Rp} \mid \exists \sigma_2 \in L_2.\ (\sigma, \sigma_2) \in R (E_1, E_2) \land \sigma \oplus \sigma_2 \in L_1 \}$$

If the dividend is $C_1 = C'_1 \times_{(R,\oplus)} C'_2$, and the divisor is an operand of the product, e.g., $C_2 = C'_2$, then the behavior of the result of the division, $C$, contains all s in the behavior of the other operand (i.e., $C'_1$) composable with a  in the behavior of $C_2$.

Let $C_1 = (E_1, L_1)$ and $C_2= (E_2, L_2)$ be two components.
Let $(C_1 \times_{(R, \oplus)} C_2) /_{(R, \oplus)} C_2 = (E_3,L_3)$, with $(R,\oplus)$ a pair of a  composability relation and a composition function on s.
$$\{\sigma_1 \in L_1 \mid \exists \sigma_2 \in L_2.\ (\sigma_1,\sigma_2) \in R(E_1 \cup E_2, E_2) \cap R(E_1, E_2)\} \subseteq L_3$$

In the case where $R = \top$ (see Definition <ref>)
then $L_1 \subseteq L_3$.

The results of Section <ref> show a wide variety of product operations that our semantic model offers.
Given a fixed set of components, one can change how components interact by choosing different composability relations and composition functions.
We also give some sufficient conditions for a product operation on components to be associative, commutative, and idempotent, in terms of the algebraic properties of its composability relation and its composition function. Such results are useful to simplify and to prove equivalence between component expressions.

§.§ A co-inductive construction for composition operators

In Section <ref>, we presented a general framework to design components in interaction.
As a result, the same set of components, under different forms of interaction, leads to the creation of alternative systems.
The separation of the composability constraint and the composition operation gives complete control to design different interaction protocols among components.

In this section, we provide a co-inductive construction for composability relations on s.
We show how constraints on observations can be lifted to constraints on s, and give weaker conditions for Lemma <ref> to hold.
The intuition for such construction is that, in some cases, the condition for two s to be composable depends only on a composability relation on observations. An example of composability constraint for a robot with its battery and a field enforces that each move event discharges the battery and changes the state of the field. As a result, every move event observed by the robot must coincide with a discharge event observed by the battery and a change of state observed by the field. The lifting of such composability relation on observations to a constraint on s is defined co-inductively.

A composability relation on observations is a parametrized relation $\kappa$ s.t. for all pairs
$(E_1, E_2) \in \Po(\E) \times \Po(\E) $, we have $\kappa(E_1,E_2) \subseteq (\Po(E_1) \times \Rp) \times (\Po(E_2) \times \Rp)$

Let $\kappa$ be a composability relation on observations, and let $\Phi_\kappa : \Po(\E)^2 \rightarrow (\Po(\TES{\E}{\Rp}^2) \rightarrow \Po(\TES{\E}{\Rp}^2))$ be such that, for any $\Rel \subseteq \TES{\E}{}^2$:

\begin{array}{rl}
\Phi_\kappa(E_1,E_2)(\Rel) = \{(\tau_1, \tau_2) \mid & (\tau_1(0), \tau_2(0)) \in \kappa(E_1,E_2) \land   \\
& (\pr_2(\tau_1)(0) =t_1 \land  \pr_2(\tau_2)(0) =t_2) \land \\
&(t_1 < t_2 \land (\tau_1',\tau_2) \in \Rel \lor t_2 < t_1 \land (\tau_1,\tau_2') \in \Rel \lor  \\
&\ t_2 = t_1 \land (\tau_1',\tau_2') \in \Rel)\}
\end{array}

The lifting of $\kappa$ on s, written $[\kappa]$, is the parametrized relation obtained by taking the fixed point of the function $\Phi_\kappa(E_1, E_2)$ for arbitrary pair $E_1, E_2 \subseteq \E$, i.e., the relation $[\kappa](E_1, E_2) = \bigcup_{\Rel \subseteq \TES{\E}{} \times \TES{\E}{}} \{ \Rel \mid \Rel \subseteq \Phi_\kappa(E_1, E_2)(\Rel)\}$.

For any $E_1, E_2\subseteq \E$, the function $\Phi_\kappa$ is monotone, and therefore has a greatest fixed point.

If $\kappa$ is a composability relation on observations, then the lifting $[\kappa]$  is a composability relation on s.
Moreover, if $\kappa$ is symmetric (as in Definition <ref>), then $[\kappa]$ is symmetric.

See annexe.

As a consequence of Lemma <ref>, any composability relation on observations gives rise to a composability relation on s.
We define three composability relations on s, where Definition <ref> and Definition <ref> are two examples that construct co-inductively the composability relation on s from a composability relation on observations.
For the following definitions, let $C_1 = (E_1, L_1)$ and $C_2 = (E_2, L_2)$ be two components, and $\oplus$ be a composition function on s.

We use $\top$ for the most permissive composability relation on s such that, for any $\sigma, \tau \in \TES{\E}{\Rp}$, we have $(\sigma,\tau) \in \top$.

The behavior of component $C_1 \times_{(\top, \oplus)} C_2$ contains every  obtained from the composition under $\oplus$ of every pair $\sigma_1 \in L_1$ and $\sigma_2 \in L_2$ of s.
This product does not impose any constraint on event occurrences of its operands.

Let $\sqcap \subseteq \Po(\E)^2$ be a relation on observables.
We define two observations to be synchronous under $\sqcap$ according to the following two conditions:

* every observable that can compose (under $\sqcap$) with another observable must occur simultaneously with one of its related observables; and

* only an observable that does not compose (under $\sqcap$) with any other observable can occur independently, i.e., at a different time.

A synchronous composability relation on observations $\kappa_{sync, \sqcap}(E_1,E_2)$ satisfies the two conditions above. For any two observations $(O_i, t_i) \in \Po(E_i) \times \Rp$ with $i \in \{1,2\}$, $((O_1, t_1), (O_2, t_2)) \in \kappa_{sync,\sqcap}(E_1, E_2)$ if and only if:

\begin{array}{ccl}
(t_1 < t_2 & \land & \neg( \exists O_2' \subseteq E_2.\ (O_1, O_2') \in \sqcap)) \  \lor\\
(t_2 < t_1 & \land & \neg( \exists O_1' \subseteq E_1.\ (O_1', O_2) \in \sqcap)) \  \lor\\
t_2 = t_1 & \land &((O_1, O_2) = (O_1' \cup O_1'', O_2' \cup O_2'') \land (O_1',O_2') \in \sqcap \ \land   \\
&       &(( \forall O \subseteq E_2.\ (O_1'', O) \not \in \sqcap) \land \forall O \subseteq E_1.\ (O, O_2'') \not \in \sqcap)\lor (O_1,O_2) = (\emptyset, \emptyset))
\end{array}

Let $E_1 = \{a,b\}$ and $E_2 = \{c,d\}$ with $\sqcap = \{(\{a\},\{c\})\}$.
Thus, $((\{a\}, t_1), (\{d\},t_2)) \in \kappa_{\ssync,\sqcap}$ if and only if $t_2 < t_1$.
Alternatively, we have $((\{a\}, t_1), (\{c\},t_2)) \in \kappa_{\ssync,\sqcap}$ if and only if $t_1 = t_2$.

The lifting $[\kappa_{\ssync,\sqcap}]$ of $\kappa_{\ssync,\sqcap}$, written $\sync$, defines a synchronous composability relation on s.
The behavior of component $C_1 \times_{(\sync, \oplus)} C_2$ contains s obtained from the composition under $\oplus$ of every pair $\sigma_1 \in L_1$ and $\sigma_2 \in L_2$ of s that are related by the synchronous composability relation $\sync$ which, depending on $\sqcap$, may exclude some event occurrences unless they synchronize.
[If we let $\oplus$ be the element wise set union, define an event as a set of port assignments, and in the pair $(\sync, \oplus)$ let $\sqcap$ be true if and only if all common ports get the same value assigned, then this composition operator produces results similar to the composition operation in Reo <cit.>.]

Let $\sqcap \subseteq \Po(\E)^2$ be a relation on observables.
We define two observations to be mutually exclusive under the relation $\sqcap$ if no pair of observables in $\sqcap$ can be observed at the same time.
The mutually exclusive composability relation $\kappa_{\eexcl,\sqcap}$ on observations allows the composition of two observations $(O_1, t_1)$ and $(O_2, t_2)$, i.e., $((O_1, t_1), (O_2, t_2)) \in \kappa_{\eexcl,\sqcap}(E_1, E_2)$, if and only if

(t_1 < t_2) \lor
(t_2 < t_1) \lor
(\neg(O_1 \sqcap O_2) \land t_1 = t_2)

Let $E_1 = \{a,b\}$ and $E_2 = \{c,d\}$ with $\sqcap = \{(\{a\},\{c\})\}$.
Thus, $((\{a\}, t_1), (\{c\},t_2)) \not \in \kappa_{\eexcl,\sqcap}$ for any $t_2 = t_1$, and $\{a\}$ and $\{c\}$ are two mutually exclusive observables.

Similarly as in Example <ref>, the lifting  $[\kappa_{\eexcl,\sqcap}]$ of $\kappa_{\eexcl,\sqcap}$, written  $\excl$, defines a mutual exclusion composability relation on s.
The behavior of component $C_1 \times_{(\nparallel_\sqcap, \oplus)} C_2$ contains s resulting from the composition under $\oplus$ of every pair $\sigma_1 \in L_1$ and $\sigma_2 \in L_2$ of s that are related by the mutual exclusion composability relation $\nparallel_\sqcap$ which, depending on $\sqcap$, may exclude some simultaneous event occurrences.

Composability relations as defined in Definition <ref> and Definition <ref> can be combined to form new relations, and therefore new products.
Let $((\sync) \cap (\excl))(E_1, E_2) = (\sync(E_1, E_2)) \cap (\excl(E_1, E_2))$.
The behavior of component $C_1 \times_{((\sync) \cap (\nparallel_\sqcap), \oplus)} C_2$ contains all s that are in the behavior of $C_1 \times_{(\sync, \oplus)} C_2$ and $C_1 \times_{(\nparallel_\sqcap, \oplus)} C_2$, except those that have observations containing an occurrence of at least one event related by $\sqcap$.

Similarly, we give a mechanism to lift a composition function on observable to a composition function on s.
Such lifting operation interleaves observations with different time stamps, and compose observations that occur at the same time.

Let $+: \Po(\E) \times \Po(\E) \rightarrow \Po(\E)$ be a composition function on observables.
The lifting of $+$ to s is $[+]: \TES{\E}{} \times \TES{\E}{} \rightarrow \TES{\E}{}$ s.t., for $\sigma_i \in \TES{\E}{}$ where $\sigma_i(0) = (O_i, t_i)$ with $i \in \{1,2\}$:

\sigma_1[+]\sigma_2 =
\begin{cases}
\langle \sigma_1(0)\rangle \cdot (\sigma_1'[+] \sigma_2)   &\mathit{if}\ t_1 < t_2 \\
\langle \sigma_2(0)\rangle \cdot (\sigma_1[+] \sigma_2')     &\mathit{if}\ t_2 < t_1 \\
\langle (O_1 + O_2, t_1)\rangle \cdot (\sigma_1'[+] \sigma_2') &  \mathit{otherwise}
\end{cases}

Definition <ref> composes observations only if their time stamp is the same. Alternative definitions might consider time intervals instead of exact times.

Besides the product instances detailed in Definitions <ref>, <ref>,  <ref>, and <ref>, the definition of composability relation or composition function as the lift of some composability relation on observations or function on observables allows weaker sufficient conditions for Lemma <ref> to hold.

Let $+_1$ and $+_2$ be two composition functions on observables and let $\kappa_1$ and $\kappa_2$ be two composability relation on observations.

* $\times_{([\kappa_1], [+_1])}$ is commutative if $\kappa_1$ is symmetric and $+_1$ is commutative;

* $\times_{([\kappa_1],[+_1])}$ and $\times_{([\kappa_2],[+_2])}$ are associative if, for all $E_i \subseteq \E$ and for any triple of observations $o_i = (O_i, t_i) \in \Po(E_i) \times \Rp$ with $i \in \{1,2,3\}$, we have
$(O_1 +_1 O_2)  +_2 O_3 = O_1 +_1 (O_2 +_2 O_3)$

\begin{array}{rl}
&((o_1,o_2) \in \kappa(E_1,E_2)  \land  (\iota_1(o_1,o_2), o_3) \in \kappa(E_1 \cup E_2,E_3)) \iff \\
&((o_2,o_3) \in \kappa(E_2,E_3)  \land (o_1, \iota_2(o_2,o_3)) \in \kappa(E_1 ,E_2 \cup E_3))
\end{array}

$\iota_k((O,t),(P,l)) =
\begin{cases}
(O,t)          &\text{if } t < l \\
(P,l)          &\text{if } l < t \\
(O +_k P, t)  &
\end{cases}
, where $k \in \{1,2\}$.

* $\times_{([\kappa_1],[+_1])}$ is idempotent if $+_1$ is idempotent and, for all $E \subseteq \E$ we have $((O_1,t_1), (O_2, t_2)) \in \kappa_1(E, E) \implies (O_1, t_1) = (O_2, t_2)$.

§.§ Properties

We distinguish two kinds of properties: properties on s that we call trace properties, and properties on sets of s that we call behavior properties, which correspond to hyper-properties in <cit.>.
The generality of our model permits to interchangeably construct a component from a property and extract a property from a component.
As illustrated in Example <ref>, when composed with a set of interacting components, a component property constrains the components to only expose desired behavior (i.e., behavior in the property).
In Section <ref>, we provide more intuition for the practical relevance of these properties.

A trace property $P$ over a set of events $E$ is a subset $P \subseteq \TES{E}{\Rp}$.
A component $C = (E,L)$ satisfies a property $P$, if $L \subseteq P$, which we denote as $C \models P$.

We distinguish the usual safety and liveness properties <cit.>, and recall that every property can be written as the intersection of a safety and a liveness property.
Let $X$ be an arbitrary set, and $P$ be a subset of $\N \rightarrow X$.
Intuitively, $P$ is safe if every bad stream not in $P$ has a finite prefix every completion of which is bad, hence not in $P$.
A property $P$ is a liveness property if every finite sequence in $X^*$ can be completed to yield an infinite sequence in $P$.

For instance, the property of terminating behavior for a component with interface $E$ is a liveness property, defined as:

P_{\mathit{finite}}(E) = \{ \sigma \in \TES{E}{\Rp} \mid \exists n \in \mathbb{N}. \forall i > n.\ \pr_1(\sigma)(i) = \emptyset \}

$P_{\mathit{finite}}(E)$ says that, for every finite prefix of any stream in $\TES{E}{\Rp}$, there exists a completion of that prefix with an infinite sequence of silent observations $\emptyset$ in $P_{\mathit{finite}}(E)$.

A trace property is similar to a component, since it describes a set of s, except that it is a priori not restricted to any interface.
A trace property $P$ can then be turned into a component, by constructing the smallest interface $E_P$ such that, for all $\sigma \in P$, and $i \in \mathbb{N}$, $\pr_1(\sigma)(i) \subseteq E_P$.
The component $C_P = (E_P, P)$ is then the componentized-version of property $P$.

Let $E$ be a set of events, and let $\sqcap$ be the smallest relation such that for all non empty $O \subseteq E$, $(O,O) \in \sqcap$.
Given a property $P$ over $E$, its componentized-version $C_P$ (see Example <ref>), the product $\sync$ as in Definition <ref>, and a component $C = (E,L)$, then $C \models P$ if and only if $C \times_{(\sync, [\cup])} C_P = C$.

We use the term coordination property to refer to a property used in order to coordinate behaviors.
Given a set of $n$ components $C_i = (E_i, L_i)$, $i \in \{1, ..., n\}$, a coordination property $\Coord$ ranges over the set of events $E = E_1 \cup ... \cup E_n$, i.e., $\Coord \subseteq \TES{E}{\Rp}$.

Consider the synchronous interaction of the $n$ components, with  $\sqcap$ a symmetric relation on observables, $\oplus$ an associative and commutative composition function on s, and let $C = ((C_1 \times_{(\sync, \oplus)} C_2) ... \times_{(\sync, \oplus)} C_n)$ be their synchronous product.

Typically, a coordination property will not necessarily be satisfied by the composite component $C$, but some of the behavior of $C$ is contained in the coordination property.
The coordination problem is to find (e.g., synthesize) an orchestrator component $\Orch = (E_O,L_O)$ such that $C \times_{(\sync, \oplus)} \Orch \models \Coord$.
The orchestrator restricts the component $C$ to exhibit only the subset of its behavior that satisfies the coordination property.
In other words, in their composition, $\Orch$ coordinates $C$ to satisfy $\Coord$.
The coordination problem can be made even more granular by changing the composability relations or the composition functions used in the construction of $C$.

As shown in Example <ref>, since $\Coord$ ranges over the same set $E$ that is the interface of component $((C_1 \times_{(\sync, \oplus)} C_2) ... \times_{(\sync, \oplus)} C_n)$, a coordination property can be turned into an orchestrator by building its corresponding component.

Trace properties are not sufficient to fully capture the scope of interesting properties of components and cyber-physical systems. Some of their limitations are highlighted in Section <ref>. To address this issue, we introduce behavior properties, which are strictly more expressive than trace properties, and give two illustrative examples.

A behavior property $\phi$ over a set of events $E$ is a hyper-property $\phi \subseteq \Po(\TES{E}{\Rp})$.
A component $C = (E,L)$ satisfies a hyper-property $\phi$ if $L \in \phi$, which we denote as $C \mmodels \phi$.

A component $C = (E,L)$ can be oblivious to time, as in Example <ref>.
Any sequence of time-stamps for an acceptable sequence of observables is acceptable in the behavior of such a component. This “obliviousness to time" property is not a trace property, but a hyper-property, defined as:

\phi_{\shift}(E) := \{ Q \subseteq \TES{E}{\Rp} \mid \forall \sigma \in Q.  \forall t \in OS(\Rp). \exists \tau \in Q.
\pr_1(\sigma) = \pr_1(\tau) \land \pr_2(\tau) = t\}

Intuitively, if $C \mmodels \phi_{\shift}(E)$, then $C$ is independent of time.

We use $\phi_{\iinsert}(X, E)$ to denote the hyper-property that allows for arbitrary insertion of observations in $X \subseteq \Po(E)$ into every  at any point in time, i.e., the set defined as:

\begin{array}{rlcccccc}
\{ Q \subseteq \TES{E}{\Rp} \mid \forall \sigma \in Q.  \forall i \in \mathbb{N}. \exists \tau \in Q.
\exists x \in X. (\forall&\hspace{-0.2em} j < i.     & \sigma(j) &=& \tau(j)) &\land \\
(\exists&\hspace{-0.2em} t \in \Rp. & \tau(i)   &=& (x,t))   &\land \\
(\forall&\hspace{-0.2em} j \geq i.      & \tau(j+1) &=& \sigma(j))& \}
\end{array}

Intuitively, elements of $\phi_{\iinsert}(X,E)$ are closed under insertion of an observation $O \subseteq X $ at an arbitrary time.
We show in Section <ref> how we use this closure property to design cyber-physical components.

§ APPLICATION

This section is inspired by the work on soft-agents <cit.>,
and elaborates on the more intuitive version this work presented in Section <ref>.
We show in Sections <ref> and  <ref> some expressions that represent interactive cyber-physical systems, and in Section <ref> we formulate some trace and behavior properties of those systems.
Through this example, we show the details of how we use component based descriptions to model a simple scenario of a robot roaming around in a field while taking energy from its battery.
We structurally separate the battery, the robot, and the field as independent components, and we explicitly model their interaction in a specific composed system.

§.§ Description of components

We give, in order, a description for a robot, a battery, and a field component.
Each component reflects a local and concise view of the physical and cyber aspects of the system.

Robot. A robot component $R$ is a tuple $(E_R,L_R)$ with:

\begin{array}{rll}
E_R &= \{(\rread(&\hspace{-0.7em}\loc,R); l), (\rread(\bat,R); b), (\move(R);(d, \alpha)), (\charge(R); s) \mid \\
&                                             &l \in [0,20]^2,\ b \in \Rp,\
d \in \{\No, \Ea, \We, \So \},\ \alpha \in \Rp,\ s \in \{\ON,\OFF\}\}\\
L_R &= \{\sigma \in &\hspace{-1.7em}\mathit{TES}(E_R) \mid \forall i \in \N. \exists e \in E_R.\ \pr_1(\sigma)(i) = \{e\}  \}
\end{array}

where the read of the position, the read of the battery, the move, and the charge events contain respectively the position of the robot as a pair of coordinates $l\in[0,20]^2$ grid; the remaining battery power $b$ (in Wh); the move direction as pair of a cardinal direction $d$ and a positive number $\alpha$ for a demand of energy (in ); and the charge status $s$ as $\ON$ or $\OFF$.
Note that the set of TESs $L_R$ allows for arbitrary increasing and non-Zeno sequences of timestamp.

Battery. A battery component $B(C)$ with capacity $C$ (in Wh) is a tuple $(E_B, L_B)$ with:

\begin{align*}
E_B &= \{ (\rread(B); l), (\discharge(B); \eta_d), (\charge(B); \eta_c) \mid  0 \leq l \leq C,\ \eta_c, \eta_d: \Rp \rightarrow \Rp\}\\
L_B &= \{ \sigma \in \TES{E_B}{\Rp} \mid \forall i \in \N. \exists e \in E_B.\ \pr_1(\sigma)(i) = \{e\} \land P_{B}(\sigma) \}
\end{align*}

where the read, the charge, and the discharge events respectively contain the current charge status $l$ (in Wh), the discharge rate $\eta_d$, and the charge rate $\eta_c$.
The discharge and charge rates are coefficients that depend on the internal constitution of the battery, e.g., its current and voltage, and influence how the battery supplies energy to its user. The integration of $\eta_d$ (or $\eta_c$) on a time interval gives the power delivered (or received) by the battery in Wh.
The predicate $P_{B}(\sigma)$ guarantees that every behavior $\sigma$ of the battery satisfies the physical constraints for its acceptability.
An example for the structural constraint $P_{B}$ is that every $\rread$ event instance returns the battery level as a function of the occurrence of prior $\discharge$ and $\charge$ events.
We introduce the $lev$ function, that takes a sequence of observations $s \in (\Po(\E) \times\Rp)^*$ of size $i > 1$ and returns the cumulative energy spent: $lev(s) = lev(\langle s(0),s(1)\rangle) + lev(\langle s(1) ...s(i)\rangle)$, where

lev(\langle (O_1, t_1), (O_2, t_2)\rangle) =
\begin{cases}
\int_{t_1}^{t_2}(\eta_d(t) +\eta_I(t))dt &\ if\ (\discharge(B);\eta_d) \in O_1 \\
\int_{t_1}^{t_2}(\eta_I(t) - \eta_c(t)) dt&\ if\ (\charge(B);\eta_c) \in O_1 \\
\int_{t_1}^{t_2}\eta_I(t) dt &\ otherwise
\end{cases}

and $\eta_I$ is an internal discharge rate.
The constraint $P_B$ is defined such that all $(\rread(B);l)$ events in $E_B$ return the current battery level of the robot, in accordance with the $lev$ function, i.e., for all $\sigma \in L_B$:

\begin{align*}
\forall i \in \mathbb{N}.  &(\rread(B);l) \in \pr_1(\sigma)(i) \implies l = \min(C, \max(C - lev(\langle \sigma(0), ..., \sigma(i)\rangle), 0))
\end{align*}

where $C$ is the maximum capacity of the battery.
The property $P_B$ assumes that initially at $t=0$ the battery is at its maximum charge $C$, that the battery level decreases after each discharge event, increases after each charge event, proportionally to the discharge and the charge rates. Moreover, a discharge below $0$ is physically forbidden.
Observe that different alternatives for the predicate $P_{B}$ account for different models of batteries.
Moreover, our model allows for specifications where the discharge factor depends on external parameters (temperature, discharge level, etc), adding a non-linear aspect to the model.

Field. A field component $F(l_0)$ contains a single object that we identify as $I$ initially at location $l_0$, has a fixed size of $[0,20]^2$, and contains a charging station at location $(5;5)$.
A field component is a tuple  $(E_F, L_F)$ with:

\begin{align*}
E_F &= \{ (\loc(I);p), (\move(I);(d,F))  \mid  p \in [0,20]^2,\ d \in \{\No, \So, \Ea, \We\},\
F_t \in \Rp\}\\
L_F &= \{ \sigma \in \TES{E_F}{\Rp} \mid  \forall i \in \N. \exists e \in E_F.\ \pr_1(\sigma)(i) = \{e\} \land P_F(\sigma) \}
\end{align*}

where the $\loc$ and the $\move$ events respectively contain the position of object $I$ and the pair of a direction $d$ of the move of object $I$ and a force $F_t$ of traction applied by object $I$.
A field has an internal friction factor $\mu$ whose value depends on the position on the field.
With a friction value of $0$, the object will have no traction and thus will stay put in place instead of moving on the field (e.g., failure to move on a layer of ice). With a friction of $1$, the move event will displace the object proportionally to the force of the move (e.g., a move on a layer of concrete). A friction factor between $0$ and $1$ captures other scenarios between those two extremes (e.g., a move on a layer of grass).
The predicate $P_F(\sigma)$ guarantees that every behavior $\sigma$ satisfies the physics of the field component.
$P_F$ models the case where the object $I$ is initially at position $l_0$ and every move event changes continuously the location of the object on the field according to the direction $d$, the force of traction $F_t$, and the friction $\mu$. A move event has no effect if it occurs while the position of $I$ is on the boundary of the field: this scenario simulates the case of a fenced field, where moving against the fence has the same observable as not moving.

The internal constraints of the field are such that the $\move$ observation triggers an internal displacement of object $I$ proportional to the force that the object has applied.
We write $\Delta d(t,t_0, (x_0,y_0))$ to denote the displacement from a time $t_0$ where the object is at rest at position $(x_0,y_0)$, to a time $t$, defined as:

\begin{align}
m\vec{a} &= \vec{F_t}\notag\\
ma &=  F_t\notag\\
v(t,t_0) &=  (\cfrac{F_t}{m})(t - t_0) \notag\\
\Delta d(t,t_0,(x_0,y_0)) &=  \cfrac{1}{2}(\cfrac{F_t}{m})(t - t_0)^2
\end{align}

where $||\vec{F_t}|| \leq \cfrac{1}{4}\ \mu m g$, e.g., the traction force on a wheel (supporting one fourth of the weight of the object) is less than the maximal friction force, with $\mu$ the friction coefficient, $m$ the mass of the object; and $F_t$ is the constant traction force of the object.
Observe that we chose to make the friction coefficient dependent on the initial position $x_0$ of the object before the move. This choice reflects the simplifying assumption that the friction will not substantially change during the movement.
Alternatively, one can imagine a different structure for the field component to support variable friction during a move in $P_F$.

An example for the constraint $P_{F}$ reflects the constraint that for each sequence of observations, the output value of a $read$ event corresponds to the current position of the robot given its previous moves.
We will use a function called $\dis$ to determine the cumulative displacement of the robot after a sequence of observations.
Let $s \in (\Po(\E)\times \Rp)^*$ be a finite sequence of observations of size $i>1$. The displacement of the object $I$, at position $(x_0,y_0)$, after a sequence of events $s$ is given by $\dis(\langle(O_0,t_0)\rangle, (x_0,y_0)) = (x_0,y_0)$ and $\dis(s,(x_0,y_0)) = \dis(\langle s(1),...,s(i)\rangle, (x', y'))$, where for $s(0) = (O_0,t_0)$ and $s(1) = (O_1, t_1)$:

(x',y') =
\begin{cases}
(x_0,y_0+\Delta d(t_1,t_0, (x_0,y_0)))   &\  if\ (\move(I); (\No,F_t)) \in O_0 \\
(x_0,y_0-\Delta d(t_1, t_0,(x_0,y_0))) &\  if\ (\move(I); (\So, F_t)) \in O_0 \\
(x_0+\Delta d(t_1, t_0,(x_0,y_0)),y_0)  &\  if\ (\move(I); (\Ea,F_t)) \in O_0 \\
(x_0-\Delta d(t_1, t_0,(x_0,y_0)),y_0) &\  if\ (\move(I); (\We, F_t)) \in O_0  \\
(x_0,y_0) &\ otherwise
\end{cases}

with $\Delta d(t,t_0,(x_0,y_0))$ defined in Equation (1).
$P_F$ is defined to accept all s such that every $\rread$ event returns the current position of the robot on the field, according to its displacement over time.
Given $\sigma \in \TES{E_F}{}$, $P_F(\sigma)$ is true if and only if

\begin{array}{rl}
\forall i \in \N.&  (\loc(I);p) \in \pr_1(\sigma)(i) \implies p = |\dis(\langle \sigma(0) .... \sigma(i)\rangle, l_0)|_{[-20,20]}
\end{array}

|(x,y)|_{[-20,20]} = (\min(\max(x,-20),20), \min(\max(y,-20),20))
$, and $l_0$ the initial position of object $I$.
$P_F$ models the case where the robot starts in position $l_0$ and every move event changes the location of the robot on the field.

Robots $R_1$ and $R_2$ are two instances of the robot component, where all occurrences of $R$ have been renamed respectively to $R_1$ and $R_2$ (e.g., $(\rread(\loc,R),l)$ becomes $(\rread(\loc,R_1),l)$ for the robot instance $R_1$, etc.).
Similarly, we consider $B_1$ and $B_2$ to be two instances of the battery component $B$, and $F_1((0;0))$ and $F_2((5;0))$ to be two instances of the field component $F$ parametrized by the initial location for the object $I$, where the objects in fields $F_1$ and $F_2$ are renamed to $I_1$ and $I_2$, and respectively initialized at position $(0;0)$ and $(5;0)$.

§.§ Interaction

We detail three points of interactions on observables among a robot and its battery, a robot and a field on which it moves, and two instances of a field component.
The composability relations that relate the events of a robot, a battery, and a field impose some necessary constraints for the physical consistency of the cyber-physical system. For instance, that the power requested by the robot must match the characteristic of the battery.

Interactions between a robot component and its battery are such that, for instance, every occurrence of a move event at the robot component must be simultaneous with a discharge event of the battery, with the discharge factor proportional to the demand of energy from the robot.
Given a robot component $R$ and a battery component $B$, we define the symmetric relation $\sqcap_{RB}$ on the set $\Po(E_R \cup E_B)$ to be the smallest relation such that:

\begin{array}{rcll}
\{(\rread(\bat,R);b)\} &\sqcap_{RB}& \{(\rread(B);b)       \} &\text{ for all } 0 \leq b \leq C \\
\hspace{-0.4em}\{(\move(R);(d,\alpha))      \} &\sqcap_{RB}& \{(\discharge(B);\eta_d)\} &\text{ for all }d \in \hspace{-0.2em}\{\No,\So,\We,\Ea\} \\
\hspace{-0.2em}\{(\charge(R);\ON)  \} &\sqcap_{RB}& \{(\charge(B);\eta_c)   \} &
\end{array}

with $\eta_d(t) > \alpha$ for all $t \in \Rp$, e.g, the power delivered by the battery during a discharge is greater than the power required by the move; and $C$ is the maximal battery capacity.

Robot-field. Interactions between a robot component and a field component are such that, for instance, every move event of the robot component must be simultaneous with a move event of the object $I$ on the field, with a variable friction coefficient.
Given a robot component $R$ and a field component $F$, we define the symmetric relation $\sqcap_{RF}$ on the set $\Po(E_R \cup E_F)$ to be the smallest relation such that:

\begin{array}{rcll}
\{(\rread(\loc,R);l) \} &\sqcap_{FR}& \{(\loc(I);l)      \} &\text{ for all }l \in [0,20]^2 \\
\{(\move(R);(d,\alpha))       \} &\sqcap_{FR}& \{(\move(I);(d,F_t))     \} &\text{ for all }d \in \{\No,\We,\Ea,\So\}, v \in \Rp\\
\{(\charge(R); \ON)  \} &\sqcap_{FR}& \{(\loc(I);(5,5))  \} &
\end{array}

with $F_t = \cfrac{\alpha}{R\omega}$ with $R$ the radius of the wheels of the robot and $\omega$ the speed of rotation of the wheels (assumed to be constant during the move).
Observe that a robot can charge only if it is located at the charging station.

We add also interaction constraints between two fields, such that no observation can gather two read events containing the same position value.
Thus, given two fields $F_1$ and $F_2$, let $\sqcap_{F_{12}}$ be the smallest symmetric mutual exclusion relation on the set $\Po(E_{F_1} \cup E_{F_2})$ such that:

\{(\loc(I_1);l)\} \sqcap_{F_{12}} \{(\loc(I_2);l)\} \text{ for all }l \in [0,20]^2.

Observe that we interpret $\sqcap_{F_{12}}$ as a mutual exclusion relation.

Product. We use set union as a composition function on observables: given two observables $O_1$ and $O_2$, we define $O_1 \oplus O_2$ to be the observable $O_1 \cup O_2$.
We use the synchronous and mutual exclusion composability relations on s introduced in Definition <ref> and Definition <ref>.
We represent the cyber-physical system consisting of two robots $R_1$ and $R_2$ with two private batteries $B_1$ and $B_2$, and individual fields $F_1$ and $F_2$, as the expression:

\begin{equation}\label{eq:cps}
\times_{(\bowtie_{\sqcap_{FR_{12}}}, [\cup])}
\times_{(\top, [\cup])}
\end{equation}

where $F_1F_2 := (F_1 \times_{(\nparallel_{\sqcap_{F_{12}}},[\cup])}F_2)$, $
R_iB_i := (R_i \times_{(\bowtie_{\sqcap_{R_iB_i}}, [\cup])} B_i)
$, and $\sqcap_{FR_{12}} := {(\sqcap_{F_1R_1} \cup \sqcap_{F_2R_2})}$,  with $i \in \{1,2\}$.

Note that the previous expression describes the same component as:

\times_{(\nparallel_{\sqcap_{F_{12}}},[\cup])}

where $F_iR_iB_i := F_i \times_{(\bowtie_{\sqcap_{F_iR_i}}, [\cup])} R_i \times_{(\bowtie_{\sqcap_{R_iB_i}}, [\cup])} B_i$ with $i \in \{1,2\}$.

§.§ Properties

Let $E = E_{R_1} \cup E_{R_2} \cup E_{B_1} \cup E_{B_2} \cup E_{F_1} \cup E_{F_2}$ be the set of events for the composite system in Equation <ref>.
We formulate the scenarios described in Section <ref> in terms of a satisfaction problem involving a safety property on s and a behavior property on the composite system.
We first consider two safety properties:

P_{\energy} = \{ \sigma \in \TES{E}{\Rp} \mid \forall i \in \mathbb{N}. \{(\rread(B_1),0), (\rread(B_2),0)\} \cap \pr_1(\sigma)(i) = \emptyset \}

P_{\nooverlap} = \{ \sigma \in \TES{E}{\Rp} \mid \forall i \in \mathbb{N}. \forall l \in [0,20]^2, \{ (\loc(I_1),l), (\loc(I_2),l) \} \nsubseteq  \pr_1(\sigma)(i) \}

The property $P_{\energy}$ collects all behaviors that never observe a battery value of $0\si{Wh}$.
The property $P_{\nooverlap}$ describes all behaviors where the two robots are never observed together at the same location.
Observe that, while both $P_{\energy}$ and $P_{\nooverlap}$ specify some safety properties, they are not sufficient to ensure the safety of the system.
We illustrate some scenarios with the property $P_{\energy}$.
If a component never reads its battery level, then the property $P_{\energy}$ is trivially satisfied, although effectively the battery may run out of energy.
Also, if a component reads its battery level periodically, each of its readings may return an observation agreeing with the property. However, in between two read events, the battery may run out of energy (and somehow recharge).
To circumvent those unsafe scenarios, we add an additional hyper-property.

Let $X_{\rread} = \{ (\rread(B_1);l_1), (\rread(B_2);l_2) \mid 0 \leq l_1 \leq C_1,\ 0 \leq l_2 \leq C_2 \}$ be the set of reading events for battery components $B_1$ and $B_2$, with maximal charge $C_1$ and $C_2$ respectively. The property
\phi_{\mathit{insert}}(X_{\rread}, E)
$, as detailed in Example <ref>, defines a class of component behaviors that are closed under insertion of $\rread$ events for the battery component.
Therefore, the system denoted as $C$, defined in Equation <ref> is energy safe if $C \models P_{\energy}$ and its behavior is closed under insertion of battery read events, i.e., $C \mmodels \phi_{\mathit{insert}}(X_{\rread}, E)$.
In that case, every run of the system is part of a set that is closed under insertion, which means all read events that the robot may do in between two events observe a battery level greater than $0\si{Wh}$.
The behavior property enforces the following safety principle: had there been a violating behavior (i.e., a run where the battery has no energy), then an underlying  would have observed it, and hence the hyperproperty would have been violated.

Another scenario for the two robots is to consider their coordination in order to have them swap their positions. Let $F_1$ be initialized to have object $I_1$ at position $(0,0)$ and $F_2$ have $I_2$ at position $(5,0)$. The property of position swapping is a liveness property defined as:

P_{swap} = \{ \sigma \in \TES{E}{\Rp} \mid \exists i \in \mathbb{N}. \{ (\loc(I_1),(5,0)), (\loc(I_2),(0,0)) \} \subseteq \sigma(i) \}

It is sufficient for a liveness property to be satisfied for the system to be live. However, it may be that the two robots swap their positions before the actual observation happens. In that case, using a similar hyper-property as for safety property will make sure that if there exists a behavior where robots swap their positions, then such behavior is observed  as soon as it happens.

§ RELATED AND FUTURE WORK

Our work offers a component-based semantics for cyber-physical systems <cit.>. In <cit.>, a similar aim is pursued by defining an algebra of components using interface theory. Our component-based approach is inspired by <cit.>, where a component exhibits its behavior as a set of infinite timed-data streams.
More details about co-algebraic techniques to prove component equivalences can be found in <cit.>.

In <cit.>, the authors describe an algebra of timed machines and of networks of timed machines.
A timed machine is a state based description of a set of timed traces, such that every observation has a time stamp that is a multiple of a time step $\delta$.

The work provides some decidability results on feasibility and consistency of networks of timed machines.

The work differs from our current development in several respects.
We focus in this paper on different algebraic operations on sets of timed-traces (TESs), and abstract away any underlying operational model (e.g., timed-automata).
In <cit.>, the authors explain how algebraic operations on timed machines approximate the intersection of sets of timed-traces.
In our case, interaction is not restricted to input/output composition, but depends on the choice of a composability constraint on s and a composition function on observables.
The work in <cit.> denotes an interesting class of components (closed under insertion of silent observation - $r$-closed) that deserves investigation.

Cyber-physical systems have also been studied from an actor perspective, where actors interact through events <cit.>. Problems of building synchronous protocols on top of asynchronous means of interaction are presented in <cit.>.

In <cit.> a multiset rewriting model of time
sensitive distributed systems such as cyber-physical agent, is
introduced. Two verification problems are defined relative to a given
property P: realizability (is there a trace that satisfies P), and
survivability (do all traces satisfy P) and the complexity is analyzed.
In <cit.> the theory is extended with two further
properties that concern the ability to avoid reaching a bad state.

Recent work has shown plenty of interest in studying the satisfaction problem of hyper-properties and the synthesis of reactive systems <cit.>. Some works focus more particularly on using hyper-properties for cyber-physical design <cit.>.

The extension of hybrid automata <cit.> into a quantized hybrid automata is presented in <cit.>, where the authors apply their model to give a formal semantics for data flow models of cyber-physical systems such as Simulink.

Compared to formalisms that model cyber-physical systems as more concrete operational or state-based mechanisms, such as automata or abstract machines, our more general abstract formalism is based only on the observable behavior of cyber-physical components and their composition into systems, regardless of what more concrete models or mechanisms may produce such behavior.

For future work, we want to provide a finite description for components, and use our current formalism as its formal semantics.
In fact, we first started to model interactive cyber-physical systems as a set of finite state automata in composition, but the underlying complexity of automata interaction led us to introduce a more abstract component model to clarify the semantics of those interactions.
Moreover, we want to investigate several proof techniques to show equivalences of components. We expect to be able to reason about local and global coordination, by studying how coordinators distribute over our different composition operators.
Finally, our current work
serves as a basis for defining a compositional semantics for a state-based component framework <cit.> written
in Maude <cit.>, a programming language based on rewriting logic. We will focus on evaluating the robustness of a set of components with respect to system requirements expressed as trace or hyper-properties. The complexity of the satisfaction problem requires some run-time techniques to detect deviations and produce meaningful diagnosis <cit.>, a topic that we are currently exploring.

§ CONCLUSION

This paper contains three main contributions. First, we introduce a component model for cyber-physical systems where cyber and physical processes are uniformly described in terms of sequences of observations.
Second, we provide ways to express interaction among components using algebraic operations, such as a parametric product and division, and
give conditions under which product is associative,
commutative, or idempotent.
Third, we provide a formal basis to study trace and hyper-properties of components, and demonstrate the application of our work in an example describing several coordination problems.

The expressiveness of our semantic model provides a formal grounds to design interacting cyber-physical systems, where interaction is defined explicitly and exogenously as an algebraic operation acting on components.
As a future step, we plan to use the semantic model introduced in this work to give a compositional semantics for interacting (state-based) specification for cyber-physical components.
We aim to use our modular design in order to study problems of diagnosis in systems of interacting cyber-physical components.

Talcott was partially supported by the U. S. Office of Naval Research under award numbers N00014-15-1-2202 and N00014-20-1-2644, and NRL grant N0017317-1-G002.
Arbab was partially supported by the U. S. Office of Naval Research under award number N00014-20-1-2644.