=Paper=
{{Paper
|id=Vol-1844/10000488
|storemode=property
|title=Logical Time Models to Study Cyber-Physical Systems
|pdfUrl=https://ceur-ws.org/Vol-1844/10000488.pdf
|volume=Vol-1844
|authors=Hassan Khalil El Zein,Grygoriy Zholtkevych
|dblpUrl=https://dblp.org/rec/conf/icteri/ZeinZ17
}}
==Logical Time Models to Study Cyber-Physical Systems==
<pdf width="1500px">https://ceur-ws.org/Vol-1844/10000488.pdf</pdf>
<pre>
    Logical Time Models to Study Cyber-Physical Systems

                 Hassan Khalil El Zein and Grygoriy Zholtkevych
                     School of Mathematics and Computer Science
                       V.N. Karazin Kharkiv National University
                       4, Svobody Sqr., Kharkiv, 61022, Ukraine
             dr.hassanelzein@icloud.com; g.zholtkevych@karazin.ua



       Abstract. The paper is devoted to problems caused by the nonlinearity of logical
       time in distributed, especially cyber-physical, systems. Two approaches to the
       modelling of such systems are considered in the paper. The operational approach
       is based on the traditional model that defines the admissible system behaviour
       as a set of acceptable schedules of the system. The paper argues in favour of
       restricting possible sets of schedules by that sets of schedules that satisfy certain
       safety properties. The denotational approach is stated in the language of category
       theory. This abstraction level clarifies concepts used in the models. In particular,
       it is explained the feature of linear models as terminal objects with respect to
       some natural class of morphisms. Further, the interrelation between these two
       approaches is represented as a formal relation and discuss some properties of the
       relation that need to be studied.

       Keywords: cyber-physical system, logical time, clock, denotational semantic
       model, operational semantic model, schedule, safety property, clock structure,
       clock morphism


1    Introduction

The National Science Foundation of USA defines cyber-physical systems (CPS
for short) as “engineered systems that are built from and depend upon the syn-
ergy of computational and physical components”[12, Synopsis of Program] and
clarifies ibidem that “emerging CPS will be coordinated, distributed, and con-
nected, and must be robust and responsive”. The perspectives of the CPS-techno-
logy is estimated by this document as follows: “The CPS of tomorrow will far
exceed the simple embedded systems of today in capability, adaptability, re-
siliency, safety, security, and usability. CPS technology will transform the way
people interact with engineered systems, just as the Internet transformed the way
people interact with information. New smart cyber-physical systems will drive
innovation and competition in sectors such as the power grid, transportation,
buildings, medicine, and manufacturing”[12, Synopsis of Program]. The last
revision of the mentioned document [13] states the following: “CPS are engi-
neered systems that are built from, and depend upon, the seamless integration of
computational algorithms and physical components. Advances in CPS will en-
able capability, adaptability, scalability, resiliency, safety, security, and usability
that will far exceed the simple embedded systems of today. CPS technology will
transform the way people interact with engineered systems – just as the Internet
has transformed the way people interact with information. New smart CPS will
drive innovation and competition in sectors such as agriculture, energy, trans-
portation, building design and automation, healthcare, and manufacturing just
as the Internet has transformed the way people interact with information. In-
deed, it is also clear that CPS technologies are central to achieving the vision
of Smart & Connected Communities (S&CC), including “Smart Cities”, which
spans these multiple sectors and includes the important attributes of efficiency,
safety, and security” [13, Synopsis of Program]. Thus, comparing this texts we
may say that the notion of CSP is a well-established concept and refer to a com-
bined system of executive subsystems and network of controlling units (cyber
components), which guarantee the wholeness of the system.
     It should be emphasised that the development trend of modern technology is
the integration of CPS-components through technology Internet of Things (IoT).
Analysing trends of IoT- and CPS-technology Kate Carruthers notes [3]: “CPS
include traditional embedded and control systems, and these will be transformed
by new approaches from IoT. However, the challenge for IoT and CPS remains
security and risk management. As less rigorously controlled systems are linked
then risk becomes distributed and the provenance of software components be-
comes difficult to trace. This gives rise to questions around risk management
and liability for breaches or damages”.
     Thus, we may state that any modern CPS should be considered as a safety-
