1 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 CyberPhysical 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 cybercyber, cyberphysical, and physicalphysical pairs of modules; and (3) when to use which formalism to express composition and interactions of hybrid cyberphysical 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 [AR03] 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 cyberphysical 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 cyberphysical systems [LML06, TSSL13], time data streams for connectors [AR03]), 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, inputoutput 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 cyberphysical 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 [AR03] in that it explicitly and directly expresses synchronous occurrences of events. Like the one in [AR03] 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 lockstep 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 cyberphysical 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 [CS10]. We show, for instance, how the energy adequacy property in a cyberphysical system requires both a behavioral property and a trace property.
Contribution

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 coinductive 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 2. We provide in Section 3 formal definitions for components, their composition, and their properties. We describe a detailed example in Section LABEL:section:formalexample. We present some related and our future work in Section LABEL:section:relatedwork, and conclude the paper in Section LABEL:section:conclusion.
2 Coordination of energyconstrained robots on a field
In this work, we consider a cyberphysical system as a set of interacting processes. Whether a process consists of a physical phenomenon (sun rising, electrochemical reaction, etc.) or a cyber phenomenon (computation of a function, message exchanges, etc.), it exhibits an externally observable behavior resulting from some internal nonvisible 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 sunrise or the temperature reading of 5. An event occurs at a point in time, yielding an event occurrence (e.g., the sunrise event occurred at 6:28 am today), and the same event can occur repeatedly at different times (the sunrise 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 of a set of observable events together with its timestamp represents an observation. An observation in fact consists of a set of event occurrences: occurrences of events in at the same time . We call an infinite sequence of observations a TimedEvent 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 timedevent 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 , has two kinds of events: a read event that measures the level of its battery or that obtains its position , and a move event when the robot moves in the direction with energy (in ). The TES in the Robot column in Table 2 shows a scenario where robot reads its location and gets the value at time , then moves north with 20 at time , reads its location and gets at time , and reads its battery value and gets at time , ….
A battery component, with identifier , has three kinds of events: a charge event , a discharge event , and a read event , where and are respectively the discharge and charge rates of the battery, and is the current charge status. The TES in the Battery column in Table 2 shows a scenario where the battery discharged at a rate of at time , and reported its chargelevel of at time , ….
Robot ()  Battery ()  Field () 


{(discharge(B);20)}  {(move(I);(N,40))}  R(2)∪B(2)∪F(2)  
A field component, with identifier , has two kinds of events: a position event that obtains the position of an object , and a move event of the object in the direction with traction force (in ). The TES in the Field column in Table 2 shows a scenario where the field has the object at location at time , then the object moves in the north direction with a traction force of 40 at time , subsequently to which the object is at location at time , ….
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 robotbattery 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 robotfield 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 TES for the composite RobotBatteryField system collects, in sequence, all observations from a TES in a Robot, a Battery, and a Field component behavior, such that at any moment the interaction constraints are satisfied. The column RobotBatteryField in Table
2 displays the first elements of such a TES.3 Components, composition, and properties
Each lemma of the section has its proof in the technical report [LAT21].
3.1 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 temperaturereading event, each of which has the internal structure of a namevalue 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.
Notation 1 (Events).
We use to denote the universal set of events.
An observable is a set of event occurrences that happen together and an observation is a pair of an observable and a timestamp .^{1}^{1}1Any totally ordered dense set would be suitable as the domain for time (e.g., positive rationals ). For simplicity, we use , the set of real numbers for this purpose. An observation represents an act of atomically observing occurrences of events in at time . Atomically observing occurrences of events in at time means there exists a small such that during the time interval :

every event is observed exactly once^{2}^{2}2A finer time granularity may reveal some ordering relation on the occurrence of events in the same set of observation., and

no event is observed.
We write to denote a finite sequence of size of elements over an arbitrary set , where for . The set of all finite sequences of elements in is denoted as . A stream^{3}^{3}3The set denotes the set of natural numbers . over a domain is a function . We use to represent the element of , and given a finite sequence , we write to denote the stream such that for and for . We use to denote the derivative of , such that for all .
A TimedEvent Stream (TES) over a set of events and a set of timestamps is a stream where, for :

for every , [i.e., time monotonically increases] and

for every , there exists such that [i.e., time is nonZeno progressive].
Notation 2 (Time stream).
We use to refer to the set of all monotonically increasing and nonZeno infinite sequences of elements in .
Notation 3 (TimedEvent Stream).
We use to denote the set of all TESs whose observables are subsets of the event set with elements in as their timestamps.
Given a sequence , we use the projections and to denote respectively the sequence of observables and the sequence of time stamps .
3.2 Components
The design of complex systems becomes simpler if such systems can be decomposed into smaller subsystems that interact with each other. In order to simplify the design of cyberphysical 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 TESs) and an interface (set of events).
Like existing semantic models, such as timedata streams [AR03], time signal [TSSL13], or discrete clock [FLDL18], 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 allornothing transaction.
Definition 1 (Component).
A component is a tuple where is a set of events, and is a set of TESs. We call the interface and the externally observable behavior of .
More particularly, Definition 1 makes no distinction between cyber and physical components. We use the following examples to describe some cyber and physical aspects of components.
Example 1.
Consider a set of two events , and restrict our observations to and . A component whose behavior contains TESs with alternating observations of and is defined by the tuple where L = { σ∈TES(E) ∣∀i ∈N.(pr1(σ)(i) = {0} ⟹pr1(σ)(i+1) = {1}) ∧(pr1(σ)(i) = {1} ⟹pr1(σ)(i+1) = {0}) } Note that this component is oblivious to time, and any stream of monotonically increasing nonZeno real numbers would serve as a valid stream of time stamps for any such sequence of observations.
Example 2.
Consider a component encapsulating a continuous function , where is a set of initial values, and is the codomain of values for . Such a function can describe the evolution of a physical system over time, where means that at time the state of the system is described by the value if initialized with . We define the set of all events for this component as the range of function given an initial parameter . The component is then defined as the pair such that: Lf = { σ∈TES(D) ∣∃d0 ∈D0. ∀i ∈N. pr1(σ)(i) = {f(d0,pr2(σ)(i))} } Observe that the behavior of this component contains all possible discrete samplings of the function at monotonically increasing and nonZeno sequences of time stamp. Different instances of would account for various cyber and physical aspects of components.
3.3 Composition
A complex system typically consists of multiple components that interact with each other. The example in Section 2 shows three components, a , a , and a , 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^{4}^{4}4Also 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.
Definition 2 (Composability relation on TESs).
A composability relation is a parametrized relation such that for all , we have .
Definition 3 (Symmetry).
A parametrized relation is symmetric if, for all and for all : .
A composability relation on TESs serves as a necessary constraint for two TESs to compose. We give in Section 3.4 some examples of useful composability relations on TESs that, e.g., enforce synchronization or mutual exclusion of observables. We define composition of TESs as the act of forming a new TES out of two TESs.
Definition 4.
A composition function on TES is a function .
We define a binary product operation on components, parametrized by a composability relation and a composition function on TESs, 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 TESs in the behavior of its operands deemed composable by the composability relation.
Definition 5 (Product).
Let be a pair of a composition function and a composability relation on TESs, and , , two components. The product of and , under and , denoted as , is the component where and is defined by L = { σ1 ⊕σ2 ∣σ1 ∈L1, σ2 ∈L2, (σ1, σ2) ∈R(E1,E2)}
Definition 5 presents a generic composition operator, where composition is parametrized over a composability relation and a composition function.
Lemma 1.
Let and be two composition functions on TESs, and let and be two composability relations on TESs. Then:

