=Paper=
{{Paper
|id=Vol-3013/20210296
|storemode=property
|title=Coalgebraic Understanding of Random Systems with Output
|pdfUrl=https://ceur-ws.org/Vol-3013/20210296.pdf
|volume=Vol-3013
|authors=Artem Panchenko,Grygoriy Zholtkevych
|dblpUrl=https://dblp.org/rec/conf/icteri/PanchenkoZ21
}}
==Coalgebraic Understanding of Random Systems with Output==
https://ceur-ws.org/Vol-3013/20210296.pdf
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.