critical system. The necessity to use trustworthy strategies for development of
systems of such a type is the first significant conclusion for the practice of sys-
tem design.
     The above reasons motivate our research, which is aimed to clarification
of objective limits to the applicability of the clock model for the specification
and computer-aided analysis of behavioural constraints for cyber components
of CPS. The principal tool of our study is the clock model proposed by Leslie
Lamport [8](see also [2, Chap. 2] and [6, Chap. 3]) for studying distributed
computing. A survey of examples of applying this model to study CPS can be
found in [11].


2   General Structure of a Cyber-Physical System

Remind that in the paper we use the term cyber-physical system to refer to a het-
erogeneous complex of natural objects and artificial subsystems. This complex
is managed by the system of interacting controllers (cyber components), which
provides its operation as a whole entity.
    This informal description can be refined by the following class diagram
(Fig. 1) representing the abstract framework for CPS.



            CPS

                                      1..*

                          CyberComponent


               1..*
                                                       receives

    ExecutiveSubsystem
                                                     Message

                                                                      generates

          {complete,
           disjoint}         {complete, disjoint}
                                                     sends

                       Component


                                        receives               Response


                  ArtificialSubsystem



                      NaturalObject




                           Fig. 1. CPS: Conceptual Framework



   This framework establishes that

 – any CPS consists of at least one instance of class ExecutiveSubsystem and
   at least one instance of class CyberComponent;
 – each of these instances is an instance of class Component;
 – an instance of class ExecutiveSubsystem is either an instance of class Natu-
   ralObject or of class ArtificialSubsystem.
This model fixes that the message interchange between components of CPS is
the only way to provide interaction of these components:
 – each instance of class Component sends an instance of class Message,
   which are received by some instances of class CyberComponent;
 – each instance of class CyberComponent generates a special message, which
   is an instance of class Response, of course, a response depends on mes-
   sages received by the cyber component that has generated this response;
 – if the component receiving responses is an instance of class ExecutiveSub-
   system then it executes the actions corresponding to the received response
   collection, otherwise, the behaviour is similar to the previous case.
The described architecture model establishes that the behaviour of each cyber
component is determined only by a message stream, received by the component.
In this case, the use of trace semantics to distinguish between the correct and
incorrect behaviour of a cyber component is a reasonable solution.
     The appropriate approach to the correctness of the logical time dependencies
was apparently first used by Leslie Lamport [8].
     The clock model is developed to specify and analyse the logical temporal
relationships between the event occurrences (called below instants) inhabiting
different event types. The first class citizens of the model are clocks, which
are considered as sources of monotypic instants. The uniqueness of the source
for each event type means that all instants of the same event type are linearly
ordered in time, i.e. for any pair of such instants, we can exactly establish what
instant from this pair has happened before.
     We are interested in studying such relationships between instants which do
not depend on fortuitous aspects of behaviours of the system being studied, but
which fix regularities of behaviours of the system. In other words, our interests
are focused on relations of causality.
     There are two approaches to study these relationships, namely, the approach
based on representing admissible system behaviours by using sequences of mes-
sages describing the sets of simultaneous event occurrences, and the approach
based on representing admissible system behaviours by using objects of the spe-
cial category, the category of clock structures. The first approach (see Sec 3) can
be used to define the operational semantics of the specification languages, and
the second approach (see Sec 4) can be used to define the denotational seman-
tics for languages describing the temporal requirements limiting possible system
behaviours.
     Thus, understanding the interrelationship between these two approaches is
an important both theoretical and applied problem for the theory of CPS. The
first results concerning this problem were obtained in [15]. This paper develops
the study presented in the mentioned paper.
3     Model of Acceptable Schedules

The operational approach goes back, apparently, to L. Lemport’s long-standing
paper [8]. This approach is based on the simple idea to distinguish correct and
incorrect system behaviours by observing streams of system messages that carry
information about occurred events. In the context the concept of safety property
introduced by L. Lamport [7] is very important. This concept was formalised by
B. Alpern and F. B. Schneider in [1]. They also established an interconnection
between the concepts of safety and liveliness and the topological properties of
the corresponding system traces.