if is symmetric, then is commutative if and only if is commutative;

if, for all and with , we have
then and are associative if and only if

if for all and , we have , then is idempotent if and only if 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 by a component yields a component whose behavior contains all TESs that can compose with TESs in the behavior of to yield the TESs in the behavior of .
Definition 6 (Division).
Let be a composability relation on TESs, and a composition function on TESs. The division of two components and under and , denoted as , is the component such that: L = { σ∈TES(E1) ∣∃σ2 ∈L2. (σ, σ2) ∈R (E1, E2) ∧σ⊕σ2 ∈L1 }
If the dividend is , and the divisor is an operand of the product, e.g., , then the behavior of the result of the division, , contains all TESs in the behavior of the other operand (i.e., ) composable with a TES in the behavior of .
Lemma 2.
Let and be two components. Let , with a pair of a composability relation and a composition function on TESs. Then, {σ1 ∈L1 ∣∃σ2 ∈L2. (σ1,σ2) ∈R(E1 ∪E2, E2) ∩R(E1, E2)} ⊆L3
Corollary 1.
In the case where (see Definition 9) then .
The results of Section 3.3 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.
3.4 A coinductive construction for composition operators
In Section 3.3, 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 coinductive construction for composability relations on TESs. We show how constraints on observations can be lifted to constraints on TESs, and give weaker conditions for Lemma 1 to hold. The intuition for such construction is that, in some cases, the condition for two TESs 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 TESs is defined coinductively.
Definition 7 (Composability relation).
A composability relation on observations is a parametrized relation s.t. for all pairs , we have
Definition 8 (Lifting composability relation).
Let be a composability relation on observations, and let be such that, for any : Φκ(E1,E2)(R) = {(τ1, τ2) ∣(τ1(0), τ2(0)) ∈κ(E1,E2) ∧(pr2(τ1)(0) =t1 ∧pr2(τ2)(0) =t2) ∧(t1 ¡ t2 ∧(τ1’,τ2) ∈R∨t2 ¡ t1 ∧(τ1,τ2’) ∈R∨t2 = t1 ∧(τ1’,τ2’) ∈R)} The lifting of on TESs, written , is the parametrized relation obtained by taking the fixed point of the function for arbitrary pair , i.e., the relation .
Lemma 3 (Correctness of lifting).
For any , the function is monotone, and therefore has a greatest fixed point.
Lemma 4.
If is a composability relation on observations, then the lifting is a composability relation on TESs. Moreover, if is symmetric (as in Definition 3), then is symmetric.
As a consequence of Lemma 4, any composability relation on observations gives rise to a composability relation on TESs. We define three composability relations on TESs, where Definition 10 and Definition 11 are two examples that construct coinductively the composability relation on TESs from a composability relation on observations. For the following definitions, let and be two components, and be a composition function on TESs.
Definition 9 (Free composition).
We use for the most permissive composability relation on TESs such that, for any , we have .
The behavior of component contains every TES obtained from the composition under of every pair and of TESs. This product does not impose any constraint on event occurrences of its operands.
Definition 10 (Synchronous composition).
Let be a relation on observables. We define two observations to be synchronous under according to the following two conditions:

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

