Category Methods for Analysis of Two Approaches to Modelling Logical Time Based on Concept of Clocks

Abstract

This paper continues the study that has been begun in the series of authors' papers and has devoted to clarifying the interconnection between denotational and operational approaches for modelling logical time based on the concept of logical clocks. In the paper, a new category, namely the category of schedules, has introduced. The original definition of a morphism of schedules precedes to introducing this category. Refinement of a number of results of previous papers made it possible to establish the functorial nature of the method of associating the linear clock structure with a schedule and to prove that the corresponding functor determines the equivalence of the category of schedules and the category of linear clock structures.

Keywords

• logical time
• clock
• denotational semantic model
• operational semantic model
• schedule
• clock structure
• clock morphism
• schedule morphism

-

The trend of widespread use of distributed computing, observed in recent years, is a technological answer to the practical achievement of the upper bound of processor performance on the one side and the development of communication tools on the other. In addition, there is a tendency to integrate cybernetic and physical systems, which has been accelerated in the context developing Internetof-Things. You can find the more detailed analysis of these trends in [ 1 ].

But this analysis allows us to state that the problems associated with parallel, distributed and parallel computations turned out to be on the leading edge of

Computer Science and Information Technology.

This work is focused on the problem of modelling logical time in distributed systems, in particular on the model based on the concept of logical time, and is a continuation of authors’ results presented in [ 1 ]1.

1 Preliminary results of this article are available by http://ceur-ws.org/Vol-1844/ 10000488.pdf in [ 2 ].

The mentioned above paper is focused on the two approaches based on logical clocks to the modelling of time. Authors had shown that the language of the category theory is adequate for building models of Universum of events. In other words, the denotational approach to the modelling can well be formulated in the terms of the category theory. In contrast, for building operational models, authors have selected the set-theoretic approach. Unfortunately, the difference between mathematical backgrounds led to unclarity and incompleteness of describing the relationship between two classes of models, denotational and operational.

Thus, we see that the relationship of two approaches for determining semantic meaning of temporal constraint specifications based on the concept of logical clocks did not clarify by the paper. Therefore, the following problem arises. Problem. Establish the nature of the relationship between the two approaches described above to modelling of logical time based on the concept of clocks. The object of this paper to identify and ground the required relationship in the terms of category theory.

This paper has the following structure: Section 2 reminds the categorytheoretic description of the denotational model of logical time given in [ 2, 1 ]; Section 3 contains the category-theoretic description the operational model of logical time.

Section 2 has an overview character and contains a small number of new results, which are mostly of an auxiliary nature.

In the contrast, section 3 is original. It contains the definitions of schedule morphisms, the description of the category of schedules, and the proof of Main Theorem that establishes the equivalence of the category of linear clock structures and the category of schedules. This equivalence is precisely the relationship that eluded authors in the set-theoretic formulation. 2

Category of Clock Structures

The main definitions and results obtained in [ 1 ] are collected in this section. We do not give those proofs that do not require any changes in comparison with the corresponding proofs in [ 1 ]. A proof is given only if this proof simplifies the corresponding proof in [ 1 ] or if this proof establishes a new fact.

Consideration of causality relationship as a quasi-order (i.e. a reflexive and transitive relation) on the set of event occurrences is a generally accepted approach. Following this approach, we understand an Universum of events as a set I of event occurrences with a quasi-order “4” . Usually, we consider along with the relation “4” the relations , , # , and k . These relations are defined by the causality relation as in Table 1 (see also [ 1 ]). Now we give the definition of clock structure as an Universum of events with additional structures and properties. First of all we fix a finite set C whose each element is interpreted as a reference to the source (it is called a clock) of occurrences of the same event.

This leads us to the following definition in accordance with [1].

Definition 1. A C-structure is a triplet S = I; ; 4 where

I is the set of instants corresponding to the occurrences of events,

: I ! C is a surjective mapping that associates the clock that is the source of an instant with this instant, “4” is a quasi-order on I that models the causality relation between instants.

The triplet meets also the following axioms 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 c-timeline Ic = 1(c) is linearly ordered by “ ”.

This definition is not a novelty introduced in [ 1 ], it was used in accordance with [ 3 ]. But the following definition is such a novelty.

Definition 2. Let S0 = (I0; 0; 4) and S00 = (I00; 00; 4) be C-structures then a mapping f : I0 ! I00 is called a morphism of C-structures if the following holds for any i 2 I0 , the equation 00 ( f i) = 0 i is fulfilled, for any i 2 I0 and j 2 I0 , f i 4 f j whenever i 4 j , for any i 2 I0 and j 2 I0 , f i # f j whenever i # j .

The following proposition is evident.