3.1     Clocks, Messages, and Schedules
As mentioned above all monotypic instants have the same source. We call these
sources by clocks and introduce some finite set C whose elements are used to
refer to clocks.
Definition 1. Any non-empty subset of C is called a message.
The corresponding set of messages we denote below by MC .
Definition 2. A schedule (or more precisely a C-schedule) is an infinite se-
quence of messages.
As usual, the set of all C-schedule we denote by MCω .
Any message µ ∈ MC is interpreted as the notification “at the moment, each
clock belonging to µ and only they fired the event occurrence”.
Definition 3. Let n ∈ N and u be a non-empty finite sequence (a non-empty
word)1 of messages then the pair (n, u) is called a local schedule that starts at
time point n.
To work with sequences and words, we use the notation like the Python notation
for sequential data types.

3.2     Topology on Mω
                           C
This subsection contains some facts of the general topology necessary to un-
derstand the topological nature of the notions of safety and liveliness. For more
detailed acquaintance with the subject, you can refer to [1,14].

Proposition 1. The family Zn (u) | n ∈ N+ , u ∈ MC+ where Zn (u) = {π ∈ MCω |
                            n                        o

π[n : n + len(u)] = u} forms the base of Tikhonov topology on MCω .
 1
     The set of non-empty words we denote as usually by MC+ .
Proposition 2. Let {πn | n ∈ N} be a sequence of C-schedules and π be a C-
schedule then πn −−−−→ π in Tikhonov topology iff for any M ∈ N+ there exists
                  n→∞
N ∈ N+ such that for any n > N the equality πn [0 : M] = π[0 : M] holds.

Definition 4. Let P be a subset of MCω then P is called closed if for any schedule
sequence {πn ∈ P | n ∈ N} such that there exists π = lim πn the schedule π is
                                                        n→∞
also a member of P.

3.3    Safety Properties

Speaking not formally, L. Lamport proposed to recognise the property of sched-
ules (the set of schedules satisfying this property) a safety property if any vio-
lation of this properties can be detected by the way of system observing during
a finite time interval [7]. The following definition describes formally a safety
property.
Definition 5. Let P be a property of C-schedules then P is a safety property iff
for any π < P there exists n ∈ N+ such that π0 < P for each π0 ∈ Z0 [π[0 : n]].
In other words, a property P is a safety property iff the set of schedules satisfying
P is a closed set in Tikhonov topology.
One can find the detailed discussion of the formal definition of safety properties
and their topological characteristics in [1].
    We consider that any acceptable behaviour of CPS is being described by the
corresponding safety property. Safety ensures that the corresponding property is
physically correct because it can be checked using information obtained in the
past and present. In other words, checking such a property does not require the
presence of magical abilities like foresight ability.

4     Category of Clock Structures

We try to describe the denotational approach to modelling of CPS behaviour in
this section. We emphasize that if the approach specified above gives accept-
able schedules in physical time, then the denotational approach describes a pure
logical picture of relations between event occurrences without any references to
physical time.

4.1    Quasi-Ordered Sets

This subsection is given to introduce the mathematical basis for the denotational
approach to semantic modelling of CPS behaviour. The principal source is [5]. It
is well known that the quasi-ordered set is a set equipped with a binary relation
that is reflexive and transitive.
    As usual, for a quasi-ordered set (X, 4) we define the following derived bi-
nary relations on X (see Table 1).

                      Table 1. The Derived Relations on a Quasi-ordered Set

             Name                     Properties               Notation Definition
          coincidence reflexive, antisymmetric, and transitive  i≡ j    i4 j ∧ j4i
          precedence          irreflexive and transitive        i≺ j     i 4 j ∧ j 64 i
           exclusion                  symmetric                  i# j   i≺ j ∨ j≺i
         independence                 symmetric                  ik j   i 64 j ∧ j 64 i



    Further, for a quasi-ordered set (X, 4) and i ∈ X the principal ideal generated
by i is the subset ( i ] of X defined as ( i ] = { j ∈ X | j 4 i}.

4.2     Clock Structures
We start this section with the following formal definition.
Definition 6. Let C be a finite set, each element of which is interpreted as a
reference to the source (it is called a clock) of occurrences of the same event.
Then a C-structure S 2 is a triple (I, γ, 4) where
 – I is the set of instants corresponding to the occurrences of events,
 – 4 is a quasi-order on I that models the causality relation between instants,
   and, finally,
 – γ : I → C is a surjective mapping that associates each instant with the
   clock that is the source of this instant