only an observable that does not compose (under ) with any other observable can occur independently, i.e., at a different time.
A synchronous composability relation on observations satisfies the two conditions above. For any two observations with , if and only if: (t1 ¡ t2∧¬( ∃O2’ ⊆E2. (O1, O2’) ∈⊓)) ∨(t2 ¡ t1∧¬( ∃O1’ ⊆E1. (O1’, O2) ∈⊓)) ∨t2 = t1∧((O1, O2) = (O1’ ∪O1”, O2’ ∪O2”) ∧(O1’,O2’) ∈⊓ ∧(( ∀O ⊆E2. (O1”, O) ／∈⊓) ∧∀O ⊆E1. (O, O2”) ／∈⊓)∨(O1,O2) = (∅, ∅))
Example 3.
Let and with . Thus, if and only if . Alternatively, we have if and only if .
The lifting , written , defines a synchronous composability relation on TESs. The behavior of component contains TESs obtained from the composition under of every pair and of TESs that are related by the synchronous composability relation which, depending on , may exclude some event occurrences unless they synchronize. ^{5}^{5}5If we let be the element wise set union, define an event as a set of port assignments, and in the pair let 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 [AR03].
Definition 11 (Mutual exclusion).
Let be a relation on observables. We define two observations to be mutually exclusive under the relation if no pair of observables in can be observed at the same time. The mutually exclusive composability relation on observations allows the composition of two observations and , i.e., , if and only if (t1 ¡ t2) ∨(t2 ¡ t1) ∨(¬(O1 ⊓O2) ∧t1 = t2)
Example 4.
Let and with . Thus, for any , and and are two mutually exclusive observables.
Similarly as in Example 10, the lifting of , written , defines a mutual exclusion composability relation on TESs. The behavior of component contains TESs resulting from the composition under of every pair and of TESs that are related by the mutual exclusion composability relation which, depending on , may exclude some simultaneous event occurrences.
Similarly, we give a mechanism to lift a composition function on observable to a composition function on TESs. Such lifting operation interleaves observations with different time stamps, and compose observations that occur at the same time.
Definition 12 (Lifting  composition function).
Let be a composition function on observables. The lifting of to TESs is s.t., for where with : σ1[+]σ2 = {⟨σ1(0)⟩⋅(σ1’[+] σ2)if t1 ¡ t2⟨σ2(0)⟩⋅(σ1[+] σ2’)if t2 ¡ t1⟨(O1 + O2, t1)⟩⋅(σ1’[+] σ2’)otherwise
Definition 12 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 9, 10, 11, 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 1 to hold.
Lemma 5.
Let and be two composition functions on observables and let and be two composability relation on observations. Then,

is commutative if is symmetric and is commutative;

and are associative if, for all and for any triple of observations with , we have and ((o1,o2) ∈κ(E1,E2) ∧(ι1(o1,o2), o3) ∈κ(E1 ∪E2,E3)) ⇔((o2,o3) ∈κ(E2,E3) ∧(o1, ι2(o2,o3)) ∈κ(E1 ,E2 ∪E3)) with , where .

is idempotent if is idempotent and, for all we have .
3.5 Properties
We distinguish two kinds of properties: properties on TESs that we call trace properties, and properties on sets of TESs that we call behavior properties, which correspond to hyperproperties in [CS10]. 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 LABEL:ex:coordination, 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 LABEL:section:formalexample, we provide more intuition for the practical relevance of these properties.
Definition 13.
A trace property over a set of events is a subset . A component satisfies a property , if , which we denote as .
Example 5.
We distinguish the usual safety and liveness properties [AS85, CS10], and recall that every property can be written as the intersection of a safety and a liveness property. Let be an arbitrary set, and be a subset of . Intuitively, is safe if every bad stream not in has a finite prefix every completion of which is bad, hence not in . A property is a liveness property if every finite sequence in can be completed to yield an infinite sequence in
3 Components, composition, and properties
Each lemma of the section has its proof in the technical report [LAT21].
3.1 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 temperaturereading event, each of which has the internal structure of a namevalue 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.
Notation 1 (Events).
We use to denote the universal set of events.
An observable is a set of event occurrences that happen together and an observation is a pair of an observable and a timestamp .^{1}^{1}1Any totally ordered dense set would be suitable as the domain for time (e.g., positive rationals ). For simplicity, we use , the set of real numbers for this purpose. An observation represents an act of atomically observing occurrences of events in at time . Atomically observing occurrences of events in at time means there exists a small such that during the time interval :

every event is observed exactly once^{2}^{2}2A finer time granularity may reveal some ordering relation on the occurrence of events in the same set of observation., and

no event is observed.
We write to denote a finite sequence of size of elements over an arbitrary set , where for . The set of all finite sequences of elements in is denoted as . A stream^{3}^{3}3The set denotes the set of natural numbers . over a domain is a function . We use to represent the element of , and given a finite sequence , we write to denote the stream such that for and for . We use to denote the derivative of , such that for all .
A TimedEvent Stream (TES) over a set of events and a set of timestamps is a stream where, for :

for every , [i.e., time monotonically increases] and

for every , there exists such that [i.e., time is nonZeno progressive].
Notation 2 (Time stream).
We use to refer to the set of all monotonically increasing and nonZeno infinite sequences of elements in .
Notation 3 (TimedEvent Stream).
We use to denote the set of all TESs whose observables are subsets of the event set with elements in as their timestamps.
Given a sequence , we use the projections and to denote respectively the sequence of observables and the sequence of time stamps .
3.2 Components
The design of complex systems becomes simpler if such systems can be decomposed into smaller subsystems that interact with each other. In order to simplify the design of cyberphysical 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 TESs) and an interface (set of events).
Like existing semantic models, such as timedata streams [AR03], time signal [TSSL13], or discrete clock [FLDL18], 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 allornothing transaction.
Definition 1 (Component).
A component is a tuple where is a set of events, and is a set of TESs. We call the interface and the externally observable behavior of .
More particularly, Definition 1 makes no distinction between cyber and physical components. We use the following examples to describe some cyber and physical aspects of components.
Example 1.
Consider a set of two events , and restrict our observations to and . A component whose behavior contains TESs with alternating observations of and is defined by the tuple where L = { σ∈TES(E) ∣∀i ∈N.(pr1(σ)(i) = {0} ⟹pr1(σ)(i+1) = {1}) ∧(pr1(σ)(i) = {1} ⟹pr1(σ)(i+1) = {0}) } Note that this component is oblivious to time, and any stream of monotonically increasing nonZeno real numbers would serve as a valid stream of time stamps for any such sequence of observations.
Example 2.
Consider a component encapsulating a continuous function , where is a set of initial values, and is the codomain of values for . Such a function can describe the evolution of a physical system over time, where means that at time the state of the system is described by the value if initialized with . We define the set of all events for this component as the range of function given an initial parameter . The component is then defined as the pair such that: Lf = { σ∈TES(D) ∣∃d0 ∈D0. ∀i ∈N. pr1(σ)(i) = {f(d0,pr2(σ)(i))} } Observe that the behavior of this component contains all possible discrete samplings of the function at monotonically increasing and nonZeno sequences of time stamp. Different instances of would account for various cyber and physical aspects of components.
3.3 Composition
A complex system typically consists of multiple components that interact with each other. The example in Section 2 shows three components, a , a , and a , 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^{4}^{4}4Also 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.
Definition 2 (Composability relation on TESs).
A composability relation is a parametrized relation such that for all , we have .
Definition 3 (Symmetry).
A parametrized relation is symmetric if, for all and for all : .
A composability relation on TESs serves as a necessary constraint for two TESs to compose. We give in Section 3.4 some examples of useful composability relations on TESs that, e.g., enforce synchronization or mutual exclusion of observables. We define composition of TESs as the act of forming a new TES out of two TESs.
Definition 4.
A composition function on TES is a function .
We define a binary product operation on components, parametrized by a composability relation and a composition function on TESs, 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 TESs in the behavior of its operands deemed composable by the composability relation.
Definition 5 (Product).
Let be a pair of a composition function and a composability relation on TESs, and , , two components. The product of and , under and , denoted as , is the component where and is defined by L = { σ1 ⊕σ2 ∣σ1 ∈L1, σ2 ∈L2, (σ1, σ2) ∈R(E1,E2)}
Definition 5 presents a generic composition operator, where composition is parametrized over a composability relation and a composition function.
Lemma 1.
Let and be two composition functions on TESs, and let and be two composability relations on TESs. Then:

if is symmetric, then is commutative if and only if is commutative;

if, for all and with , we have
then and are associative if and only if

if for all and , we have , then is idempotent if and only if 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 by a component yields a component whose behavior contains all TESs that can compose with TESs in the behavior of to yield the TESs in the behavior of .
Definition 6 (Division).
Let be a composability relation on TESs, and a composition function on TESs. The division of two components and under and , denoted as , is the component such that: L = { σ∈TES(E1) ∣∃σ2 ∈L2. (σ, σ2) ∈R (E1, E2) ∧σ⊕σ2 ∈L1 }
If the dividend is , and the divisor is an operand of the product, e.g., , then the behavior of the result of the division, , contains all TESs in the behavior of the other operand (i.e., ) composable with a TES in the behavior of .
Lemma 2.
Let and be two components. Let , with a pair of a composability relation and a composition function on TESs. Then, {σ1 ∈L1 ∣∃σ2 ∈L2. (σ1,σ2) ∈R(E1 ∪E2, E2) ∩R(E1, E2)} ⊆L3
Corollary 1.
In the case where (see Definition 9) then .
The results of Section 3.3 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.
3.4 A coinductive construction for composition operators
In Section 3.3, 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 coinductive construction for composability relations on TESs. We show how constraints on observations can be lifted to constraints on TESs, and give weaker conditions for Lemma 1 to hold. The intuition for such construction is that, in some cases, the condition for two TESs 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 TESs is defined coinductively.
Definition 7 (Composability relation).
A composability relation on observations is a parametrized relation s.t. for all pairs , we have
Definition 8 (Lifting composability relation).
Let be a composability relation on observations, and let be such that, for any : Φκ(E1,E2)(R) = {(τ1, τ2) ∣(τ1(0), τ2(0)) ∈κ(E1,E2) ∧(pr2(τ1)(0) =t1 ∧pr2(τ2)(0) =t2) ∧(t1 ¡ t2 ∧(τ1’,τ2) ∈R∨t2 ¡ t1 ∧(τ1,τ2’) ∈R∨t2 = t1 ∧(τ1’,τ2’) ∈R)} The lifting of on TESs, written , is the parametrized relation obtained by taking the fixed point of the function for arbitrary pair , i.e., the relation .
Lemma 3 (Correctness of lifting).
For any , the function is monotone, and therefore has a greatest fixed point.
Lemma 4.
If is a composability relation on observations, then the lifting is a composability relation on TESs. Moreover, if is symmetric (as in Definition 3), then is symmetric.
As a consequence of Lemma 4, any composability relation on observations gives rise to a composability relation on TESs. We define three composability relations on TESs, where Definition 10 and Definition 11 are two examples that construct coinductively the composability relation on TESs from a composability relation on observations. For the following definitions, let and be two components, and be a composition function on TESs.
Definition 9 (Free composition).
We use for the most permissive composability relation on TESs such that, for any , we have .
The behavior of component contains every TES obtained from the composition under of every pair and of TESs. This product does not impose any constraint on event occurrences of its operands.
Definition 10 (Synchronous composition).
Let be a relation on observables. We define two observations to be synchronous under according to the following two conditions:

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

only an observable that does not compose (under ) with any other observable can occur independently, i.e., at a different time.
A synchronous composability relation on observations satisfies the two conditions above. For any two observations with , if and only if: (t1 ¡ t2∧¬( ∃O2’ ⊆E2. (O1, O2’) ∈⊓)) ∨(t2 ¡ t1∧¬( ∃O1’ ⊆E1. (O1’, O2) ∈⊓)) ∨t2 = t1∧((O1, O2) = (O1’ ∪O1”, O2’ ∪O2”) ∧(O1’,O2’) ∈⊓ ∧(( ∀O ⊆E2. (O1”, O) ／∈⊓) ∧∀O ⊆E1. (O, O2”) ／∈⊓)∨(O1,O2) = (∅, ∅))
Example 3.
Let and with . Thus, if and only if . Alternatively, we have if and only if .
The lifting , written , defines a synchronous composability relation on T
Comments
There are no comments yet.