Proposition 1. The class of all C-structures equipped with morphisms of Cstructures forms a category denoted below by StructC .

An important special class of clock structures is formed by so-called linear clock structures, defined in [ 1 ]. is false for all i; j 2 I . of clock structures.

Definition 3. A C-structure L = (I; ; 4) is called a linear structure if i k j

Now let us recall some results obtained in [ 1 ] concerning the arrangement Definition 4. Let S = ( ; ; 4) be a clock structure, A

I

I and i 2 A then i is called a minimal instant in A if the statement j i is false for any j 2 A.

To refer to the subset of minimal instants of A we use the denotation min A .

We associate the sequence of slices

structure S in the following manner

I[0] , I[ 1 ] , . . . , I[n] , . . .

with any CI[0] = min I ; I[n] = min I n S I[k]

! n 1 k=0 for n 2 N+ (1) where I is the instant set of S .

Proposition 2. For a C-structure S = (I; ; 4) the following properties hold 3. the sequence of slices is a covering of the set of instants; 4. if i 2 I[n] , j 2 I , and j

i then j 2 I[n] for some n 2 N ; 5. if i 2 I[n + 1] then there exists j 2 I[n] such that j i for some n 2 N . We will need some other properties of slices. From item 2 we directly obtain the follows. implies i

Corollary 1. If L with an instant set I is a linear C-structure then i; j 2 I[n] Corollary 2. The restriction

on I[n] is injective for all n 2 N .

Proof. If i =

j for some i; j 2 I[n] then the axiom of total ordering for the

Further i

j together with the mentioned axiom implies i = j . clock timelines of Def. 1 makes impossible the case i k j in item 2 of Prop. 2. tu i 2 I[m] and j 2 I[n] then the following properties hold Proposition 3. Let S = ( ; ; 4) be a C-structure and for some m; n 2 N ,

I 1. if i 4 j then m n , while i

j implies m < n ;

2. if S is linear and m

n then i 4 j , while m < n implies i j . existence of j0 2 I[n] such that j0 Prop. 2 the fact j0; j 2 I[n] .

To prove item 2 note the following.

i . But j0 i 4 j contradicts by item 2 of Proof. To prove item 1 suppose m > n . Then item 5 of Prop. 2 implies the If m = n we directly obtain the statement by Cor 1. i0 j then i0 i and from i 4 i0 j we conclude i j .

If m < n then item 5 of Prop. 2 implies the existence of i0 2 I[m] such that

The established properties of the clock structures make it possible to establish the properties of their morphisms. for some m; n 2 N the following properties hold

Proposition 4. For any morphism f : S0 !

S00 from the C-structure S0 = (I0; 0; 4) into the C-structure S00 = (I00; 00; 4) and i 2 I0[m] , f i 2 I00[n] 3. n

m ; 4. if f is an isomorphism then m = n .

2. if for some j 2 I0, we have i j then f j 2 I00[n] ; 1. the mapping f : I0 ! I00 preserves relations “4”, “ ”, “ ”, and “#”;

Proof. To prove item 1 note that f preserves relations “4” and “#” by Def. 2.

The statement i

j is equivalent to i 4 j and j 4 i and, therefore, f preserves “ ” . Further taking into account that i j if and only if i 4 j and i # j one can immediately obtain that f preserves “ ” .

To prove item 2 let us use proven item 1. Really, i j ensures, as item 1 claims,

f i

f j. Now use of item 4 of Prop. 2 leads to the required statement. To prove item 3 we use induction in m . For m = 0 it is true that n m . Suppose n < k + 1 . Then by item 5 of Prop. 2 there exists j 2 I0[n] such that j the statement holds for m

k and let m = k + 1 , i 2 I0[m] , f i 2 I00[n]. Suppose above shown f j into account j

f i . If f j 2 I00[r] then by induction hypothesis r i and item 1 of Prop. 3 one can derive that r < n . Thus, we i. As n. Taking have obtained two mutually excluding inequality r n and r < n and conclude that our supposition is incorrect i.e. n m .

Item 4 follows immediately from item 3.

Morphisms of linear clock structures hold additional properties.

following properties hold 1. if f i f j then i j ;

Proposition 5. For any morphism f : L

0 !

L00 from the linear C-structure

L 0 = (I0; 0; 4) into the linear C-structure L00 = (I00; 00; 4) and i; j 2 I0 the 2. if i 2 I0[m] , j 2 I0 , f i; f j 2 I00[n] for some m; n 2 N then j 2 I0[m] ; tu tu 3. f I0[m]

I00[n] for some n such that m

n . structures. Item 1 of Prop. 4 ensures f i # f j but this contradicts to f i Proof. To prove item 1 note that i 6 j is equivalent to i # j for linear clock f j .