provided that the following axioms met:
         the axiom of unbounded liveness:
                                                                                              (1)
            the set I is infinite;
         the axiom of finite causality:
                                                                                              (2)
            for any i ∈ I the corresponding principal ideal ( i ] is finite;
         the axiom of total ordering for clock timelines:
            for each c ∈ C the set Ic = γ−1 (c) is linearly ordered by the                    (3)
            corresponding restriction of “4”.
This definition is a repetition of the corresponding definition given in [10].
   Some simple conclusions from this definition are gathered in the following
proposition.
 2
     Usually, one uses the term clock structure if C is uniquely determined by the context.
Proposition 3. Let S = (I, γ, 4) be a C-structure then
1. width of the ordered set (I, ≺) is less than or equal to |C|;
2. for each c ∈ C the set Ic is well-ordered;
3. for each c ∈ C the ordinal type of Ic is less than or equal to ω;
4. there is at least one c ∈ C such that its ordinal type equals ω;
5. the set I is countable;
6. if i, j ∈ I and i ≡ j then either i = j or i 6≺ j and j 6≺ i, i.e. any equivalence
   class for the relation “≡” is an antichain for the strict order ≺;
7. if i, j, i0 , j0 ∈ I, i ≺ j, i ≡ i0 , and j ≡ j0 then i0 ≺ j0 ;
8. each instant i ∈ I is uniquely characterized by the pair (γ(i), idx(i)) where
   idx : I → N is defined as follows

                               idx(i) = { j ∈ Iγ(i) | j ≺ i} .

4.3   Morphisms of Clock Structures
As usual, we define morphisms of C-structures to describe the relationship be-
tween them.
Definition 7. Let S0 and S00 be C-structures, I0 and I00 be the corresponding
sets of instants then a mapping f : I0 → I00 is called a C-morphism from S0
into S00 if the following holds
1. γ(i) = γ( f (i)) for any i ∈ I0 ;
2. i 4 j implies f (i) 4 f ( j) for any i, j ∈ I0 ;
3. i # j implies f (i) # f ( j) for any i, j ∈ I0 .

Note 1. Usually, we do not distinguish symbols used to denote the causality
relations and the mappings associated instants with their sources for different
clock systems.

Note 2. The fact that f is a C-morphism from S0 into S00 is as usually denoted
by f : S0 → S00 .

The following statement establishes an important property of C-morphisms.
Proposition 4. Any C-morphism is an injective mapping.

Proof. Indeed, let us suppose that f : I0 → I00 be a morphism of C-structures
(I0 , 4, γ) and (I00 , 4, γ), i , j ∈ I0 , and f (i) = f ( j). Then either γ(i) , γ( j) or
γ(i) = γ( j) and idx(i) , idx( j) (see Prop 3, item 8).
Firstly, let us assume that γ(i) , γ( j) but then we get γ( f (i)) = γ(i) , γ( j) =
γ( f ( j)) and, therefore, f (i) , f ( j). This contradicts to the supposition, hence
the case is impossible.
Secondly, let us assume that γ(i) = γ( j) = c and idx(i) , idx( j). Let for definite-
ness idx(i) < idx( j) then γ(i) = γ( j) ensures i ≺ j. But this means that i ≺ j, i.e.
i # j and, therefore, f (i) # f ( j), i.e. we have that f (i) ≡ f ( j) is false and, hence,
 f (i) = f ( j) is false also. Thus, in this case, we also obtain a contradiction with
the supposition. The case idx( j) < idx(i) is analysed by the similar way.               t
                                                                                         u

The following statement is evident.

Proposition 5. For any finite set C, the class of C-structures together with the
class of C-morphisms form a small category 3 .

Corollary 1 (of Prop 4). Any C-morphism is a monomorphism in the category
of C-structures.

The above results lead to the following classification of C-morphisms.

Definition 8. A C-morphism f : S0 → S00 is called a covering C-morphism if
the mapping f : I0 → I00 is surjective.

The following evident proposition clarifies logical relations between different
classes of C-morphisms.

