=Paper= {{Paper |id=Vol-3730/paper15 |storemode=property |title= Petri nets in Modeling Glucose Regulating Processes in the Liver |pdfUrl=https://ceur-ws.org/Vol-3730/paper15.pdf |volume=Vol-3730 |authors=Kamila Barylska,Anna Gogolińska |dblpUrl=https://dblp.org/rec/conf/apn/BarylskaG24a }} == Petri nets in Modeling Glucose Regulating Processes in the Liver== https://ceur-ws.org/Vol-3730/paper15.pdf
                         Petri Nets in Modeling Glucose Regulating Processes in
                         the Liver
                         Kamila Barylska1 , Anna Gogolińska1
                         1
                             Nicolaus Copernicus University in Toruń


                                        Abstract
                                        Diabetes is a chronic condition, considered one of the civilization diseases, that is characterized by sustained
                                        high blood sugar levels. There is no doubt that more and more people is going to suffer from diabetes, hence it is
                                        crucial to understand better its biological foundations. The essential processes related to the control of glucose
                                        levels in the blood are: glycolysis (process of breaking down of glucose) and glucose synthesis, both taking
                                        place in the liver. The glycolysis occurs during feeding and it is stimulated by insulin. On the other hand,
                                        the glucose synthesis happens during fasting and it is stimulated by glucagon. In the paper we present a Petri
                                        net model of glycolysis and glucose synthesis in the liver. The model is created based on medical literature.
                                        Standard Petri nets’ techniques were used to analyse the properties of the model: traps, reachability graphs,
                                        tokens dynamics, deadlocks analysis. The results are described in the paper. Our analysis shows that the model
                                        captures the interactions between different enzymes and substances, which is consistent with the biological
                                        processes occurring during fasting and feeding. The model constitutes the first element of our long-time goal to
                                        create the whole body model of the glucose regulation in a healthy human and a person with diabetes.

                                        Keywords
                                        diabetes, glycolysis, glycogenesis, bioinformatics, Petri nets, modelling




                         1. Introduction
                         Diabetes is a chronic disease that occurs either when the pancreas does not produce enough insulin
                         (a hormone that regulates blood glucose) or when the body cannot effectively use the insulin it produces.
                         Diabetes is considered one of the civilization diseases. According to International Diabetes Federation
                         data for 2021 [28] and IDF Diabetes Atlas [27], one in ten people in the world, that is, approximately, 537
                         million adults (20-79 years), are living with diabetes. The total number of people living with diabetes is
                         projected to rise to 643 million by 2030 and 783 million by 2045. It is estimated that 6.7 million adults
                         died from diabetes or its complications in 2021, which means 1 death every 5 seconds. Diabetes was
                         responsible for at least $966 billion in health expenditure in 2021, which is 9% of the global total spent
                         on healthcare.
                            It is therefore not surprising, that in many fields of science intensive work has been undertaken
                         not only to cure the disease, but also, and perhaps above all, to prevent or delay its future health
                         complications (such as heart disease, chronic kidney disease, nerve damage, and other problems with
                         feet, oral health, vision, hearing, and mental health) or improving the quality of life of patients and
                         their families.
                            More and more advanced systems are being developed to continuously measure blood glucose levels
                         without the need to puncture the skin (CGM - continuous glucose monitoring [8, 2]), the insulin pump
                         industry has been developing rapidly. Closed loop systems (so called artificial pancreas), enabling
                         automatic insulin delivery by the pump, were also created and operate successfully, both as a commercial
                         solution (a.o. MiniMed 780G System [30], Tandem Tslim Control IQ [31], CamAPS FX [26]), or developed
                         on a DIY basis (a.o. AAPS [25], Loop [29]). Countless applications are being developed for diabetics
                         and their families, as well as health care professionals, such as bolus calculators, applications for
                         counting food nutritional value, diabetes management, statistics and many others. Intensive work is
                         also underway on the use of artificial intelligence in this field [12, 11, 7]. However, we have noticed that
                         most non-medical solutions focus on solving a particular problem without offering a broader view of
                          PNSE’24, International Workshop on Petri Nets and Software Engineering, 2024
                          " leii@mat.umk.pl (A. Gogolińska)
                                     © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings

                                                                                                              261
Kamila Barylska et al. CEUR Workshop Proceedings                                                       261–269


diabetes. On the other hand, medical papers usually focus on one single element of the whole process
of glucose regulation for healthy and diabetic people. Therefore, there exists a great need for a more
holistic approach, which recently became more and more popular.
   Our long-term goal is to create a simple and intuitive mathematical model representing the changes
occurring in the body of a healthy person and a person with diabetes. This model should be easily
analysable and clear, but at the same time capable of representing complex processes consisting of
interactions between many components. In our opinion, Petri nets (PNs) constitute a perfect tool for this
purpose. Due to PNs intuitive graphical representation and mathematical properties, the model would
be useful for people with and without medical background. This could allow for a better understanding
of the processes occurring in a human body, predicting new therapeutic targets and designing drug
therapies. We are aware, that our goal (modelling the entire process) is ambitious and would not be
reached at once. Hence, our first step, presented below, is to model the glycolysis process in the liver.
The medical basis of our model is taken from [20].
   Glycolysis is the pathway of breakdown of glucose into pyruvate following glucose uptake by cells.
It is an ancient metabolic pathway, meaning that it evolved long ago, and it is found in the great
majority of organisms alive today[14]. The process is highly important in maintaining the homeostasis
of glucose levels in the body of a healthy person, especially the glycolysis that occurs in the liver. For
that reason we start modelling diabetes from this process. Our model allows to scrupulously follow the
glycolysis process in a healthy person, as well as to analyse what happens in an organism in which
insulin secretion is disturbed or completely absent. Insulin and glucagon are hormones produced and
released by the pancreas to regulate blood sugar levels. Insulin is released by the beta cells of the
pancreas and reduces blood sugar levels while glucagon is released by the alpha cells of the pancreas
and increases blood sugar levels. The two hormones are responsible for maintaining homeostasis of
blood glucose levels. An increase in blood glucose levels triggers the release of insulin which promotes
glycolysis, while when glucose levels decrease, glucagon is released to stimulate the opposite process.
   In this paper, we present a model of the glycosite and the opposite process in the liver designed using
Petri nets. We also use standard Petri nets’ analysis tools, such as the reachability graph, to study it. In
the following section, we recall the basic concepts of Petri nets, and in subsequent parts of the paper we
introduce created Petri net, modeling the processes occurring in the liver, and then conduct an analysis
of it. The paper ends with a summary and future plans.


2. Preliminaries
In this section we recall the basic notions concerning Petri nets and its properties [4, 10, 15, 16, 9].
   A finite labelled transition system with initial state is a tuple 𝑇 𝑆 = (𝑆, →, 𝑇, 𝑠0 ) with nodes 𝑆 (a finite
set of states), edge labels 𝑇 (a finite set of letters), edges → ⊆ (𝑆 × 𝑇 × 𝑆), and an initial state 𝑠0 ∈ 𝑆.
A label 𝑡 is enabled at 𝑠 ∈ 𝑆, denoted by 𝑠[𝑡⟩, if ∃𝑠′ ∈ 𝑆 : (𝑠, 𝑡, 𝑠′ ) ∈ →. A state 𝑠′ is reachable from 𝑠
through the execution of 𝜎 ∈ 𝑇 * , denoted by 𝑠[𝜎⟩𝑠′ , if there is a directed path from 𝑠 to 𝑠′ whose edges
are labelled consecutively by 𝜎. The set of states reachable from 𝑠 is denoted by [𝑠⟩. A sequence 𝜎 ∈ 𝑇 *
is allowed, or firable, from a state 𝑠, denoted by 𝑠[𝜎⟩, if there is some state 𝑠′ such that 𝑠[𝜎⟩𝑠′ .
   An (initially marked) Petri net (PN) is denoted as 𝑁 = (𝑃, 𝑇, 𝐹, 𝑀0 ) where 𝑃 is a finite set of places,
𝑇 is a finite set of transitions, 𝐹 is the flow function 𝐹 : ((𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 )) → N specifying the
arc weights, and 𝑀0 is the initial marking (where a marking is a mapping 𝑀 : 𝑃 → N, indicating the
number of tokens in each place). A transition 𝑡 ∈ 𝑇 is enabled at a marking 𝑀 , denoted by 𝑀 [𝑡⟩,
if ∀𝑝 ∈ 𝑃 : 𝑀 (𝑝) ≥ 𝐹 (𝑝, 𝑡). The firing of 𝑡 leads from 𝑀 to 𝑀 ′ , denoted by 𝑀 [𝑡⟩𝑀 ′ , if 𝑀 [𝑡⟩ and
𝑀 ′ (𝑝) = 𝑀 (𝑝) − 𝐹 (𝑝, 𝑡) + 𝐹 (𝑡, 𝑝). This can be extended, as usual, to 𝑀 [𝜎⟩𝑀 ′ for sequences 𝜎 ∈ 𝑇 * ,
and [𝑀 ⟩ denotes the set of markings reachable from 𝑀 . We call a marking 𝑀 deadlock if it does not
enable any transition, i.e. for every 𝑡 ∈ 𝑇 we have ∃𝑝 ∈ 𝑃 : 𝑀 (𝑝) < 𝐹 (𝑝, 𝑡). The reachability graph
𝑅𝐺(𝑁 ) of a bounded (such that the number of tokens in each place does not exceed a certain finite
number) Petri net 𝑁 is the labelled transition system with the set of vertices [𝑀0 ⟩, initial state 𝑀0 ,
label set 𝑇 , and set of edges {(𝑀, 𝑡, 𝑀 ′ ) | 𝑀, 𝑀 ′ ∈ [𝑀0 ⟩ ∧ 𝑀 [𝑡⟩𝑀 ′ }.



                                                      262
Kamila Barylska et al. CEUR Workshop Proceedings                                                                   261–269


                                          𝑝
                                                                        𝑀0       𝑎

                                      𝑎              𝑏       𝑐              𝑐          𝑐
                                                                                  𝑏




Figure 1: A Petri net and its reachability graph.


   Let 𝑥 ∈ 𝑃 ∪ 𝑇 , ∙ 𝑥 = {𝑦 ∈ (𝑃 ∪ 𝑇 ) | (𝑦, 𝑥) ∈ 𝐹 }⋃︀and 𝑥∙ = {𝑦 ∈ (𝑃 ⋃︀    ∪ 𝑇 ) | (𝑥, 𝑦) ∈ 𝐹 }. We extend
this notation to sets: for 𝑆 ⊆ 𝑃 ∪ 𝑇 , we have ∙ 𝑆 = 𝑥∈𝑆 ∙ 𝑥 and 𝑆 ∙ = 𝑥∈𝑆 𝑥∙ . Let 𝑆 be a non-empty
subset of places. We call 𝑆 ⊆ 𝑃 a trap if 𝑆 ∙ ⊆∙ 𝑆. The following property follows directly from the
definition: once a trap is marked under some marking, it is always marked at the subsequent markings
reachable from this one.
   Note that the reachability graph of a bounded Petri net captures the exact information about the
reachable markings of the net, and therefore reflects the entire behaviour of a given net. Figure 2 depicts
a Petri net, together with its reachability graph. Reachability graphs of real biological systems are
usually quite large and therefore difficult to analyse. To deal with this inconvenience, we use reduced
reachability graphs, called stubborn reduced reachability graphs, created on the basis of partial order
reduction techniques, where not all interleaving sequences of concurrent behaviour are considered.
As a result of the reduction only a subset of the complete reachability graph is constructed, nevertheless
it still allows the discussion of certain properties, in particular: it preserves all deadlock states and the
whole cyclic behaviour.
The reduction of a reachability graph to a stubborn reduced reachability graph proceeds as follows:
      1. For a given marking, determine a set of "independent" transitions (called stubborn set), such
         that their behaviour cannot be influenced by any transitions from the complement of this set
         (i.e. excluded transitions). Additionally, the following conditions must hold: any sequence of
         excluded transitions cannot enable or disable an included transition (hence their firing can be
         postponed) and the set contains at least one enabled transition.
      2. Compute a stubborn reduced reachability graph, using a variation of a standard algorithm: at each
         marking (node), instead of firing all enabled transitions, only transitions of a stubborn set are
         fired.
The notion of stubborn sets capture the lack of interaction between transitions, and such excluded
transitions may not be interesting from our point of view (for instance in case of biological systems).
Executions of transitions from outside a stubborn set could be postponed because it does not affect the
merits of the system’s behaviour1 .


3. Model
Our Petri net model, presented in Figure 2, represents the process of glycolysis and the opposite activity
in a liver described in [20]. It contains 17 places and 13 transitions.
   Homeostasis is the state of steady chemical conditions maintained by organism. In our paper we
focuse on the glucose homeostasis. There are three basic organs of the human body that control the
level of glucose: the pancreas, the liver and the fat tissue. The goal of our PN model is to represent
the processes occurring in the liver that control the level of glucose. Two basic processes are present,
namely: glycolysis and synthesis of glucose.

1
    Due to lack of space, we do not provide detailed definitions and properties here, interested readers are referred to the
    literature (a.o. [17], [18], [6], [21]).



                                                             263
Kamila Barylska et al. CEUR Workshop Proceedings                                                     261–269


   The glycolysis in the liver is stimulated by the presence of insulin and glucose, which physiologically
is associated with feeding. Those substances, in the PN model, are represented by places: Insulin and
Glucose respectively. The presence of insulin activates various protein phosphatases (place PP). It results
in an increase in the expression of glucokinase (place GK) and leads to increasing the kinase activity
of complex 6PFK2/FBPase2 (place Kin) and to decreasing the phosphatase activity of 6PFK2/FBPase2
(place Pho). As a result of kinase activity of 6PFK2/FBPase2, the level of fructose-2,6-bisphosphate
(F2,6P2) is increasing (place F26P2), leading to an elevation of 6-phosphofructo-1-kinase (6PFK1) activity
(place a6PFK1) and a reduction of fructose-1,6-bisphosphatase (FBPase) activity (place nFBPase). All those
changes cause an increase in glycolysis rates. The glycolysis is represented by the part of the net (places
and transitions) leading from place Glucose, through place F6P to place Pyruvate, which represents the
final product of the glycolysis. Long after the feeding, during the fasting time, the levels of glucose and
insulin in the blood are very low. It provokes a production of glucagon by the pancreas. The presence of
this enzyme is represented by place Glucagon. By the signal cascade, (places cAMP and PKA), glucagon
alters the level of glucokinase and of phosphorylation of complex 6PFK2/FBPase2. It results in an
increase of the phosphatase activity of 6PFK2/FBPase2 (place Pho) and a decrease of the kinase activity
of 6PFK2/FBPase2 (place Kin). The phosphatase activity of 6PFK2/FBPase2 causes a decrease of F2,6P2
level (place mF26P2). It leads to a reduction of 6PFK1 activity (place n6PFK1) and an elevation of FBPase
activity (place aFBPase). Those enzymes inhibit the glycolysis process and stimulates the synthesis of
glucose from pyruvate.

          Glucagon                                         Glucose                      Insulin


                                                𝑡5           𝑡6

                                                                                   GK               𝑡3
     𝑡0


                                                           F6P
                                                                                               PP
          cAMP
                                          𝑡11                          𝑡12



                                                Pyruvate                           aFBPase
     𝑡1
                      a6PFK1

                               𝑡9                                                  nFBPase
          PKA                                                            𝑡10                        𝑡4


                      n6PFK1
                                                     F26P2

                 𝑡2                 𝑡7
                                                                                   𝑡8



                                         Pho               mF26P2                                   Kin
Figure 2: The PN model representing the process of maintaining a glucose homeostasis by the liver. During
feeding, when the levels of glucose and insulin are high, and glucagon is not present, the glycolysis occurs.
During fasting, when the level of glucagon is high, the synthesis of glucose occurs.


   Notice, that markings of places Insulin, Glucose and Glucagon have the greatest impact on the
dynamics of the model. Markings of other places, associated with different enzymes and sub-
stances like 6PFK2/FBPase2 (places Kin and Pho), F26P2 (places F26P2, nF26P2), 6PFK1 (places
a6PFK1, n6PFK1) and FBPase (places aFBPase, nFBPase), would be established according to the
presence of insulin and glucose or glucagon. This could happen because those places are in-



                                                     264
Kamila Barylska et al. CEUR Workshop Proceedings                                                     261–269


cluded in different traps. There are eight traps in the model: {𝐾𝑖𝑛, 𝑃 ℎ𝑜}, {𝐹 26𝑃 21, 𝑚𝐹 26𝑃 2},
{𝑎6𝑃 𝐹 𝐾1, 𝑛6𝑃 𝐹 𝐾1}, {𝑎𝐹 𝐵𝑃 𝑎𝑠𝑒, 𝑛𝐹 𝐵𝑃 𝑎𝑠𝑒}, {𝑛6𝑃 𝐹 𝐾1, 𝑛𝐹 𝐵𝑃 𝑎𝑠𝑒}, {𝑎6𝑃 𝐹 𝐾1, 𝑎𝐹 𝐵𝑃 𝑎𝑠𝑒},
{𝑃 ℎ𝑜, 𝐺𝐾}, {𝐺𝑙𝑢𝑐𝑜𝑠𝑒, 𝐹 6𝑃, 𝑃 𝑦𝑟𝑢𝑣𝑎𝑡𝑒}. It means that if at least one of the place from a trap is
marked, the token would not leave the trap. Hence, if 6PFK1 is less active – we observe less tokens in
place a6PFK1, and at the same time more tokens in place n6PFK1. This behaviour is consistent with the
actual biological processes. The same holds for each trap. Transitions which transfer tokens among the
places included in the traps are affected by markings of places Insulin, Glucose and Glucagon. Those
markings in our analysis are fixed in the initial marking. Nevertheless, in the more extended model
of glucose regulation (which is our final goal) markings of places Insulin, Glucose and Glucagon would
arise from activity of particular parts of the model. Especially, in the case of diabetics, by endogenous
(produced in the pancreas) and exogenous (provided from the outside) insulin supply. In the current
state of the model those markings are set by hand.
   The reachability graph of the net depicted in Figure 2 (created using [24]) contains 162 states with
702 arcs. The graph is presented in Figure 3, but due to its size it is too big to be depicted properly.
Moreover, because of the size of the graph, it is difficult to grasp and observe the fundamental dynamic
processes present the model, which is our goal in this phase of the analysis.




Figure 3: The reachability graph obtained for the PN model with the initial marking presented in Figure 2 with
a slight change: place Glucose contains 1 token. Created using [24].


   For that reason, from now on, to study the behaviour of our model, we use reachability graphs obtained
according to stubborn reduction (described in Preliminaries), computed by [21]. Note, that such graphs’
properties are sufficient for the analysis of our model, making it easier and more transparent.
   As mentioned above, the PN model represents the two basic processes of glucose homeostasis in the
liver: glycolysis and synthesis of glucose. Those processes in a human body occur alternately, one after
the other. Hence, two kinds of initial markings of the PN model are possible. The first – associated
with the feeding state, and the second – with the fasting. We may start our analysis from any of those
two. Let us begin with the model in the feeding phase. This results in the presence of glucose and
insulin, and consequently, in the initial marking, places associated with those substances are marked.
In a human body, in such a situation, the level of glucagon is very low (in comparison to glucose and
insuline) and in the model it is simply omitted. As mentioned above, markings of other places would be
set according to the presence of glucose and insulin, we just have to make sure that at least one place of
the each trap is marked.



                                                     265
Kamila Barylska et al. CEUR Workshop Proceedings                                                          261–269


   The initial marking corresponding to the feeding phase is presented in Figure 2. For that marking, the
stubborn reduced reachability graph is generated and depicted in Figure 4. One can easily notice, that
every sequence of transitions executions ends up in the (black) deadlock marking. Hence, we always
start with tokens present in places representing glucose and insulin, and eventually, those places are
emptying, and the place representing pyruvate becomes marked. It indicates that glycolysis happened.
Obviously, someone might notice, that the presence of one or two tokens is not representative for the
modelling of biological processes. Usually, in biological models, the number or value of tokens existing
in a place, corresponds to the level of the substance associated to the given place. The marking depicted
in Figure 2 is chosen only for the illustration and to obtain a relatively small reachability graph. We
have performed also analysis with higher numbers of tokens in initial markings. The behaviour of
the model is very similar to the case of the marking in Figure 2 – each execution results in a deadlock
marking, where places Insulin and Glucose are empty and place Pyruvate contains the same number
of tokens as place Glucose in the initial marking. It indicates that the process of glycolysis has been
accomplished. Since the reachability graphs for Petri nets with significantly larger initial markings are
too large to be shown and analysed here, we present the plot depicting the changes of the markings of
the crucial places - Figure 5.




Figure 4: The reachability graph obtained for the PN model with the initial marking presented in Figure 2. The
initial marking is located top left and depicted blue, while the final (deadlock) marking is on the right corner of
the figure (depicted black). Created using [21].


   After the feeding is finished, the fasting state starts, which means that the food from the environment
is (temporarily) not more provided, and the level of glucose in the blood is declining. In that state of the
organism, the pancreas is not producing insulin. When the level of glucose is low, the body is forced to
use its own stored substances to ensure its suitable level in the blood. To obtain that goal, the pancreas
starts to produce glucagon, and other organs, especially the liver, react to the presence of glucagon.
This situation is represented in our PN model as the deadlock marking obtained after the feeding,
with additional tokens added to place Glucagon. As the result, the initial marking of the PN model to
represent the fasting phase would consist of: tokens in place Glucagon and tokens in place Pyruvate,
empty place Glucose and empty place Insulin – during fasting the level of insulin would be much lower
than the level of glucagon and in the model it is omitted for simplification. Markings of other places are
not that crucial as long as the each trap contains a token. Figure 6 depicts the reachability graph of the
PN model presented in Figure 2, but with a different initial marking determined as follows: places are
marked as in the deadlock marking from Figure 4 with two additional tokens in place Glucagon.



                                                       266
Kamila Barylska et al. CEUR Workshop Proceedings                                                         261–269




Figure 5: Changes in markings of places Glucose (red), Pyruvate (blue) and Insulin (green) in the feeding phase.
In the initial marking places Glucose and Insulin contained each 100 tokens. At the end of model dynamic
simulation place Glucose contains zero tokens, and Pyruvate contains 100 tokens. Created using [13, 22].




Figure 6: The reachability graph calculated for the PN model with the initial marking obtained from the dead-
lock marking, which is the final marking for the net in Figure 2 and two tokens added to place Glucagon. The
initial marking is located top right and depicted orange, while the final (deadlock) marking is on the left bottom
corner of the figure (depicted black). Created using [21].



  Like in the previous case, each execution results in the deadlock marking. In the initial marking,
places Glucagon and Pyruvate are marked, in the deadlock marking, places Glucagon and Pyruvate are
empty and place Glucose contains the same number of tokens as Pyruvate in the initial marking. It
corresponds to the process of glucose synthesis.
  Like above, we have also analysed the dynamic of the PN model with larger number of tokens in initial
markings. The changes of number of tokens in places Glucose, Pyruvate and Glucagon are depicted in



                                                       267
Kamila Barylska et al. CEUR Workshop Proceedings                                                    261–269


Figure 7. It is easy to observe that the number of tokens representing the level of glucose is increasing,
while the number of tokens representing the level of pyruvate is deceasing. At the end of dynamics
simulation, eventually there are as many tokens in Glucose as there were in Pyruvate in the initial state.
The behaviour of the PN model with larger numbers of tokens is consistent with the behaviour of the
model with the smaller one. The deadlock marking obtained after the fasting phase can be afterwards
used as the initial marking for the simulation of the feeding and the next cycle of feeding and fasting
can start.




Figure 7: Changes in markings of places Glucose (red), Pyruvate (blue) and Glucagon (green) in the fasting
phase. In the initial marking places Pyruvate and Glucagon contained 100 tokens each. At the end of places
dynamics simulation place Pyruvate contains zero tokens, and Glucose contains 100 tokens. Created using [22].




4. Conclusions and Future Work
The paper constitutes the first step towards designing a model representing the regulation of glucose
levels in the body, which would aim to better understand the processes occurring in the body of a healthy
person, as well as a person suffering from diabetes. As the first step, we model (with the use of Petri
nets) glucose regulating processes in the liver. Two basic processes have been included in our model:
glycolysis during the feeding phase and synthesis of glucose during the fasting phase. The model
preserves the interactions between those processes, as shown in Section 3.
   We are aware that we are setting an ambitious goal and that subsequent steps towards it may
require the use of more advanced tools, such as extensions to Petri nets (for instance: stochastic Petri
nets, continuous Petri nets, fuzzy Petri nets, see [1, 5, 3]). In the future, we also plan to verify our
model (process modelling) and use it to find regularities and irregularities in the functioning of an
unhealthy body. We hope that the consequence of our actions will be greater awareness of diabetes and
improvement of the physical and mental condition of people suffering from it.


References
 [1] Ajmone Marsan, M.: Stochastic Petri nets: An elementary introduction, Lecture Notes in Computer
     Science, vol 424, 1990.
 [2] Battelino T., Alexander C.M., Amiel S.A., Arreaza-Rubin G., Beck R.W. , Bergenstal R.M., Bucking-
     ham B.A., Carroll J., Ceriello A, Chow E., Choudhary P., Close K., Danne T., Dutta S., Gabbay R.,
     Garg S., Heverly J., Hirsch I.B., Kader t., Kenney J., Kovatchev B., Laffel L., Maahs D., Mathieu C.,



                                                    268
Kamila Barylska et al. CEUR Workshop Proceedings                                                   261–269


     Mauricio D., Nimri R., Nishimura R., Scharf M., Del Prato S., Renard E., Rosenstock J., Saboo B.,
     Ueki K., Umpierrez G.E., Weinzimer S.A., Phillip M.: Continuous glucose monitoring and metrics
     for clinical trials: an international consensus statement, The Lancet Diabetes & Endocrinology,
     2023.
 [3] Cardoso J, Valette R., Dubois D.: Fuzzy Petri Nets: An Overview, IFAC Proceedings Volumes, 1996.
 [4] Desel J, Reisig W.: Place/transition Petri Nets, Lectures on Petri Nets, Vol. I: Basic Models, Advances
     in Petri Nets, 1491, 1998.
 [5] Fraca E., Haddad S: Complexity Analysis of Continuous Petri Nets, Application and Theory of
     Petri Nets and Concurrency, Lecture Notes in Computer Science, vol 7927, 2013
 [6] Heiner M., Schwarick M., Wegener J.-T.: Charlie - An Extensible Petri Net Analysis Tool, Petri
     Nets 2015, 2015
 [7] Jin X., Cai A., Xu T., Zhang X.: Artificial intelligence biosensors for continuous glucose monitoring,
     Interdisciplinary Materials, 2023.
 [8] Lee I., Probst D., Klonoff D., Sode K.: Continuous glucose monitoring systems - Current sta-
     tus and future perspectives of the flagship technologies in biosensor research, Biosensors and
     Bioelectronics, 2021.
 [9] Liu GY., Barkaoui K.: A survey of siphons in Petri nets. Information Sciences 363. 2016.
[10] Murata T.: Petri nets: Properties, analysis and applications, Proceedings of the IEEE, vol. 77, no. 4,
     1989.
[11] Nitesh P., Geeta R., Vijaypal S. D., Ramesh C. P.: Diabetes prediction using artificial neural network,
     Deep Learning Techniques for Biomedical and Health Informatics, Academic Press, 2020.
[12] Prakash E. P., Srihari K., S. Karthik, Kamal M. V., Dileep P., Bharath Reddy S., Mukunthan M. A.,
     Somasundaram K., Jaikumar R., Gayathri N., Kibebe Sahile: Implementation of Artificial Neural
     Network to Predict Diabetes with High-Quality Health System. Computational Intelligence and
     Neuroscience, vol. 2022, Article ID 1174173, 2022.
[13] Radom M. et al.: Holmes: A graphical tool for development, simulation and analysis of Petri net
     based models of complex biological systems, Bioinformatics 33.23, 2017.
[14] Raven, P. H., G. B. Johnson, K. A. Mason, J. B. Losos, and S. R. Singer. "How cells harvest energy."
     In Biology. 10th ed. AP ed. (New York, NY: McGraw-Hill, 2014), 129. Raven P. H.; Johnson G. B.;
     Mason K. A.; Losos J. B.; Singer S. R.: How cells harvest energy, In Biology 10th ed., 2014.
[15] Reisig W: Petri Nets. An Introduction, Part of the book series: Monographs in Theoretical Computer
     Science, 1985.
[16] Starke P: Petri-Netze, VEB Deutscher Verlag der Wissenschaften, 1980.
[17] Valmari A.: Error detection by reduced reachability graph generation. Proceedings of the 9th
     European Workshop on Application and Theory of Petri Nets, 1988.
[18] Valmari A.: A Stubborn Attack on State Explosion, Formal Methods in System Design, 1992.
[19] Valmari A., Hansen H.: Stubborn Set Intuition Explained, Transactions on Petri Nets and Other
     Models of Concurrency XII., vol 10470, 2017.
[20] Xin G., Honggui L., Hang X., Shihlung W., Hui D., Fuer L., Alex J. L., Chaodong W.: Glycolysis in
     the control of blood glucose homeostasis, Acta Pharmaceutica Sinica B, Volume 2, Issue 4, 2012.
[21] Charlie, https://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Charlie
[22] Holmes, http://www.cs.put.poznan.pl/mradom/Holmes/index.html
[23] Pipe2, https://pipe2.sourceforge.net/
[24] Snoopy, https://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Snoopy
[25] AAPS, https://androidaps.readthedocs.io/en/latest/
[26] CamAPS FX, https://camdiab.com/
[27] Diabetes Atlas, https://diabetesatlas.org/
[28] International Diabetes Federation, https://federation idf.org
[29] Loop, https://loopkit.github.io/loopdocs/
[30] MiniMed 780G System, https://www.medtronic-diabetes.com/en-gb/minimed-780g-system-info
[31] Tandem Tslim Control IQ https://www.tandemdiabetes.com/en-gb/home




                                                    269