To prove item 2 note f i; f j 2 I00[n] ensures f i

Taking into account the previous item one can conclude that i j . Now we need f j for a linear clock structure. to use item 4 of Prop. 2 to obtain the required statement.

Item 3 follows directly from the previous item.

tu

The operational approach to describe logical time dependences in distributed systems (including cyber-physical systems) is based on observing streams of system messages. Below this approach is described with the language of the category theory.

Definition 5. Let C be a finite set of logical clocks then any non-empty subset of C is called a clock message.

Informally, a clock message contains the information about which clocks ticked at the same time-point. the denotation MC .

To refer to the set of clock messages associated with a clock set C we use below Definition 6. A schedule (or more precisely a C-schedule) is an infinite sequence

= ( [0]; [ 1 ]; : : : ; [n]; : : :) of clock messages.

In [ 1 ], authors have defined the relation of modelling between linear clock structures and sets of schedules. Unfortunately, this relation does not associate natural sets of schedules with linear clock structures.

Thus, one can see that the use of the category theory language only for the denotational semantic model does not give a tool for establishing the required relationship with the operational semantic model being formulated in the set-theoretic terms. In this context, an attempt to reformulate the operational semantic model using the category theory language seems reasonable. 3

Category of Schedules

The operational approach to describe logical time dependences in distributed systems (including cyber-physical systems) is based on observing streams of system messages. Below this approach is described with the language of the category theory.

Definition 7. Let C be a finite set of logical clocks then any non-empty subset of C is called a clock message.

Informally, a clock message contains the information about which clocks ticked at the same time-point.

To refer to the set of clock messages associated with a clock set C we use below the denotation MC .

Definition 8. A schedule (or more precisely a C-schedule) is an infinite sequence = ( [0]; [ 1 ]; : : : ; [n]; : : :) of clock messages.

For two C-schedules 0 and 00 , a C-morphism from 0 into 00 is a triple h 0; k; 00i where k : N ! N is an injective mapping such that for any n 2 N 1. C-morphisms of the form h ; 1N; i are units of this composition;

2. the associative law is fulfilled for this composition.

Thus, the following statement is true.

Proposition 6. The set of all C-schedules equipped with C-morphisms of schedules forms a small category denoted below by SchedC .

Now we can formulate the principal result of this paper.

Main Theorem. The categories LinStructC and SchedC are equivalent i.e. there exists a pair of functors

F : SchedC ! LinStructC and

G : LinStructC ! SchedC such that F G is naturally isomorphic to the identity endofunctor of LinStructC and G F is naturally isomorphic to the identity endofunctor of SchedC . Note 1. All necessary definitions and facts about natural transformations and natural isomorphisms can be found in [ 4 ].

We use the following theorem as the main tool to establish the validity of Main

Theorem.

Theorem 1. Categories C and D are equivalent if and only if there exists a functor F : C ! D such that in the following manner

L = hI ; ; 4i where isomorphic; is a bijection. 1. for any object d in D , there exists an object c in C such that F c and d are 2. for any objects c0 and c00 in C , the mapping F : C c0; c00 ! D F c0; F c00 The proof of this theorem one can find in [5, Theorem 7.1], the proof of the more general statement is given in [4, IV.4, Theorem 1].

In [ 1 ], the linear C-structure L was associated with any 2 MC schedule I = fhc; ni 2 C

N j c 2 [n]g ; hc; ni = c for hc; ni 2 I ; hc0; n0i 4 hc00; n00i if and only if n0 n00 for hc0; n0i; hc00; n00i 2 I : Here we generalize this association by its extension up to a functor F from the category SchedC into the category LinStructC .

To do this we assign the required correspondences as follows for

2 SchedC for h 0; k; 00i 2 SchedC 0; 00 and hc; ni 2 L 0

F

= L ; F h 0; k; 00i hc; ni = hc; k(n)i : Now we need to check the validity of some statements. The corresponding checks are gathered in the following proposition.

Proposition 7. Let 0 , 00 , and 000 be objects of SchedC then 1. for any hc; ni 2 I belongs to I

2. for any C-morphisms h 0; k1; 00i and h 00; k2; 000i, the following is true

0 and h 0; k; 00i 2 SchedC 0; 00 , the item hc; k(n)i F h 0; k1; 00 i h 00; k2; 000i = F h 0; k1; i00 F h 00; k2; 000i ;

3. Fh 0; 1; 0i is the identity mapping from L

0 into itself .

Proof. Item 1 follows immediately from the definition of a schedule morphism (see Def. 8).

Item 2 and item 3 are checked by direct calculation. (2a) (2b)

Corollary 3. Formulae (2a) and (2b) determine a functor

