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