Proposition 6. Logical relations between the notions C-isomorphism, covering
C-morphism, C-epimorphism, C-bimorphism, C-monomorphism, and C-mor-
phism are shown in Fig. 2.


                                         C-isomorphism


                                      covering C-morphism

               C-epimorphism                                       C-bimorphism

                                       C-monomorphism


                                           C-morphism

                 Fig. 2. Logical relations between different classes of C-morphisms



 3
     The necessary definitions and results from the theory of categories can be found in [9].
5     Interrelation between Operational and Denotational Approaches

This section contains some results concerning mutual relationships between op-
erational and denotational models. Below we construct a relation between clock
structures and schedules. This relation describes the possible ways to dip a clock
structure in physical time. Properties of schedules represent these ways.

5.1    Some Needed Technique
Below we need the following notion.
Definition 9. Let S = (I, γ, 4) be a C-structure, A ⊂ I, and i ∈ A then i is
called a minimal instant in A if for any j ∈ A the statement j ≺ i is false.
The subset of minimal instants of A is below denoted by min A.
    We associate the sequence of slices I[0], I[1], . . . with any C-structure S in
the following manner

                      I[0] = min I
                                       n−1
                                                   
                                     [          
                      I[n] = min I \
                                           I[m]     for n > 0
                                          m=0

where I is the instant set of S.
Proposition 7. The following properties hold:
1. |I[n]| ≤ |C| for each n ∈ N;
2. if i, j ∈ I[n] for some n ∈ N then either i k j or i ≡ j;
3. the sequence of slices is a covering of the set of instants;
4. if i ∈ I[n] for some n ∈ N, j ∈ I, and j ≡ i then j ∈ I[n];
5. if i ∈ I[n + 1] for some n ∈ N then there exists j ∈ I[n] such that j ≺ i.

Proof. 1) This property follows directly from Def 6 and item 6 of Prop 3.
2) Indeed, each of statements i ≺ j and j ≺ i contradicts to the statement that
the both statements i ∈ I[n] and j ∈ I[n] are true.
3) Suppose that there exists some i ∈ I such that i < I[n] for any n ∈ N then
using induction one can demonstrate that for each n ∈ N there exists jn ∈ I[n]
such that jn ≺ i. Taking into account that I[m] I[n] = ∅ for m , n we
                                                       T
conclude that the set { jn | n ∈ N} is infinite. But this set is a subset of ( i ]. This
contradiction (see Def 6) demonstrates that the proposition is true.
4) If j < I[n] then item 3 ensures that j ∈ I[m] for! some m , n.
                                            n−1
If m < n then k ≺ i for some k ∈ I \
                                            S
                                                I[s] . The statement i ≡ j ensures
                                                s=0
                                                      !
                                            m−1
                                            S
that k ≺ j and, therefore, j < min I \            I[s] . This contradiction shows that
                                            s=0
m > n. But similar reasoning demonstrates that the assumption m > n leads also
to a contradiction.                                                               !
5) If i ∈ I[n + 1] for some i ∈ I[n] then j 6≺ i for any j ∈ I \
                                                                         S
                                                                              I[k] . If
                                                                       !0≤k≤n
                                                              S
 j 6≺ i for all j ∈ I[n] also then j 6≺ i for any j ∈ I \          I[k] . This means
                                                             0≤k<n
                 I[k] and, therefore, i ∈ I[n + 1] is false. This proves the item of
            S
that i ∈
          0≤k<n
the proposition.                                                                        t
                                                                                        u

Corollary 2. An instant i belongs to I[n] iff number of elements of each maxi-
mal chain in ( i ] equals n + 1.

Proof. It is being proved by induction with respect to n.                               t
                                                                                        u

Corollary 3. Slice I[n] for each n ∈ N is a union of ≡-equivalence classes of
elements belonging the slice, moreover slice elements lying to different classes
are independent.

5.2    Linear Clock Structures

An important special class of clock structures is formed by so-called linear clock
structures.
Definition 10. A C-structure L = (I, γ, 4) is called a linear C-structure if i k j
is false for any i, j ∈ I.
      Any linear clock structure holds the following property.
Proposition 8. Let L = (I, γ, 4) be a linear C-structure, S0 = (I0 , γ, 4) be a C-
structure, and f : I → I0 be a covering C-morphism then f is a C-isomorphism.