F : SchedC ! LinStructC :

Below the following lemma are also needed for us.

is isomorphic to L .

Lemma. For any linear C-structure L , there exists C-schedule such that L Proof. Let L = ( ; ; 4) then we assign [n] =

I quence = [0]; [ 1 ]; : : : ; [n]; : : : is a C-schedule. i for some i 2 I[n] . Cor. 2 guarantees that such i is uniquely

N and hc; ni 2 I if c 2 [n] . In other words, determined. Thus, we can determine the mapping f : I conditions

f hc; ni = i 2 I[n] ensures that f is a morphism from L into L .

if and only if f (g i) = i for any i 2 I .

Thus, we have proven that L and L are isomorphic.

Now consider the mapping g : I ! I determined as follows g i = h i; ni where i 2 I[n] . The correctness of g is ensured by the construction of L . Item 1 of Prop. 3 ensures that g is a morphism from L into L .

It is evident that by construction g f hc; ni = hc; ni for any hc; ni 2 I and tu ! I by the following i = c . Item 2 of Prop. 3

Now we have all necessary to prove Main Theorem.

Proof (of Main Theorem). Our proof is based on applying Theorem 1 with the constructed above functor F : SchedC ! LinStructC . In accordance with the mentioned theorem, it is su cient to prove that functor F holds two following properties 1. for any L 2 LinStructC , there exists 2 SchedC such that F is isomorphic to L ; is bijective. 2. for any 0; 00 2 SchedC the mapping

h 0; k; 00i 2 SchedC 0; 00 7! F h 0; k; 00i 2 LinStructC F 0; F 00 Lemma and the method of constructing the functor F guarantee the validity of the first property. count that for each n 2 N, there exists c 2 C such hc; ni 2 I The mapping in the second property is injective. Indeed, if F h 0; k1; 00i = F h 0; k2; 00i then hc; k1(n)i = hc; k2(n)i for all hc; ni 2 I 0 . Taking into ac

The mapping in the second property is surjective. Really, if f is a morphism from L 0 into L

00 then f hc; ni = hc; k f (n)i . The occurrence of the same c on both sides of the equation is caused that f is a morphism. Reasoning as above we obtain the function k f : N ! N . It is evident that

I 0 [n] = nc 2 C j hc; ni 2 I Summing up the above, one can conclude that the approach based on the category theory is more expressive than the approach based on the set theory. Systematic using this approach we have established the character of the relationship between denotational and operational approaches to modelling logical time based on the concept of logical clocks. This relationship, as it has been shown (see Main Theorem), is an equivalence of the corresponding categories. This equivalence explains the equivalence between the denotational and operational semantics for some subset of Clock Constraint Specification Language (CCSL) called RCCSL [ 6 ].

At the same time, it should be mentioned that the results presented above do not give an exhaustive description of the categories introduced in [ 2 ] and this paper. Among the problems being posed by this and previous papers are the following. 1. What does a morphism of schedules mean informally or, in other words, how are relations between schedules established by morphisms understanding informally? 2. Does the equivalence of categories established above ensure the equivalence of the denotational and operational semantics of CCSL? 3. Does the category-theoretic approach provide methods to compose more complex systems using less complex systems or, in other words, what category-theoretic constructions are realised in the introduced categories? 4. Does the theoretic-category approach give a general model theory for logical time modelling based on the concept of logical clocks?

References

1. Zholtkevych , G. , El Zein , H. K. : Two approaches to modelling logical time in cyber-physical systems . In N. Bassiliades , et al., eds.: Information and Communication Technologies in Education, Research, and Industrial Applications . Volume 826 of CCIS., Springer, Cham ( 2018 ) 21 - 40

2. Zholtkevych , G. , El Zein , H. K. : Logical time models to study cyber-physical systems . In V. Ermolayev , et al., eds.: Information and Communication Technologies in Education, Research, and Industrial Applications . Integration, Harmonization and Knowledge Transfer . Volume 1844 of Workshop Proceedings., CEUR-WS (May 2017 )

3. Andre´, C. , Mallet F. : Clock constraints in UML MARTE CCSL . Research Report RR-6540 , INRIA ( 2008 )

4. Mac Lane , S. : Categories for the Working Mathematicians . 2nd edn . Springer-Verlag ( 1998 )

5. Novikov , B. : Lecture Notes on Category Theory. Luhansk National Pedagogical University ( 2004 )

6. Zholtkevych , G., other: Two semantic models for clock relations in the clock constraint specification language . In V. Ermolayev , et al., eds.: Information and Communication Technologies in Education, Research, and Industrial Applications . Volume 412 of CCIS., Springer, Cham ( 2013 ) 190 - 209