The safety concept for clock constraints has already been coalgebraically studied for fully deterministic 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 deterministic 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.
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, [
Herein distributed system is a collection of independent entities that cooperate to solve a
problem that cannot be individually solved [
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 [
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
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-efect relationship between events in the system. It is good to take into account
the cause-and-efect approach and that it is possible to use only the logical clocks model in
distributed systems during the synchronisation of its elements [
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 [
The main shortcoming of the solutions proposed above [
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.
The approach whereby we use logical rules to verify the work of CFS is suficiently 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.
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.
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 diferent 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-efect) 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.
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-efect relationship between events. One
possible solution to this problem is to build coalgebraic models. This is primarily because of the
induction principle [
In addition to the studies described above [
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].
Let and be -coalgebras then a morphism : → is called an
?
commutes or, equivalently, the equation ( ) = holds. morphism from into (symbolically, : → ) if the diagram
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 [
? pr
pr
? pr
? pr- commutes.
Final objects of category of coalgebras are very important for constructing semantic models of programming and specification languages.
denoted by .
A terminal object of Coalg if it exists is called a final -coalgebra, which is 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 [
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 }︃
: → [
⃒ ∈ Now for any mappings : → , let us define : → as follows = . ∈ .
∑︁ ∈|=
().
Of course, we need to check (-mor) specifies an element of . Indeed, and 0 ≤ (︀ ( ))︀ () =
∑︁ ∈|= () ≤ ∑︁ () = 1 ∈ ∑︁ (︀ ( ))︀ () = ∑︁ ∈ ∑︁
() = ∑︁ () = 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.
Further, for →− →− , Proof. For any set , we have evidently ( id ) = ∈ . () = i.e. id = id .
⎛ ︀( ()( ))︀ = ()(︀ ( ))︀ = () ⎝ ∈ . (-obj) (-mor) = ∈ . = ∈ . = (︀ ( ))︀ .
∈ |()= ∑︁ ∑︁ ⎛ ⎝ ∈ . ⎛
∑︁ ⎝ ∈ |()= ∈|= Thus, is an endofunctor of Set.
∑︁ ∈|= ∑︁
⎞ ()⎠
⎞ ()⎠ () ∈|=
⎞ ()⎠ = ∈ .
∑︁ ∈|(())= ()
Let us take two sets and then we have the universal arrow − − ← pr × →−− pr 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 [
We use the idea of randomization for obtaining random systems with output.
More precisely, let us consider the endofunctor ℛ of Set defined as follows
ℛ = ( ) = ( × ) for any set
ℛ = ( ) = (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.
(ℛ -obj)
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 [
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 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 as the root label
with as the root label
with as the root label 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. coalgebras. from into if
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 ℛ Proposition 3. For systems with output and , a mapping : → is an ℛ -morphism ︀( ( ))︀ (, ) =
∑︁ ′∈ |′= ( )(, ′) whenever ∈ and ∈ .
Proof. The mapping is an ℛ -morphism if the next diagram commutes 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. Using this denotation, one can rewrite formula (3) as follows ( )(, ′) = Pr ︁( →− ′ .
︁) Pr →− ︁) = ︁(
∑︁ ′∈ |′=
Pr ︁( →− ′ .
︁) ? (ℛ ) = or, in other words, the next equation holds.
Therefore, let us compute the left and right sides of (4a).
For the left side, we have
︁( (︀ (ℛ ) )︀ ︁) (, ) = (︀ (ℛ )( ))︀ (, ) And for the right side, we have ︁( (︀ )︀ ︁) (, ) = (︀ ( ))︀ (, ).
= (︀ (id × )( ))︀ (, ) = ( )(, ′).
(4b) ∑︁ ′∈ |′= (3) (4a) (4c) (3* ) is a category, which is denoted by Coalgℛ .
Due to general theory, the class of random systems with output equipped with ℛ -morphism from as follows Example 2. Let be a random system with output then for any ∈ , one can build a tree 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 .
Moreover, ( ) = (ℛ )( ) by construction of .
It is evident the tree meets all constraints characterising trees from . family of anamorphisms.
Conjecture. The constructed above random system with output is a final random system with output and the constructed family of ℛ -morphisms { : → | : Coalgℛ } is the 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
Pr ︁( →− ′ =
︁) ︁(
︁) Pr →− ′ = ∑︀ ∑︀ ′∈ |(′,′)∈ ′∈ |(′,′)∈ ⊂ × ︂( ︂( Pr (, →)− (′, ′) Pr (, →)− (′, ′) .
︂) ︂) (5a) (5b) (5c) Proof. is a bissimulation of and if the next diagramm commutes ? Prop. 3 for these mappings. It and Remark 4 give (5b) and (5c). or in other worlds, (5a) is evident and pr and pr are both ℛ -morphisms. Thus, we can apply
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 [
[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 Symposium 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 Efectuses, 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.