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.
The National Science Foundation of USA defines cyber-physical systems (CPS
for short) as “engineered systems that are built from and depend upon the
synergy of computational and physical components”[12, Synopsis of Program] and
clarifies ibidem that “emerging CPS will be coordinated, distributed, and
connected, and must be robust and responsive”. The perspectives of the
CPS-technology is estimated by this document as follows: “The CPS of tomorrow will far
exceed the simple embedded systems of today in capability, adaptability,
resiliency, 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 [
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 [
Thus, we may state that any modern CPS should be considered as a safetycritical system. The necessity to use trustworthy strategies for development of systems of such a type is the first significant conclusion for the practice of system 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 [
General Structure of a Cyber-Physical System Remind that in the paper we use the term cyber-physical system to refer to a heterogeneous 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.
receives Message sends
generates receives
Response CPS
1..* ExecutiveSubsystem
1..*
CyberComponent {complete, disjoint}
{complete, disjoint}
Component ArtificialSubsystem
NaturalObject
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 NaturalObject 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 messages received by the cyber component that has generated this response; – if the component receiving responses is an instance of class ExecutiveSubsystem 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 [
The clock model is developed to specify and analyse the logical temporal relationships between the event occurrences (called below instants) inhabiting di erent 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 messages describing the sets of simultaneous event occurrences, and the approach based on representing admissible system behaviours by using objects of the special 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 semantics 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 [
Model of Acceptable Schedules
The operational approach goes back, apparently, to L. Lemport’s long-standing
paper [
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.
The corresponding set of messages we denote below by MC.
quence of messages.
As usual, the set of all C-schedule we denote by MC!.
clock belonging to and only they fired the event occurrence”.
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 MC!
This subsection contains some facts of the general topology necessary to
understand the topological nature of the notions of safety and liveliness. For more
detailed acquaintance with the subject, you can refer to [
Proposition 1. The family nZn(u) j n 2 N+; u 2 MC+o where Zn(u) = f 2 MC! j [n : n + len(u)] = ug forms the base of Tikhonov topology on MC!. 1 The set of non-empty words we denote as usually by MC+.
schedule then n n!1! in Tikhonov topology i for any M 2 N+ there exists N 2 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 f n 2 P j n 2 Ng such that there exists = lim n the schedule is n!1 also a member of P. 3.3
Safety Properties
Speaking not formally, L. Lamport proposed to recognise the property of
schedules (the set of schedules satisfying this property) a safety property if any
violation of this properties can be detected by the way of system observing during
a finite time interval [
for any < P there exists n 2 N+ such that 0 < P for each 0 2 Z0[ [0 : n]]. In other words, a property P is a safety property i 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 [
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 acceptable 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 [
As usual, for a quasi-ordered set (X; 4) we define the following derived binary relations on X (see Table 1).
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:
the set I is infinite; the axiom of finite causality:
for any i 2 I the corresponding principal ideal ( i ] is finite;
the axiom of total ordering for clock timelines:
for each c 2 C the set Ic = 1(c) is linearly ordered by the
corresponding restriction of “4”.
(1)
(2)
(3)
This definition is a repetition of the corresponding definition given in [
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 jCj; 2. for each c 2 C the set Ic is well-ordered; 3. for each c 2 C the ordinal type of Ic is less than or equal to !; 4. there is at least one c 2 C such that its ordinal type equals !; 5. the set I is countable; 6. if i; j 2 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 2 I, i j, i i0, and j j0 then i0 j0;
idx : I ! N is defined as follows
idx(i) = f j 2 I (i) j j ig : 4.3
Morphisms of Clock Structures As usual, we define morphisms of C-structures to describe the relationship between them.
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 2 I0; 2. i 4 j implies f (i) 4 f ( j) for any i; j 2 I0; 3. i # j implies f (i) # f ( j) for any i; j 2 I0.
Note 1. Usually, we do not distinguish symbols used to denote the causality relations and the mappings associated instants with their sources for di erent clock systems.
by f : S0 ! S00.
The following statement establishes an important property of C-morphisms.
(I0; 4; ) and (I00; 4; ), i , j 2 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 definiteness 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. tu The following statement is evident.
class of C-morphisms form a small category 3.
of C-structures.
The above results lead to the following classification of C-morphisms. the mapping f : I0 ! I00 is surjective.
The following evident proposition clarifies logical relations between di erent classes of C-morphisms.
C-epimorphism
C-bimorphism
C-isomorphism covering C-morphism
C-monomorphism
C-morphism
3 The necessary definitions and results from the theory of categories can be found in [
Some Needed Technique Below we need the following notion.
Definition 9. Let S = (I; ; 4) be a C-structure, A I, and i 2 A then i is called a minimal instant in A if for any j 2 A the statement j i is false. The subset of minimal instants of A is below denoted by min A.
the following manner I[0] = min I
0 n 1 1 I[n] = min BBBBBB@I n m[=0 I[m]ACCCCCC for n > 0 where I is the instant set of S.
4. if i 2 I[n] for some n 2 N, j 2 I, and j i then j 2 I[n];
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 2 I[n] and j 2 I[n] are true. 3) Suppose that there exists some i 2 I such that i < I[n] for any n 2 N then using induction one can demonstrate that for each n 2 N there exists jn 2 I[n] such that jn i. Taking into account that I[m] T I[n] = ? for m , n we conclude that the set f jn j n 2 Ng is infinite. But this set is a subset of ( i ]. This contradiction (see Def 6) demonstrates that the proposition is true.
n 1 ! If m < n then k i for some k 2 I n S I[s] . The statement i j ensures s=0 that k
j and, therefore, j < min I n S I[s] . This contradiction shows that m > n. But similar reasoning demonstrates that the assumption m > n leads also to a contradiction. 5) If i 2 I[n + 1] for some i 2 I[n] then j 6 i for any j 2 I n j 6 i for all j 2 I[n] also then j 6 i for any j 2 I n
S 0 k n ! ! I[k] . If
S 0 k<n that i 2 the proposition.
S 0 k<n
tu tu mal chain in ( i ] equals n + 1.
Proof. It is being proved by induction with respect to n.
elements belonging the slice, moreover slice elements lying to di erent classes are independent. 5.2
Linear Clock Structures An important special class of clock structures is formed by so-called linear clock structures. is false for any i; j 2 I.
Definition 10. A C-structure L = (I; ; 4) is called a linear C-structure if i k j
Any linear clock structure holds the following property.
Proposition 8. Let L = (I; ; 4) be a linear C-structure, S0 = (I0; ; 4) be a Cstructure, 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 Now let us demonstrate that g is a C-morphism. such that g( f (i)) = i for each i 2 I and f (g(i0)) = i0 for each i0 2 I0. conclude that f is a bijection, hence there exists the unique mapping g : I0 ! I If i0; j0 2 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 j0 i0 _ i0
i implies j # i and, therefore, f ( j) = j0 # f (i) = i0, i.e. j0. On the other hand, the statement j i implies j 4 i and, therefore, 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 ensures i that i 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 2 I0 and i0 # j0 then for i = g(i0) and j = g( j0) the linearity of I j or i # j. Taking into account that i j ensures i0 j0 we conclude j contradicts to i0 # j0. Thus, we proved that g(i0) # g( j0).
Therefore, g is the inverse C-morphism for f . tu As it is below shown the proposition converse to Prop. 8 is also true. 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
extension of S. Whenever S0 is a linear C-structure we say that e is a linear extension
The following theorem refines Theorem 3 in [
Theorem (about Linear Extension). Let S = ( ; ; 4) be a C-structure and I i ; j be some pair of independent instants belonging to I then there exists a To prove the theorem we need in the following lemmas. instants in I then there exists an extension e : S ! S such that e(i ) Lemma 1. Let S = ( ; ; 4) be a C-structure and i ; j be two independent I
Proof. Let 1 = f g be some singleton. Then let us define
I = I
1 (i; ) = (i) for any i 2 I e(i) = (i; ) for any i 2 I: (i; ) 4 ( j; ) i either i 4 j or i 4 i and j 4 j for any i; j 2 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 2 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.
One can easily see that (i ; ) 4 ( j ; ), but ( j ; ) 64 ( j ; ), i.e. e(i ) The construction ensures evidently that i # j implies e(i) # e( j). And, finally, it is evident that ( (i; ) ] ( i ] S( i ]. Therefore, the set ( (i; ) ] is
and e(i ) finite for any (i; ) 2 I .
Lemma 2. Let S = (I; ; 4) then for I = I 1; (i; ) = (i); and (i; ) 4 ( j; ) meaning i 2 I[m], j 2 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
items 4 and 5 of Prop 7 ensure that i 4 j implies (i; ) 4 ( j; ) and i Proof. Taking into account that I[m] T I[n] = ? if m , n and item 3 of Prop 7 one can conclude that 4 is a correctly defined quasi-order on I , moreover j implies (i; )
( j; ). Thus, L is a linear C-structure and e is a covering C-morphism.
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 ) linear extensions in the following sense
if i; j 2 I then i 4 j i e (i) 4 e ( j) for all e . 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. tu tu tu Linear extensions of a clock structure can be considered as admissible realisations of the clock structure in physical time. In this subsection, the corresponding 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 = f(n; c) 2 N C j c 2 (n)g; 2. (n; c) = c for (n; c) 2 I ;
Thus we can define the following relation.
Def 12 leads us to the notion property of clock structure. and denote Definition 13. A set of C-schedules P is a property of C-structure S 4 if for any 2 P the condition S j= 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.
erty. 6
Conclusion The paper discusses the problems of the interaction of components for an important 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 asynchronous methods of intercomponent interactions. The successful practice of using this model for specification temporal guarantees and constraints for system behaviour on the base of Clock Constraint Specification Language was also taking into account.
4 Symbolically, S j= 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 semantics of Clock Constraint Specification Language. In the paper, our e orts 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 category, 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 approach 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 interdependence 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 features of the class of properties that are characteristic properties of clock structures.
We hope that further study of this topic will lead to formulating the weakest necessary requirements for the languages of the behaviour constraint specification based on the clock model for cyber-physical systems.