Coalgebraic Understanding of Random Systems with Output Artem Panchenko, Grygoriy Zholtkevych 1 School of Math and Computer Science, V.N. Karazin Kharkiv National University, 4 Svobody Sqr, Kharkiv, 61022, Ukraine Abstract The safety concept for clock constraints has already been coalgebraically studied for fully determin- istic cyber-physical systems (CPS). However, the corresponding control systems, as a rule, cannot be implemented in practice. There are many reasons for this, and the main one is the inability to collect accurate information about the state of the system in real time. In this article, the theory of determin- istic systems is generalised to the case of stochastic systems. The key tool for this generalisation is the use of the distribution monad. The advantage of the proposed approach is that it ensures that the previously proposed structure can be implemented in real-time systems, the behaviour of which could not be otherwise specified based on a purely deterministic approach. Keywords discrete system, system with output, random system, coalgebraic approach 1. Introduction It is known that rapid growth of CPS capacity is not possible today, primarily due to the limitations of technological progress and the atomic nature of the substances from which transistors, which provide computing power, are made, [1]. Alternative approaches are therefore being designed to address this problem, the main one being the design of distributed systems. Herein distributed system is a collection of independent entities that cooperate to solve a problem that cannot be individually solved [2]. We intentionally did not use the expression "computing machines" in the definition but replaced it with the word entities, because we mean that the nodes of such a system can be both subtracting machines and different kinds of controllers and sensors, as far as modern technical systems are complexes of interacting physical and cybernetical components. Hence, we can say that the mainstream of developing modern technical systems is developing cyber-physical systems (CPS). However, due to the fact that cyber-physical systems, as a rule, are deeply integrated with control elements, unforeseen situations can emerge which could lead to system failure. The consequences of such emergencies can be catastrophic [3] To identify emergencies in real-time mode, we need to have a precise specification of the system behaviour that must consider both desired and actual system states. The solving of this ICTERI 2021: ICT in Education, Research, and Industrial Applications, September 28–October 02, 2021, Kherson, Ukraine " panchenko2020pg@student.karazin.ua (A. Panchenko); g.zholtkevych@karazin.ua (G. Zholtkevych)  0000-0001-5865-6158 (A. Panchenko); 0000-0002-7515-2143 (G. Zholtkevych) © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) problem requires the development of formal methods for modelling the behaviour of distributed systems. The development of these methods should be carried out through a formal description of security restrictions for the designed CPS. We assume that we can describe all constraints by a cause-and-effect relationship between events in the system. It is good to take into account the cause-and-effect approach and that it is possible to use only the logical clocks model in distributed systems during the synchronisation of its elements [4]. Therefore, the main problem for us is to maintain the causal relationship between events in the system. One of the common approaches to this problem solution is to use models based on the theory of categories and coalgebras. This approach is proposed in the works of J. Rutten [5] and B. Jacobs [6]. In the context of implementing this approach to the semantic framework for building behavioural models, it should be noted the work [7, 8], which aims to create a generic tool for developing semantic models for specification language constraints of distributed systems based on the concept of logical clocks. The main shortcoming of the solutions proposed above [7, 8] is the assumption of complete determinism of the systems under study. Obviously, in practice, such an assumption cannot be fulfilled, or its implementation will be costly. This is due to many factors, the main of which is the distributed nature of the systems, as well as real-time work. Thus, this article is a continuation of the research carried out by G. Zholtkevych and M. Labzhaniia [8] and an extension of the theory to the case when we work with stochastic systems. This article makes extensive use of category theory concepts and facts. Therefore, we use the nLab [9] web resource for familiarizing readers with these concepts and facts. When citing an nLab article, we provide the corresponding URL. In the paper, we consider coalgebras over the category of sets and mappings denoted below by Set. This paper is an introduction to the research area and structured as follows • Section 3 contains a brief survey of general category-theoretic and coalgebraic concepts used in the paper. • Section 4 devoted to the concept of the finite distribution endofunctor of category Set. • Section 5 contains the definitions and preliminary results related to the coalgebraic approach for studying random systems with outputs. 2. Related Work The approach whereby we use logical rules to verify the work of CFS is sufficiently widespread. It is also worth noting the scientific community’s awareness of the need to deal with the safety of systems by applying formal methods. 2.1. Design Challenges Review The problems of modern cyber-physical systems design are clearly defined in [10]. It is shown that due to the specific field of application of such systems we are obliged to see increased trespasses to the reliability of its components. The paper concluded that standard models for constructing specifications that cope with creating single-threaded systems are bad at working with distributed systems. It was also concluded that it was necessary to develop formal approaches to describing the specification of the cyber-physical system. 2.2. Logical rules usage Due to problems with the complexity of synchronizing the states of the asynchronous system elements, we, as described above, the set of authors use exactly logical dependencies between states. In [11] the authors of such rules use a human-friendly UML diagram format. Later, the authors convert this specification model to a verifiable model in nuXmv format. This approach allows authors to use different models of specification (both UML diagrams and Petri nets), which is an indisputable advantage. However, this article does not raise the problem of working with systems with total or partial uncertainty, that is, randomly. It is worth noting that the use of logical (cause-effect) rules to describe events in parallel computing systems is the most common approach. Paper [12] points out the disadvantages of using UML associated with the model of time, called Simple Time, which is used in it. Thus, the necessity for a more complex and formal narrative model is evident. 2.3. Coalgebraic approach As we have discussed above, the priority in the modelling of shared systems is to develop formal models to describe their work with the use of cause-effect relationship between events. One possible solution to this problem is to build coalgebraic models. This is primarily because of the induction principle [5] present in this mathematical model. In addition to the studies described above [7, 8], the continuation of which is this article attention should also be drawn to [13]. The interest of this article is that the author also works with probabilistic systems. However, the author does not emphasize the application of this theory in distributed systems, which is a disadvantage. 3. Coalgebra Definition and Related Concepts In this section, we introduce the definition of a coalgebra and related basic concepts following to [9, https://ncatlab.org/nlab/show/coalgebra+for+an+endofunctor]. In addition, some specific concepts are discussed for the case the underlying category is the category Set. Thus, we assume in this section some category C called underlying and its endofunctor 𝐹 are given and fixed. Definition 1. A morphism 𝑎 of C is called an 𝐹 -coalgebra if the equality cod 𝑎 = 𝐹 (dom 𝑎) is fulfilled. In the case, dom 𝑎 is called the carrier of 𝑎 and denoted below by 𝑎 . More detail see [9, https://ncatlab.org/nlab/show/coalgebra+for+an+endofunctor]. Definition 2. Let 𝑎 and 𝑏 be 𝐹 -coalgebras then a morphism 𝑓 : 𝑎 → 𝑏 is called an 𝐹 - morphism from 𝑎 into 𝑏 (symbolically, 𝑓 : 𝑎 → 𝑏) if the diagram 𝑓 𝑎 - 𝑏 𝑎 𝑏 commutes or, equivalently, the equation (𝐹 𝑓 )𝑎 = 𝑏𝑓 holds. ? 𝐹𝑓 ? 𝐹 𝑎 - 𝐹 𝑏 More detail see [9, https://ncatlab.org/nlab/show/coalgebra+for+an+endofunctor]. Proposition 1. The class of 𝐹 -coalgebras equipped with 𝐹 -morphisms is a category, which is usually denoted by Coalg𝐹 (C) or by Coalg𝐹 if the underlying category C is clear from the context. Another important concept for a coalgebraic theory is the notion of bisimulation. For coalgebras of the category Set, this notion is introduced by the next definition [5] 𝑎 pr 𝑏 pr Definition 3. A bisimulation of 𝐹 -coalgebras 𝑎 and 𝑏 is a span 𝑎 ←−− 𝑟 −−→ 𝑏 in the category of 𝐹 -coalgebras where 𝑟 ⊂ 𝑎 × 𝑏 , and pr𝑎 and pr𝑏 are restrictions on 𝑟 of the corresponding projections i.e. the diagram pr pr𝑏 𝑎  𝑎 𝑟 - 𝑏 𝑎 𝑟 𝑏 commutes. ? 𝐹 pr𝑎 ? 𝐹 pr𝑏 ? 𝐹 𝑎  𝐹 𝑟 - 𝐹 𝑏 Final objects of category of coalgebras are very important for constructing semantic models of programming and specification languages. Definition 4. A terminal object of Coalg𝐹 if it exists is called a final 𝐹 -coalgebra, which is denoted by 𝜈𝐹 . Definition 5. For any 𝐹 -coalgebra 𝑎, the unique 𝐹 -morphism from 𝑎 into 𝜈𝐹 is called an anamorphism and denoted by (𝑎). The concepts of a final coalgebra and an anamorphism one can found in [9] with hyperlinks http://ncatlab.org/nlab/show/terminal+coalgebra+for+an+endofunctor and http://ncatlab.org/ nlab/show/cocycle respectively. Further, we follow the approach proposed by J. Rutten [5] namely to consider an 𝐹 -coalgebra for endofunctor 𝐹 of the category Set as a discrete system called 𝐹 -system. Remark 1. Coalgebra is a powerful tool for modelling dynamic systems by definition. Inclusively it illustrates the change of some mathematical entity under the influence of some transformation of it. We will always think of a dynamic system as a coalgebra, morphism as a set of rules to change its states. The F-functor, in its turn, we interpret as a tool to preserve our hypotheses when switching to another system, thus creating an upper-level abstraction of the operation of an entire class of dynamic systems. 4. Distribution Endofunctor The concept of an endofunctor of finitary distributions is here introduced similarly as in [9, http://ncatlab.org/nlab/show/distribution+monad] and [14]. To expand the System with Output in the case of random selection elements we need to set a probability distribution rule. Since we use a coalgebra approximation as the basis of the model, we need to provide an appropriate design. That’s why we need Distribution Endofunctor. For any 𝑋 : Set, let us define ⃒ 𝑝(𝑥) ̸= 0 for finite number 𝑥 ∈ 𝑋 only {︃ ⃒ }︃ 𝒟𝑋 = 𝑝 : 𝑋 → [0, 1] ⃒ and ∑︀ 𝑝(𝑥) = 1 (𝒟-obj) ⃒ ⃒ 𝑥∈𝑋 Now for any mappings 𝑓 : 𝑋 → 𝑌 , let us define 𝒟𝑓 : 𝒟𝑋 → 𝒟𝑌 as follows ∑︁ 𝒟𝑓 = 𝜆 𝑝 . 𝜆 𝑦 ∈ 𝑌 . 𝑝(𝑥). (𝒟-mor) 𝑥∈𝑋|𝑓 𝑥=𝑦 Of course, we need to check (𝒟-mor) specifies an element of 𝒟𝑌 . Indeed, (︀ )︀ ∑︁ ∑︁ 0 ≤ (𝒟𝑓 )𝑝 (𝑦) = 𝑝(𝑥) ≤ 𝑝(𝑥) = 1 𝑥∈𝑋|𝑓 𝑥=𝑦 𝑥∈𝑋 and ∑︁ (︀ )︀ ∑︁ ∑︁ ∑︁ (𝒟𝑓 )𝑝 (𝑦) = 𝑝(𝑥) = 𝑝(𝑥) = 1. 𝑦∈𝑌 𝑦∈𝑌 𝑥∈𝑋|𝑓 𝑥=𝑦 𝑥∈𝑋 Remark 2. Informally within our model (𝒟-obj) will mean the following: the function P gives the probability of this transition for each variant of the following state. Then to the end of the section, we simply prove the correctness of the work of this function and that it is a function of the probability distribution. Proposition 2. Formulae (1) determine an endofunctor of the category Set. Proof. For any set 𝑋, we have evidently (𝒟 id𝑋 )𝑝 = 𝜆 𝑥 ∈ 𝑋 . 𝑝(𝑥) = 𝑝 i.e. 𝒟 id𝑋 = id𝒟𝑋 . 𝑓 𝑔 Further, for 𝑋 − →𝑌 → − 𝑍, ⎛ ⎞ (︀ )︀ (︀ )︀ ∑︁ (𝒟𝑔)(𝒟𝑓 ) 𝑝 = (𝒟𝑔) (𝒟𝑓 )𝑝 = (𝒟𝑔) ⎝𝜆 𝑦 ∈ 𝑌 . 𝑝(𝑥)⎠ 𝑥∈𝑋|𝑓 𝑥=𝑦 ⎛ ⎞ ∑︁ ∑︁ = 𝜆𝑧 ∈ 𝑍 . ⎝𝜆 𝑦 ∈ 𝑌 . 𝑝(𝑥)⎠ (𝑦) 𝑦∈𝑌 |𝑔(𝑦)=𝑧 𝑥∈𝑋|𝑓 𝑥=𝑦 ⎛ ⎞ ∑︁ ∑︁ ∑︁ = 𝜆𝑧 ∈ 𝑍 . ⎝ 𝑝(𝑥)⎠ = 𝜆 𝑧 ∈ 𝑍 . 𝑝(𝑥) 𝑦∈𝑌 |𝑔(𝑦)=𝑧 𝑥∈𝑋|𝑓 𝑥=𝑦 𝑥∈𝑋|𝑔(𝑓 (𝑥))=𝑧 (︀ )︀ = 𝒟(𝑔𝑓 ) 𝑝. Thus, 𝒟 is an endofunctor of Set. pr pr Let us take two sets 𝑋 and 𝑌 then we have the universal arrow 𝑋 ←−𝑋− 𝑋 × 𝑌 −−→ 𝑌 𝑌 representing the product in the category Set. Applying the endofunctor 𝒟 gives 𝑋 𝒟 pr 𝑌 𝒟 pr 𝒟𝑋 ←−−− − 𝒟(𝑋 × 𝑌 ) −−−−→ 𝒟𝑌 where (𝒟 pr𝑋 )𝑝 = 𝜆 𝑥 ∈ 𝑋 . 𝑝(𝑥, 𝑦) and (𝒟 pr𝑌 )𝑝 = 𝜆 𝑦 ∈ 𝑌 . ∑︀ ∑︀ 𝑝(𝑥, 𝑦). 𝑦∈𝑌 𝑥∈𝑋 In other words, (𝒟 pr𝑋 )𝑝 and (𝒟 pr𝑌 )𝑝 are marginal distributions of the joint distribution 𝑝. 5. Concept of a Random System with Output and Related Concepts Remind that a system with output [7] is a coalgebra of type determines by the endofunctor 𝒮𝑁 of the category Set where 𝒮𝑁 𝑋 = 𝑁 × 𝑋 for any set 𝑋 (𝒮𝑁 -obj) 𝒮𝑁 𝑓 = id𝑁 ×𝑓 for any sets 𝑋, 𝑌 and mapping 𝑓 : 𝑋 → 𝑌 (𝒮𝑁 -mor) where 𝑁 is some finite set whose elements are interpreted as system notifications. We use the idea of randomization for obtaining random systems with output. 5.1. Random Systems with Outputs More precisely, let us consider the endofunctor ℛ𝑁 of Set defined as follows ℛ𝑁 𝑋 = (𝒟𝒮𝑁 )𝑋 = 𝒟(𝑁 × 𝑋) for any set 𝑋 (ℛ𝑁 -obj) ℛ𝑁 𝑓 = (𝒟𝒮𝑁 )𝑓 = 𝒟(id𝑁 ×𝑓 ) for any sets 𝑋, 𝑌 and mapping 𝑓 : 𝑋 → 𝑌 . (ℛ𝑁 -mor) Definition 6. Let 𝑋 be a set then a mapping 𝜎 : 𝑋 → ℛ𝑁 𝑋 is below called a random system with output. In this case, the set 𝑋 is called the carrier of 𝜎 and denoted by 𝜎 . Remark 3. It is obvious that the endofunctor (ℛ𝑁 -obj) manages the modeling problem of Random Systems with Outputs. Meaningfully, this means that we define a set of following possible states with probability distributions on them for each state of the system. Example 1. Let us denote by 𝒯𝑁 the set of infinite trees such that (see Fig. 1) 1. each internal node has at most finite children; 2. each internal node excluding the root node is labelled by an element of 𝑁 ; 3. each edge is labelled by a number from [0, 1] such that the sum of labels for edges outgoing from the same node is 1. Note that each subtree of a tree of the specified kind is a tree of this kind if to erase the label of its root. This note leads us to the definition of a system 𝜇 : 𝒯𝑁 → ℛ𝑁 𝒯𝑁 . If 𝑡 ∈ 𝒯𝑁 and 𝑡1 , . . . , 𝑡𝑘1 are the subtrees corresponding children of the root of 𝑡 then denote by 𝑡′1 , . . . , 𝑡′𝑘1 the trees obtained by erasing labels in their roots and define the distribution Figure 1: An element of 𝒯𝑁 𝑘1 ∑︁ 𝜇𝑡 = 𝑝1𝑖 · 𝛿(𝑛1𝑖 ,𝑡′𝑖 ) (2) 𝑖=1 Easy to understand that 𝜇𝑡 ensures restoring uniquely of 𝑡 by follows (see Fig. 2): 1. restore tree 𝑡𝑖 for 𝑖 = 1, . . . , 𝑘1 by labelling its root with 𝑛1𝑖 ; 2. create a new root; 3. create an edge from the new root to the root of 𝑡𝑖 and label it with 𝑝1𝑖 . with with with as the root label as the root label as the root label Figure 2: Restoring 𝑡 using 𝜇𝑡 5.2. Morphisms of Random Systems with Outputs Morphism is very important when working with coalgebra structures. Substantively, within the framework of our model, morphism allows us to move from one particular Random Systems with Outputs to another. Thus, our reasoning will be true not only for a particular task but for a whole class of tasks. The next proposition gives a refinement of the general definition of a coalgebraic morphism (see [9, https://ncatlab.org/nlab/show/coalgebra+for+an+endofunctor]) for the case of ℛ𝑁 - coalgebras. Proposition 3. For systems with output 𝜎 and 𝜏 , a mapping 𝑓 : 𝜎 → 𝜏 is an ℛ𝑁 -morphism from 𝜎 into 𝜏 if ∑︁ (𝜎𝑥)(𝑛, 𝑥′ ) (3) (︀ )︀ 𝜏 (𝑓 𝑥) (𝑛, 𝑦) = 𝑥′ ∈ 𝜎 |𝑓 𝑥′ =𝑦 whenever 𝑛 ∈ 𝑁 and 𝑦 ∈ 𝜏 . Proof. The mapping 𝑓 is an ℛ𝑁 -morphism iff the next diagram commutes 𝑓 𝜎 - 𝜏 𝜎 𝜏 ? ℛ𝑁 𝑓 ? ℛ𝑁 𝜎 - ℛ𝑁 𝜏 or, in other words, the next equation holds. (ℛ𝑁 𝑓 )𝜎 = 𝜏 𝑓 (4a) Therefore, let us compute the left and right sides of (4a). For the left side, we have (︁(︀ )︀ )︁ (︀ )︀ (ℛ𝑁 𝑓 )𝜎 𝑥 (𝑛, 𝑦) = (ℛ𝑁 𝑓 )(𝜎𝑥) (𝑛, 𝑦) ∑︁ (𝜎𝑥)(𝑛, 𝑥′ ). (4b) (︀ )︀ = 𝒟(id𝑁 ×𝑓 )(𝜎𝑥) (𝑛, 𝑦) = 𝑥′ ∈ 𝜎 |𝑓 𝑥′ =𝑦 And for the right side, we have (︁(︀ )︀ )︁ (4c) (︀ )︀ 𝜏 𝑓 𝑥 (𝑛, 𝑦) = 𝜏 (𝑓 𝑥) (𝑛, 𝑦). Thus, equation (3) ensures the validity of equation (4a) due to (4b) and (4c). Conversely, equation (4a) ensures evidently the validity of equation (3). 𝑛 Remark 4. Let us denote by 𝑥 − → 𝑥′ the event “system 𝜎 has passed from state 𝑥 into state 𝑥′ 𝜎 having sent notification 𝑛” then (𝜎𝑥)(𝑛, 𝑥′ ) is interpreted as the probability of this event i.e. (︁ )︁ 𝑛 (𝜎𝑥)(𝑛, 𝑥′ ) = Pr 𝑥 − → 𝑥′ . 𝜎 Using this denotation, one can rewrite formula (3) as follows (︁ )︁ (︁ )︁ 𝑛 𝑛 ∑︁ Pr 𝑓 𝑥 −→𝑦 = Pr 𝑥 − → 𝑥′ . (3* ) 𝜏 𝜎 𝑥′ ∈ 𝜎 |𝑓 𝑥′ =𝑦 Due to general theory, the class of random systems with output equipped with ℛ𝑁 -morphism is a category, which is denoted by Coalgℛ𝑁 . Example 2. Let 𝜎 be a random system with output then for any 𝑥 ∈ 𝜎 , one can build a tree 𝜅𝜎 𝑥 from 𝒯𝑁 as follows 1. set of children for the root is formed by pairs of (𝑛, 𝑦) ∈ 𝑁 × 𝜎 such that (𝜎𝑥)(𝑛, 𝑦) > 0; 2. node (𝑛, 𝑦) is labelled with 𝑛; 3. the edge connected the root and node (𝑛, 𝑦) is labelled with (𝜎𝑥)(𝑛, 𝑦); 4. then this process is repeated for each node (𝑛, 𝑦) using 𝑦 instead of 𝑥. It is evident the tree 𝜅𝜎 𝑥 meets all constraints characterising trees from 𝒯𝑁 . Moreover, 𝜇(𝜅𝜎 𝑥) = (ℛ𝑁 𝜅𝜎 )(𝜎𝑥) by construction of 𝜅𝜎 . Conjecture. The constructed above random system with output 𝜇 is a final random system with output and the constructed family of ℛ𝑁 -morphisms {𝜅𝜎 : 𝜎 → 𝜇 | 𝜎 : Coalgℛ𝑁 } is the family of anamorphisms. 5.3. Bisimulation of Systems with Output As it was said above, yet another important concept used for studying coalgebras is the concept of bisimulation. In general point of view, the concept was discussed in [15]. Proposition 4. A system with output 𝜌 is a bisimulation of systems with output 𝜎 and 𝜏 if the next is true 𝜌 ⊂ 𝜎 × 𝜏 (5a) (︁ )︁ (︂ )︂ 𝑛 𝑛 → 𝑥′ = ′ ′ (5b) ∑︀ Pr 𝑥 − Pr (𝑥, 𝑦) − → (𝑥 , 𝑦 ) 𝜎 𝑦 ′ ∈ 𝜎 |(𝑥′ ,𝑦 ′ )∈ 𝜌 𝜌 (︁ )︁ (︂ )︂ 𝑛 ′ 𝑛 ′ ′ (5c) ∑︀ Pr 𝑦 − →𝑦 = Pr (𝑥, 𝑦) − → (𝑥 , 𝑦 ) . 𝜏 𝑥′ ∈ 𝜏 |(𝑥′ ,𝑦 ′ )∈ 𝜌 𝜌 Proof. 𝜌 is a bissimulation of 𝜎 and 𝜏 iff the next diagramm commutes pr pr𝜏 𝜎  𝜎 𝜌 - 𝜏 𝜎 𝜌 𝜏 ? ℛ𝑁 pr𝜎 ℛ𝑁 pr𝜏 ? ? ℛ𝑁 𝜎  ℛ𝑁 𝜌 - ℛ𝑁 𝜏 or in other worlds, (5a) is evident and pr𝜎 and pr𝜏 are both ℛ𝑁 -morphisms. Thus, we can apply Prop. 3 for these mappings. It and Remark 4 give (5b) and (5c). 6. Conclusions Summarizing the above discussion, it can be argued that the study of the category of ℛ𝑁 - colgebras is interesting in the context of constructing semantic models for random discrete systems with output. Thanks to the methods described in this article we can solve the problem of the impossibility of full determinacy (deterministic) of a system that occurs in CPS. Based on this discussion, we can outline the following areas of research: Based on this discussion, we can outline the following areas of research • To develop the formal technique for specifying and analysing the final random system with output. This model should be less geometrical and more algebraical than the model given in Subsec. 4.1 and 4.2. • To prove the Conjecture of Subsec. 4.2 with basing this formal technique. • To construct an analogue of bifunctor 𝒥 introduced in [7, 8] as a tool for studying safety constraints and causality constraints by joining a system with output and a detector. • To construct a random analogue of a system with termination for defining indicators of system failures. • To give a probability-theoretic interpretation of system random properties recognised by the construction with use the analogue of bifunctor 𝒥 . • To extend the technique being developed to discrete distributed systems for the analysis of causality relations based on the logical clock model. References [1] G. Moore, No exponential is forever: but "forever" can be delayed! [semiconductor industry], in: 2003 IEEE International Solid-State Circuits Conference, 2003. Digest of Technical Papers. ISSCC., 2003, pp. 20–23 vol.1. doi:10.1109/ISSCC.2003.1234194. [2] A. D. Kshemkalyani, M. Singhal, Distributed Computing: Principles, Algorithms, and Systems, Cambridge University Press, 2008. [3] S. Tyszberowicz, D. Faitelson, Emergence in cyber-physical systems: potential and risk, Frontiers of Information Technology & Electronic Engineering 21 (2020) 1554–1566. [4] L. Lamport, Time, clocks, and the ordering of events in a distributed system, CACM 21 (1978) 558–565. [5] J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science 249 (2000) 3–80. [6] B. Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science, 2016. [7] G. Zholtkevych, M. Labzhaniia, Understanding Safety Constraints Coalgebraically, in: V. Lytvyn, et al. (Eds.), Computational Linguistics and Intelligent Systems, volume 2604 of CEUR Workshop Proceedings, 2020, pp. 1–19. [8] G. Zholtkevych, M. Labzhaniia, Coalgebraic Approach to Studying Discrete Systems with Output, in: A. Bollin, et al. (Eds.), Information and Communication Technologies in Education, Research, and Industrial Applications, volume 1308 of CCIS, Springer, Cham, 2021, pp. 141–165. [9] nLab authors, nLab, http://ncatlab.org/nlab/, 2021. Revision 286. [10] E. A. Lee, Cyber physical systems: Design challenges, in: 2008 11th IEEE International Sym- posium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), 2008, pp. 363–369. doi:10.1109/ISORC.2008.25. [11] I. Grobelna, Formal verification of control modules in cyber-physical systems, Sensors (Basel, Switzerland) 20 (2020) 5154. doi:10.3390/s20185154. [12] C. André, Syntax and semantics of the clock constraint specification language (ccsl), [Research Report] (2009). [13] T. Gu, F. Zanasi, Coalgebraic semantics for probabilistic logic programming, Logical Methods in Computer Science 17 (2021). URL: https://arxiv.org/pdf/2012.03916.pdf. [14] B. Jacobs, From Probability Monads to Commutative Effectuses, Journal of Logical and Algebraic Methods in Programming 94 (2018) 200–237. [15] B. Jacobs, J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bulletin 62 (1997) 62–222.