Proof. Indeed, taking into account that f is a covering C-morphism one can
conclude that f is a bijection, hence there exists the unique mapping g : I0 → I
such that g( f (i)) = i for each i ∈ I and f (g(i0 )) = i0 for each i0 ∈ I0 .
Now let us demonstrate that g is a C-morphism.
If i0 , j0 ∈ I0 and i0 4 j0 then for i = g(i0 ) and j = g( j0 ) the linearity of I ensures
either j ≺ i or i 4 j.
The statement j ≺ i implies j # i and, therefore, f ( j) = j0 # f (i) = i0 , i.e.
j0 ≺ i0 ∨ i0 ≺ j0 . On the other hand, the statement j ≺ i implies j 4 i and, there-
fore, j0 4 i0 . But the assertions i0 ≺ j0 and j0 4 i0 are evidently incompatible,
hence j0 ≺ i0 is necessary true. Taking into account that j0 ≺ i0 and i0 4 j0 are
incompatible one can conclude that i 4 j is the unique acceptable variant. Thus,
we proved that g(i0 ) 4 g( j0 ).
Further, if i0 , j0 ∈ I0 and i0 # j0 then for i = g(i0 ) and j = g( j0 ) the linearity of I
ensures i ≡ j or i # j. Taking into account that i ≡ j ensures i0 ≡ j0 we conclude
that i ≡ j contradicts to i0 # j0 . Thus, we proved that g(i0 ) # g( j0 ).
Therefore, g is the inverse C-morphism for f .                                            t
                                                                                          u

As it is below shown the proposition converse to Prop. 8 is also true.

5.3   Analogue of Szpilrajn Extension Theorem
The concept of extension is an important concept in ordered sets theory. There-
fore we study its analogue for clock structures.
Definition 11. Let S = (I, γ, 4) be C-structures then a covering non-invertible
C-morphism e : I → I0 for some C-structure S0 = (I0 , γ, 4) is called an exten-
sion of S. Whenever S0 is a linear C-structure we say that e is a linear extension
of S.
The following theorem refines Theorem 3 in [15].
Theorem (about Linear Extension). Let S = (I, γ, 4) be a C-structure and
i∗ , j∗ be some pair of independent instants belonging to I then there exists a
linear extension e : S → L such that the condition e(i∗ ) ≺ e( j∗ ) holds.
To prove the theorem we need in the following lemmas.
Lemma 1. Let S = (I, γ, 4) be a C-structure and i∗ , j∗ be two independent
instants in I then there exists an extension e : S → S∗ such that e(i∗ ) ≺ e( j∗ ).

Proof. Let 1 = {∗} be some singleton. Then let us define

        I∗ = I × 1
        γ(i, ∗) = γ(i)    for any i ∈ I
        (i, ∗) 4 ( j, ∗) iff either i 4 j or i 4 i∗ and j∗ 4 j   for any i, j ∈ I
        e(i) = (i, ∗)    for any i ∈ I.

Let us check that “4” defined on I∗ is a quasi-order. Indeed, it is evident that
this relation is reflexive. If now we have that (i, ∗) 4 ( j, ∗) and ( j, ∗) 4 (k, ∗) for
some i, j, k ∈ I then the next variants are only possible:
1. i 4 j and j 4 k; these conditions ensure i 4 k and, hence, (i, ∗) 4 (k, ∗);
2. i 4 i∗ , j∗ 4 j, and j 4 k; these conditions ensure i 4 i∗ and j∗ 4 k, but this
   means that (i, ∗) 4 (k, ∗);
3. i 4 j, j 4 i∗ , and j∗ 4 k; these conditions ensure (i, ∗) 4 (k, ∗) that is
   checked similarly to above.

Thus, “4” is a quasi-order on I∗ .
One can easily see that (i∗ , ∗) 4 ( j∗ , ∗), but ( j∗ , ∗) 64 ( j∗ , ∗), i.e. e(i∗ ) ≺ e( j∗ ).
The construction ensures evidently that i # j implies e(i) # e( j).
                                                   S
And, finally, it is evident that ( (i, ∗) ] ⊂ ( i ] ( i∗ ]. Therefore, the set ( (i, ∗) ] is
finite for any (i, ∗) ∈ I∗ .
Thus, S∗ = (I∗ , γ, 4) is a C-structure, e : S → S∗ is a covering C-morphism,
and e(i∗ ) ≺ e( j∗ ).                                                                            t
                                                                                                 u

Lemma 2. Let S = (I, γ, 4) then for I∗ = I×1; γ(i, ∗) = γ(i); and (i, ∗) 4 ( j, ∗)
meaning i ∈ I[m], j ∈ I[n], and m ≤ n the triple L = (I∗ , γ, 4) is a linear
C-structure. Moreover, e : S → L that is defined as e(i) = (i, ∗) is a linear
extension of S.

Proof. Taking into account that I[m] I[n] = ∅ if m , n and item 3 of Prop 7
                                         T
one can conclude that 4 is a correctly defined quasi-order on I∗ , moreover
items 4 and 5 of Prop 7 ensure that i 4 j implies (i, ∗) 4 ( j, ∗) and i ≺ j implies
(i, ∗) ≺ ( j, ∗). Thus, L is a linear C-structure and e is a covering C-morphism.
Therefore, e is a linear extension of S.                                          t
                                                                                  u

Proof (of Theorem about Linear Extension).
Let e0 : S → S0 be the extension of S constructed in accordance with Lemma 1
end e00 be the linear extension of S0 constructed in accordance with Lemma 2
then e = e00 ◦ e0 is a linear extension of S.
Construction of e0 ensures that e0 (i∗ ) ≺ e0 ( j∗ ) and construction of e00 ensures
that i0 ≺ j0 implies e00 (i0 ) ≺ e00 ( j0 ). Thus, e(i∗ ) ≺ e( j∗ ).              t
                                                                                  u

Corollary 4. Each C-structure S is uniquely defined by the family {eα } of all its
linear extensions in the following sense

                    if i, j ∈ I then i 4 j iff eα (i) 4 eα ( j) for all eα .

Corollary 5. If C-structure S satisfies the property “any covering C-morphism
from S is a C-isomorphism” then this C-structure is linear.

Note 3. Cor 5 is the claimed inversion of Prop 8.

Note 4. The obtained criterion for the linearity of a clock structure shows that
all linear clock structures and only them are “weak terminal” with respect to
covering clock morphisms.
5.4     Relation of Admissibility
Linear extensions of a clock structure can be considered as admissible realisa-
tions of the clock structure in physical time. In this subsection, the correspond-
ing formal relation called admissibility is defined.
    Let us assume that some finite set of clock are fixed. Then we associate
the linear C-structure Lπ = (Iπ , 4, γ) with any C-schedule π in the following
manner:
1. Iπ = {(n, c) ∈ N × C | c ∈ π(n)};
2. γπ (n, c) = c for (n, c) ∈ Iπ ;
3. (m, a) 4 (n, b) means m ≤ n for any (m, a) and (n, b) belonging to Iπ .
Thus we can define the following relation.
Definition 12. We say that a C-structure S admits a C-schedule π and denote
this fact by S |= π if there exists an extension e : S → Lπ .
Def 12 leads us to the notion property of clock structure.
Definition 13. A set of C-schedules P is a property of C-structure S 4 if for any
π ∈ P the condition S |= π is fulfilled.
Cor 4 of Theorem about Linear Extension shows that any clock structure can be
uniquely specified by some property, which we call the characteristic property of
the structure. Unfortunately, at this time we do not how can be characterised the
class of properties that contains all characteristic properties of clock structures
and only them. Such a hypothesis seems plausible.
Conjecture. The characteristic property of any clock structure is a safety prop-
erty.

6     Conclusion

The paper discusses the problems of the interaction of components for an im-
portant class of complex systems, so-called cyber-physical systems. The clock
model, first described by L. Lamport has been chosen as the principle tool for
research. Such a choice is motivated by rich expressive means of the model
language, which provide the specification process both synchronous and asyn-
chronous methods of intercomponent interactions. The successful practice of
using this model for specification temporal guarantees and constraints for sys-
tem behaviour on the base of Clock Constraint Specification Language was also
taking into account.
 4
     Symbolically, S |= P.
     Two approaches to modelling logical time for cyber-physical system have
been considered in the paper.
     The first approach is based on the notion schedule, which is used to model an
acceptable sequence of occurrences of system events. Each set of schedules can
be considered as a specification of the required property of system behaviour. In
the context, the key notion is safety property that ensures the guarantee to detect
a violation of system behaviour during a finite time.
     The second approach had been proposed to define the denotational seman-
tics of Clock Constraint Specification Language. In the paper, our efforts have
been focused on developing this approach on the base of the category-theoretic
language. Sets of instants equipped by the causality relation and the mapping
associating each instant with its source are objects of the corresponding cate-
gory, a category of clock structures. Using the category-theoretic language has
given a possibility to refine and make more rigorous this model due to the suited
definition of morphisms. The theorem about linear extension under such an ap-
proach is becoming more expressive. This theorem, which has been proved in
the paper, is a bridge between two approaches being analysed.
     The manner to use Theorem about Linear Extension to establish interdepen-
dence between clock structures and properties of schedules has been described
in the last part of the paper.
     It has been shown that properties of clock structures are identified by sets of
schedules. It is also clear that there exist sets that are not characteristic properties
of the corresponding clock structure. But the problem to prove the Conjecture
formulated in Subsection 5.4 is very important because if Conjecture is fulfilled
then the role of safety properties obtains not only operational but denotational
meaning.
     Another very important and interest problem consists in studying the fea-
tures of the class of properties that are characteristic properties of clock struc-
tures.
     We hope that further study of this topic will lead to formulating the weakest
necessary requirements for the languages of the behaviour constraint specifica-
tion based on the clock model for cyber-physical systems.

References
 1. Alpern, B., Schneider, F. B.: Defining Liveness. Information Processing Letters. 21, 181–185
    (1985).
 2. Cachin, C., Guerraoui, R., Rodrigues, L.: Introduction to Reliable and Secure Distributed
    Programming, 2nd edition. Springer-Verlag Berlin Heidelberg (2011).
 3. Carruthers, K.: Internet of Things and Beyond: Cyber-Physical Systems. IEEE
    IoT Newsletter. May (2016), http://iot.ieee.org/newsletter/may-2016/
    internet-of-things-and-beyond-cyber-physical-systems.html
 4. Glitia, C., Deantoni, J., Mallet, F.: Logical Time @ Work: Capturing Data Dependencies and
    Platform Constraints. In: Kaźmierski, T. J. J., Morawiec, A (Eds.). System Specification and
    Design Languages. LNEE, vol. 106, 223–238. Springer New York (2012).
 5. Harzheim, E.: Ordered Sets. Springer Science & Business Media (2006).
 6. Kshemkalyani, A. D., Singhal, M.: Distributed Computing: Principles, Algorithms, and Sys-
    tems. Cambridge University Press (2008)
 7. Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Transactions on Soft-
    ware Engineering. 2, 125–143 (1977).
 8. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. CACM. 21(7),
    558–565 (1978), http://lamport.azurewebsites.net/pubs/time-clocks.pdf.
 9. Mac Lane, S.: Categories for the Working Mathematician, 2nd ed. Springer-Verlag New York
    Inc (1998).
10. Mallet, F.: Clock constraint specification language: specifying clock constraints with
    UML/MARTE. Innovations in Systems and Software Engineering. 4(3), 309–314 (2008).
11. Mallet, F.: MARTE/CCSL for Modeling Cyber-Physical Systems. In: Drechsler, R. and
    Kühne, U. (Eds.) Formal Modeling and Verification of Cyber-Physical Systems. Pp. 26–49.
    Springer Fachmedien Wiesbaden (2015).
12. The National Science Foundation. Cyber-Physical Systems (CPS). Program Solicitation
    NSF 12-520. Arlington, VA: NSF, 2012, https://www.nsf.gov/pubs/2012/nsf12520/
    nsf12520.htm#toc
13. The National Science Foundation. Cyber-Physical Systems (CPS). Program Solicitation
    NSF 17-529. Arlington, VA: NSF, 2017, https://www.nsf.gov/pubs/2017/nsf17529/
    nsf17529.htm#toc
14. Willard, S.: General Topology. Dover Publication Inc. Mineola, NY (1998)
15. Zholtkevych, G., Mallet, F., Zaretska, I., Zholtkevych, G.: Two Semantic Models for Clock
    Relations in the Clock Constraint Specification Language. In: Ermolayev, V. et al (Eds.)
    Information and Communication Technologies in Education, Research, and Industrial Ap-
    plications. CCIS, vol. 412, 190–209. Springer International Publishing (2013).

</pre>