Diabetes is a chronic disease of civilization, characterized by a constant elevated concentration of glucose in the blood. Many processes are involved in the glucose regulation, and their interactions are very complex. To better understand those processes we set ourselves a goal to create a Petri net model of the glucose regulation in the whole body. So far we have managed to create a model of glycolysis and synthesis of glucose in the liver, and the general overview models of the glucose regulation in a healthy and diabetic person. In this paper we introduce Petri net models of insulin secretion in -cell of the pancreas, and glucagon in the pancreas -cells. Those two hormones have mutually opposite efects: insulin preventing hyperglycemia, and glucagon preventing hypoglycemia. Understanding the mechanisms of insulin and glucagon secretion constitutes the basis for understanding diabetes. We also present a model in which both processes occur together, depending on the blood glucose level. The dynamics of each model are analysed. Additionally, we transform the overall insulin and glucagon secretion system to a Boolean network, following standard transformation rules.
Maintaining energy balance is a fundamental goal of every living organism. Energy requirements are determined by many factors: body size, level of physical activity, age. It also depends on external conditions in which the body functions require constant adaptation to changes. These energy-consuming processes, e.g., maintaining a constant body temperature when the ambient temperature drops, require continuous access to an energy source, which is glucose.
Energy is derived from the oxidation of carbohydrates, fats, and proteins. At the cellular level, glucose is the primary fuel for energy production. Therefore, its concentration in the bloodstream is maintained within a specific range, not lower than 70 mg/dl and not higher than 140 mg/dl. It represents a constant balance between glucose entering the blood, primarily from the gut after meals, and from the liver, as well as glucose uptake by peripheral tissues. The central nervous system continuously consumes up to 60% of the glucose resources in the blood, so the blood glucose level is tightly regulated to ensure adequate glucose delivery to the brain. Peripheral tissues, especially muscles, take up 50% of an oral glucose load (after meals), and at the same time, the glucose is released by the liver. This fuel and energy homeostasis is regulated by the neuroendocrine system. This process occurs on various levels, where the central and autonomic nervous systems play a dominant, integrative role. Disruptions in the metabolic balance of the body regarding glucose metabolism regulation generate many diseases. When the blood glucose level is too high, increasing can lead to the development of diseases, one of which is diabetes. On the other hand, when blood glucose levels are too low, they can disrupt the functioning of the central nervous system (CNS). During prolonged hypoglycemia (below 40 mg/dl), severe impairment of consciousness and damage to CNS cells may occur. Diabetes is a group of diferent diseases, and they share hyperglycemia (excess blood glucose) as a common denominator. Diabetes is one of civilization’s diseases. In diabetes, hyperglycemia occurs through various mechanisms. This happens on diferent levels: impaired receptor response to insulin (insulin resistance, which often arises from overnutrition and obesity), overproduction of hyperglycemic hormones, prolonged stimulation of the sympathetic nervous system, for example, during chronic stress. In type 1 diabetes, due to an autoimmune process (inflammatory state afecting beta cells of the pancreas), apoptosis of beta cells occurs, and the ability to produce and secrete insulin is irreversibly lost. The basic role in the regulation of glycemia is played by insulin, which is the only hormone that lowers blood glucose levels. The other hormone - glucagon plays an essential role in hepatic glucose output. In this way, it increases blood glucose levels. Together, insulin and glucagon work in tandem to maintain homeostasis in glucose metabolism, ensuring that the body has a stable energy supply while preventing the detrimental efects of excessive or insuficient blood sugar levels. Understanding the dynamics of insulin secretion and the role of -cells and -cells is essential for developing strategies to address conditions such as diabetes and metabolic syndrome.
The following work presents the mathematical model of the secretion of two opposite hormones responsible for keeping the glycemia level in the normal range: insulin and glucagon. This is the first attempt by the Petri Net model to describe the hormone secretion process at the cellular level, which is one of the links in the entire metabolic balance regulation process.
Our long-term goal is to create a simple and intuitive mathematical model representing all the processes taking place in the body of a healthy person. This model should be easily analysable and clear, but at the same time capable of representing complex activities consisting of interactions between many components. In our opinion, Petri nets (PNs) constitute an appropriate tool for this purpose. Due to PNs intuitive graphical representation and mathematical properties, the model could be easy utilized by people without mathematical background, for instance biologists, doctors, diabetes educators or patients. This allows for a better understanding of the processes occurring in a human body, and predicting new therapeutic targets and designing drug therapies by in-depth analysis and simulations. We are aware that our goal is ambitious and would not be reached at once.
Our initial eforts to achieve the desired result have been described in the following papers: [
The next part of our work consists of Petri net models of insulin secretion in -cell of the pancreas, and glucagon in -cells. Moreover, we combined both models and performed a detailed analysis of the resulting comprehensive model. Additionally, we show a Boolean network that models the same phenomena exactly. After the introduction, we recall the basic concepts of Petri nets. The following section contains the biological basis, while in the subsequent sections we introduce models of insulin secretion, glucagon secretion, and the combined model. In Section 5 we present a Boolean network obtained from the overall model with the use of logic formulas based on logical formulas corresponding to the semantics of Petri nets. The paper ends with a summary and future plans.
Let us begin by recalling basic mathematical concepts, which are important to understand the paper.
In this section we recall some concepts and definitions used throughout this paper, as well as the basic
notions concerning Petri nets and their properties [
The set of non-negative integers is denoted by IN. Given a set X, the cardinality (number of elements) of is denoted by ||. A function : → IN may also be considered as a vector in IN||. 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 → ⊆ ( × × ), • 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 1. 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, • 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 execution (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 ∃ ∈ : () < (, ).
Let us now recall some basic properties of Petri nets. A Petri net = (, , , 0) is called: • -bounded for some if ∀∈[0⟩∀∈ () ≤ , • bounded if ∃∈IN∀∈[0⟩∀∈ () ≤ (i.e., there exists a natural number such that, for all reachable markings, the number of tokens in each place does not exceed that number, which allows to say that [0⟩ is finite), • safe if it is 1-bounded, • weakly live if ∀∈ ∃∈[0⟩ [⟩ (every transition is reachable from the initial state), • live ∀∈ ∀∈[0⟩∃′∈[⟩ [⟩ (no transitions can be made unfireable), • reversible ∀∈[0⟩ 0 ∈ [ ⟩ (0 always remains reachable).
If ∈ ∪ , the pre-set ∙ and post-set ∙ of are defined as:
∙ = { ∈ ∪ | (, ) > 0}, ∙ = { ∈ ∪ | (, ) > 0}. 1Recall that a sequence (0, 1, . . . , − 1) of edges is called a (directed) path if there exist nodes 0, 1, . . . , ∈ such that ∀∈{0,1,...,− 1} we have (, , +1) ∈→. We extend the above notations to sets as follows: for ⊆ ∪ :
∙ = ⋃︀∈ ∙ and ∙ = ⋃︀∈ ∙ .
Having , ∈ ∪ , if (, ) > 0, we say that is an input place to if ∈ , and an input transition to if ∈ . In that case also, is an output transition from if ∈ , and an output place from if ∈ . A self-loop in a Petri net is when a place is both an input and output place of a transition. Let = (, , , 0) be a Petri net. Assume that = {1, . . . , } and = {1, . . . , }. Then: • input matrix for is a matrix − = (, )× , where , = (, ), • output matrix for is a matrix + = (, )× , where , = ( , ), • incidence matrix for is a matrix = + − − , A -invariant is a vector ∈ IN, such that · = 0, which indicates a possible loop in the net, i.e., a sequence of transitions whose net efect is null ( i.e., which leads back to the marking it starts in). The reachability graph ( ) of a bounded Petri net is the finite labelled transition system with: • set of nodes [0⟩, • label set , • set of edges {(, , ′) | , ′ ∈ [0⟩ ∧ [⟩ ′}, • initial state 0.
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 the given net. Figure 1 depicts a Petri net, together with its reachability graph. Reachability graphs of real biological systems are usually quite large and therefore dificult 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 it still permits the analysis 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 ifred. 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 they do not afect the merits of the system’s behaviour2.
The study of Boolean networks applied to biological systems was pioneered by Stuart Kaufman [
⎧⎪1 = (1 ∨ 2) = ⎨
2 = (¬3 ∧ 1) ⎪⎩3 = (2 ∧ 1) (1) A Boolean state is an interpretation of the variables of in Boolean i.e. : → B, B = {0, 1}, and = ( → B) is the set of all states.
The analysis of a Boolean network is primarily focused on the dynamics to investigate its behaviour. The Boolean dynamics provide the full description of all efective trajectories, thereby ensuring a comprehensive and thorough investigation of all possible dynamical scenarios.
Formally, a model of dynamics is defined by a labelled transition system where for each transition the states of agents are updated according to an updating policy defined by a mode. Two modes are frequently used in modelling: the asynchronous mode where one variable exactly is updated per transition and the synchronous mode where all the variables are updated per transition. As example, the asynchronous mode leads to the following labelled transition system (with no initial state specified) ( , →− , ) where the updated agent →−⊆ × × labels the transition relation, →− such that:
1 →− 2 =de=f 1 ̸= 2 ∧ 2() = (1) ∧ ∀ ∈ ∖ {} : 2( ) = 1( ).
A key objective of the analysis is to to assess the equilibria of the modelled network to gain insight into its long-term behaviour. Basically, a state is an equilibrium for →− , if it can be infinitely reached once met, i.e. ∀′ ∈ : →− * ′ =⇒ ′ →− * . The aim is to identify and characterize the attractors, which are defined as sets of mutually reachable equilibria.
The attractors corresponding to a single state are called stable states and can be eficiently and quickly computed by symbolic method while the computation of the other attractors (cyclic) remains exponential in general, limiting their investigation to small networks.
Finally, an interaction graph ⟨, ⟩ portrays the causal interactions between variables of a Boolean
network. An interaction exists if and only if occurs as a literal in a minimal Disjunctive
Normal Form (dnf) of , i.e. =de=f ∈ (dnf( )). The interactions are refined by a
sign stipulating the nature of the interaction: positive (+) or negative (− ). Figure 2 illustrates the
asynchronous dynamics of Boolean network (1) leading to a cyclic attractor (red) and a stable state
(yellow), and its signed interaction graph.
2We do not provide detailed definitions and properties here, interested readers are referred to the literature (a.o.: [
001 3 2 In this study, the Boolean network is systematically derived from the Petri net following standard transformation rules. This alternative formalism, which maintains semantic consistency with the original Petri net, facilitates the systematic characterization of stable states interpreted as steady molecular states, each potentially associated with distinct phenotypic outcomes.
In the following subsections the mechanisms leading to insulin secretion in -cells and glucagon
secretion in -cells of pancreas, schematically presented in Figure 3, are briefly discussed, in accordance
with the papers: [
The secretion of insulin and glucagon occurs in the endocrine cells of the islets of Langerhans. These islets are located in the pancreas and constitute a small percentage of its total mass. The pancreas mainly produces digestive enzymes secreted into the digestive tract, but it also has an endocrine function. The islets of Langerhans contain four principal cell types: beta-cells, which produce insulin and amylin, constitute about 90% of the islet, alfa-cells producing glucagon, gamma-cells producing pancreatic polypeptide, and delta-cells producing somatostatin. The islets are richly vascularized and hormones are directly secreted into bloodstream.
The insulin molecule consists of two polypeptide chains: the A chain (21 - amino-acid) and B chain (30 residues) linked by two disulphide bridges. Insulin exerts its main biological efects by binding to a cell-surface receptor. Insulin acts in peripheral tissues through receptors located on the surface of muscle cells and adipocytes (fat cells). After insulin binds to the receptor, glucose channels are activated, allowing glucose to enter the cells. This mechanism leads to a decrease in blood glucose concentration.
Glucagon is a 29-amino-acid peptide that is secreted by alfa-cells from proglucagon. Its receptors are mainly found in the liver. Once glucagon is secreted into the circulation, it elicits its function intracellularly by binding to its cell surface receptor G protein-coupled receptors (GPCRs). Glucagon evokes a signaling cascade that causes the expression of gluconeogenic and glycogenolytic process. Glucagon has the opposite efect to insulin. When blood sugar levels drop, glucagon is released into the bloodstream, signaling the liver to convert stored glycogen into glucose and stimulates the process of gluconeogenesis. This process helps raise blood glucose levels, providing energy to the body, especially during periods of fasting or low carbohydrate intake. Glucagon works in opposition to insulin, which lowers blood sugar levels. It is essential in regulating energy balance and supporting metabolic functions.
The primary stimulator for insulin secretion is the rising concentration of glucose in the blood. Therefore, its secretion is related to food intake. It also depends on changes the levels of amino acids and free fatty acids (FFA). Insulin secretion is modulated by the autonomic nervous system and influenced by incretins (GLP-1 glucagon-like peptide 1) which are enterohormones produced by intestinal cells. Insulin secretion is released in response to elevated blood glucose levels, such as after a meal. Insulin is primarily secreted in a biphasic manner: a rapid release of pre-formed insulin and, after a short lag, a sustained release of newly synthesized insulin. The process begins when glucose enters the beta cells through glucose transporters, particularly GLUT2. Once inside, glucose undergoes glycolysis and subsequently enters the metabolic pathway of oxidative phosphorylation, leading to the production of ATP. As the ATP levels rise, they cause the closure of ATP-sensitive potassium channels in the cell membrane. This closure leads to depolarization of the beta cell membrane, triggering the opening of voltage-gated calcium channels. The influx of calcium ions into the beta cells is a key step; it stimulates the fusion of insulin-containing secretory granules with the plasma membrane. This fusion results in the exocytosis of insulin into the bloodstream. The secretion of insulin is also influenced by other factors, including hormones and nutrients, such as amino acids and fatty acids, which can further enhance or modulate the secretion response.
The primary stimulus for glucagon release is a decrease in blood glucose levels. When blood glucose levels drop such as during fasting or prolonged periods without food intake or during intense physical activity. Pancreatic -cells are equipped with a specific set of channels of Na+ and Ca2+, which, at low levels of glucose, triggers Ca2+ signals and finally glucagon secretion. ATP-dependent K (K-ATP) channels plays a fundamental role in -cells, such as they do in -cells, since they couple variations in extracellular glucose concentrations to changes in membrane potential and electrical activity. Also, paracrine factors afect glucagon secretion. Insulin receptors are present on -cells. Additionally, insulin may indirectly suppress glucagon secretion through increasing translocation of -cell GABA-A receptors (420). Inhibition of GABA receptors increases glucagon secretion and GABA released from -cells is postulated to mediate glucose-facilitated inhibition of glucagon secretion. The pancreas is highly innervated by both the sympathetic (splanchnic) and parasympathetic (vagus) nervous system. Centrally regulated glucagon secretion could be mediated via direct sympathetic innervation on the -cell, indirectly via the sympathetic tone and signaling through the hypothalamic-adrenalpancreas signaling axis, and/or potential indirect parasympathetic signaling. Altogether, glucagon secretion is a complex process regulated by multiple interactions between glycemic, paracrine, endocrine, and neural factors.
In our current work, we focus on the primary stimulus of glucagon secretion – changes in blood glucose levels. However, mentioned above, the more complex regulation mechanisms of glucagon secretion would be included in the next, future parts of the PN model.
In this section, we present and discuss Petri net models of insulin secretion in pancreatic -cells and glucagon secretion in pancreatic -cells. We also introduce a general model showing a joint operation of both individual models.
Let us first discuss the model of insulin production, depicted on the left side of Figure 4, while its reachability graph is shown on the right hand side.
High glucose level is represented by the token located in H_glucose place. Glucose is taken up by the -cell of the pancreas, which is represented by the absorb-B transition. When present in the cell, which is modelled by the token in place glucose-in-B, it is used in ATP production - represented by the prod-ATP-B transition. The execution of this transition results in a token being placed in place ATP>ADP-B, which means that ATP/ADP ratio is in favour of ATP. In this situation, more-ATP-B transition becomes enabled. During execution, this transition transfers a token from place K-ch-open-B to place K-ch-close-B and it corresponds to the situation when potassium channels become closed. When the channels are closed, transition abs-K-B becomes enable – it represents the increment of potassium in the cell by moving a token from place K-out-B (representing potassium outside of the cell) to place K-in-B (representing potassium inside the cell). A token in place K-in-B (corresponding to the higher amount of potassium in the cell) enables transition open-Ca-B. This transition represents opening of the calcium channels by moving the token from Ca-ch-close-B, which represents closed channels, to place Ca-Ch-open-B, which represents open channels. Then the transition abs-Ca-B is enabled, which models the process of increasing a level of calcium in the cell. This is done by moving a token from place Ca-out-B (calcium outside of the cell) to place Ca-in-B (calcium inside the cell) and place ready-B (conditions are suitable to release insulin). A token in place ready-B, representing the suitable conditions to secrete insulin, makes the transition produce-insulin enabled. This transition corresponds to insulin secretion and produces a token to the place insuline. Then transition reduce-glucose can be executed. It represents a decrease in glucose levels and moves tokens to places low-inside-B and N_glucose (symbolizes a normal level of glucose).
When glucose levels return to a normal (appropriate) value, a token appears in place low-inside-B. Then transition ATP-use-B is enabled, which represents the decrease in ATP level and the increase in ADP level. This is modelled by relocating a token from place ATP>ADP-B to ADP>ATP-B. The token in place ADP>ATP-B enables transition more-ADP-B, which moves the token from K-ch-close-B to place K-ch-open-B, which represents the opening of the potassium channels. When these channels are open, transition rem-K-B can be executed (it represents the process of potassium leaving from the cell) and it moves a token from place K-in-B to place the K-out-B. When the potassium level in the cell decreases, which in the model is represented by a token in place K-out-B (i.e. “potassium out”), transition close-Ca-B becomes enabled. It represents closing of calcium channels and transfers a token from place Ca-open-B to place Ca-close-B. This allows to execute transition rem-Ca-B – corresponding to the process of decreasing of calcium level in the cell. The transition transfers tokens from place Ca-in-B to place Ca-out-B. The token in place Ca-in-B means that the -cell returns completely to the state when the secretion of insulin is not possible.
After execution of transition EATING (representing “eating”) the entire process starts all over again. It is easy to observe that the net is bounded (as the reachability graph is finite). It is also reversible. Indeed, the parts of the model responsible for insulin production induced by high glucose levels, i.e.: and for the return of the -cell to the initial situation, i.e. execute alternately, which is observable in the reachability graph (Figure 4).
Moreover, switching from the second path (returning to the initial state) to the first one (production of insulin) is possible only after execution of transition EATING. It corresponds to the real, biological behavior, that after insulin is released (and the level of glucose decreases), secretion of insulin stops and the cell returns to its initial, nonactive state. And after eating, the increasment in glucose level initializes processes resulting in insulin secretion.
Let us now focus on the model of glucose-dependent glucagon secretion, depicted on the left side of Figure 5, while its reachability graph is shown on the right hand side.
In the case of the glucagon production, most of the model resembles the insulin production one, except that the names of the elements end with “A”. The main diference is, however, that in this case the potassium channels close when the token is located in place ADP>ATP-A, and the channels open when the token is located in place ATP>ADP-A. Transition more-ATP-A is responsible for opening the channels, and transition more-ADP-A for closing. Furthermore, since in -cells not only calcium channels must be open, but also sodium ones, the model includes places CaNa-ch-open-A and CaNach-close-A, analogous to places Ca-open-B and Ca-close-B from the insulin production model. The reachability graph presents the dynamic of the PN model. Same as in the case of insulin production by -cells, the model of -cells production of glucagon is also bounded and reversible. The two processes are performed alternately. First one represents the secretion of glucagon and consists of: (III) use-ATP-A⇒ ADP>ATP-A ⇒ more-ADP-A⇒ K-ch-close-A⇒ abs-K-A⇒
The second corresponds to the process of returning of the -cell to its initial state and consists of: (IV) prod-ATP-A⇒ ATP>ADP-A ⇒ more-ATP-A⇒ K-ch-open-A⇒ rem-K-A⇒
It is easy to observe in the graph, that the secretion process is initiated by the LIVING transition. This transition represents the normal, biological consumption of glucose by cells to perform their living functions.
In this section, we analyse the combined model, depicted in Figure 6, in which both insulin and glucagon can be secreted, depending on the current blood glucose level.
As before, places H_glucose, N_glucose, L_glucose represent high, normal, and low blood glucose levels, respectively. Let us note that if in the initial state, i.e. at a normal blood glucose level, transition EATING executes, then the token moves from place N_glucose to the place H_glucose, makes the transition absorb-B fireable and enables execution of transition in the left part of the net, responsible for insulin secretion. On the other hand, when transition LEAVING is executed, then the token goes to place L_glucose, and the right side of the net, modelling the secretion of glucagon, becomes active (transition low-efect-A becomes enabled). As one might notice, the left and right parts of the net are constructed from the previously introduced individual models for insulin and glucagon secretion, respectively.
As known, the best way to analyse the behaviour of a Petri net, is by examining its reachability graph. In this case however, even though the net is bounded, we do not show its reachability graph here, because it contains 192 states with 418 arcs, and is too large to be displayed in a transparent way. Instead, we will settle for analysis of stubborn reduced reachability graph presented in Figure 7.
In the graph four states have been distinguished: S0 which corresponds to the initial marking, S1, S2 and S3. In each of these states transitions EATING and LIVING are enabled. These states are the vertices in which the paths in the graph intersect, and the execution of one of the two mentioned transitions determines the behaviour of the model. The paths between the highlighted states correspond to the main processes described in previous sections for the separate models: secretion of glucagon by -cells, returning to the inactive state of -cells, the secretion of insulin by -cells and returning to the inactive state of -cells. The path from S0 (the initial marking) to S1, which starts with transition LIVING, contains transitions related to the secretion of glucagon (states marked in green). On the other hand, when at S0 transition EATING is executed, the state S2 is reachable and the path between S0 and S2 contains transitions representing the secretion of insulin (marked in yellow). Then, when at state S1 transition LIVING fires, the path leads back to state S1 and contains transitions related to returning to the inactive state by -cells (marked in blue) and the secretion of glucagon. Notice that, starting for the initial marking it would be the second execution of transition LIVING. Similarly, if at state S2 transition EATING is executed (starting for the initial marking it is the second execution of that transition), then the path in the graph leads back to state S1 and contains transitions representing the process of returning to the inactive state by -cells (marked in red) and the secretion of insulin. If in S1 transition EATING fires, state S3 is reached and the path corresponding to the secretion of insulin. From state S2 state S1 can be reached by firing of transition LIVING and the path containing elements related to the process of returning to the inactive state by -cells and the secretion of glucagon. Note that, starting from the initial marking, the path from S0, then S2 to S1 includes transitions EATING and living, each executed once. State S1 can be reached from state S3 by firing of transition LIVING and the path corresponds to the process of returning to the inactive state by -cells and -cells, and the secretion of glucagon. To reach S1 through S3 from S0 the transition EATING has to be executed once and transition LIVING twice. When at S3 transition EATING fires, the path leads back to S3 and it is related to the process of returning to the inactive state by -cells and the secretion of insulin. To conclude this part of the analysis, one can notice that every time transition EATING fires, the part of the model corresponding to the secretion of insulin is active. Eventually, before the next secretion, -cells have to return to their initial state. It happens when transition EATING has been previously executed. Similarly, after execution of transition LIVING, the secretion of glucagon takes place. If that transition has been executed previously, -cells have to go back to their inactive state before the next secretion. This behaviour is desirable and consistent with biological processes, which is our most important goal.
One might notice, that in the reachability graph presented in Figure 7 the model does not go back to
the initial state. This is efect of the stubborn reduction. The model is live, reversible and it is covered
by -invariants. All those properties are important and desirable in biological models.
In Figure 8 we present all the semipositive -invariants of the Petri net depicted in Figure 6. Every
transition is included in a -invariant. Moreover, -invariants 1, 2, 3 and 4 contain every transition
from the insulin part of the model, -invariants 5, 6, 7 and 8 – every transition from the glucagon
part of the model. Like mentioned in Section 2.1, the execution of transitions from -invariant does
not result in the change of the marking. Hence, by starting from the initial marking and executing
transitions from -invariants: 1, 2, 3 and 4 the initial marking would be reached. The same from
transitions for -invariants: 5, 6, 7 and 8. It shows that the model presents a cyclic behaviour.
To summarize, the models precisely reflects the biological processes of the secretion of insulin, glucagon,
their relations and cyclicality. It is important to notice, that when the most of transitions precisely
model the exact biological process, some transitions symbolize more complex efects. This applies to
transitions: EATING, LIVING, reduce-glucose and increase-glucose. The first one represents all
processes, which can elevate the glucose level. The most common one is, indeed, eating, which provides
carbohydrates. The second one corresponds to processes of reducing glucose level. The most important
one is usage of glucose by cells to perform their living functions. In both cases other phenomena may
afect the level of glucose. The process of increasing the glucose level, modelled by transition
reduceglucose, has the same efect like in the model, but in organisms it consists of many other processes, like
absorption of glucose by cells or storing of glucose in the liver or the fat tissue. All those complex efects
are represented by only one transition in the model. The same occurs for transition increase-glucose.
This process is complex, and involves releasing of glucose stored in diferent parts of the body. It the
model it is represented by a single transition. A part of this complex process is modelled in our previous
paper ([
As could be seen in the previous sections, describing biological foundations and models, glucosestimulated insulin secretion by -cells as well as glucose-stimulated glucagon secretion by -cells on the pancreas take the form of pathways, i.e. sequences of processes undergone by a specific compounds. Note that the presented Petri net models operate largely on the binary principles, where a token in a given place symbolizes the occurrence of a certain phenomenon, while the absence of a token means that the phenomenon does not occur. In fact, all presented PN models are safe (or 1-safe), which means that the number of tokens in any place at any reachable marking does not exceed 1. We decided to use this approach rather than a quantitative one in order to obtain a model that is clear, transparent, and easy to analyse, as well as easily convertible into Boolean networks.
On the other hand, one of the commonly used models to study complex dynamic behaviour of a biological
systems, which perfectly model biological pathways, are Boolean networks. In many scientific papers
(among others [
In this paper we decided to transform the combined Petri net model presented in Section 4.2 into a Boolean network. The transformation rules are rather intuitive and are based on the possibility of a token moving (by execution of a single transition) from one place to another. Describing pre-sets and post-sets of every transition, we obtain the net interaction characteristics. Due to the fact that self-loops from the original Petri net have no impact on the flow, we decided not to include them in the model, therefore the model table (Figure 9) the interaction graph (Figure 10) do not include them.
Let = (, , , 0) be a Petri net depicted in Figure 6. In order to transform into a Boolean net, we use the rules described below.
Let ∈ be a place, and let {1, 2, . . . , } = ∙ be a pre-set of , i.e. the set of transitions for which is an output place. For ∈ ∙ let {1 , 2 , . . . } be a set of all places being an entry to . Then in the Boolean network we need to introduce the following formula:
= (11 ∧ 12 ∧ . . . ∧ 11 ) ∨ (21 ∧ 22 ∧ . . . ∧ 22 ) ∨ . . . ∨ (1 ∧ 2 ∧ . . . ∧ 1 ). By performing the transformation based on the above rule for all locations in the model, we obtain the Boolean network presented in Figure 11.
As described, the Petri Net model of insulin secretion and glucagon secretion in the pancreas can be easily transformed into a Boolean network and any tools that allow analysis of Boolean networks can be used for its further analysis. This approach provides the future opportunity to analyse both models simultaneously or use them alternately depending on current needs. We can, for instance, compute all stable states for our Boolean network (depicted in Figure 12). In calculated stable states of the model, either all variables are assigned 0s, or all of them are assigned 1s. Another possibilities are (1) all variables associated with the left part of the original net (corresponding to the insulin secretion), together with those connected to glucose levels, are assigned 1s, and the remaining ones (corresponding to the glucagon secretion) are assigned 0s or vice versa, (2) variables associated with glucagon secretion (with those connected to glucose levels) are assigned 1s, and those connected to the insulin secretion are assigned 0s. This reflects well the dynamic aspects of the model.
In this paper, we took another step towards modelling all processes responsible for the regulation of glycaemia in humans. We presented Petri net models of insulin secretion in -cells of the pancreas and glucagon secretion in -cells of the pancreas, as well as a comprehensive model taking into account both processes. We also analysed the dynamics and properties of the three models. Additionally, we presented a transformation of our comprehensive model to Boolean networks.
Our analysis demonstrates that the PN model is capable of reproducing the biological processes it represents: as in the real body, high glucose levels trigger insulin secretion, while low levels stimulate glucagon release. This accurate reflection of physiological behaviour serves as a foundation for a deeper analytical framework. One might notice the one-dimensionality of the presented model in relation to the “signalling pathway” of - and -cells. Indeed, since this is our first approach, it does not take into account, among other things, the interaction between insulin secretion and glucagon secretion and vice versa: increased glucagon secretion under the influence of increased insulin concentration (postprandial). Other factors modelling the secretion of both hormones, such as incretins (endocrine hormones), were also not taken into consideration. Our future plans include modelling these interactions as well.
We also acknowledge that the reachability graph, while central to our analysis, is not the only viable method for examining Petri net dynamics. In this work, we employed stubborn set reductions to mitigate state space explosion. Looking ahead, we plan to explore alternative analysis techniques such as unfoldings and the use of advanced verification tools like TINA and GreatSPN, which ofer broader analytical capabilities and may yield deeper insights into the model’s behaviour. As a result of our work, we hope to obtain a comprehensive model of glycaemia regulation in humans. It is worth emphasising that formalising a well-understood biological process is not merely an academic exercise. Rather, it represents a foundational step towards automatic verification of biological mechanisms, with direct applications in drug development and evaluation of the consequences of genetic modifications in pancreatic - and -cells.
Building on this foundation, the purpose of our work extends beyond replication of established biological mechanisms. We aim to construct a formal and analysable model that facilitates in silico experimentation and hypothesis generation. The Petri net framework allows the simulation of both physiological and pathological conditions – such as impaired ion channel function, abnormal ATP/ADP ratios, or hormonal dysregulation – in a controlled, formalised manner. These simulations may support the identification of regulatory bottlenecks, potential therapeutic targets, or emergent behaviours that are not easily accessible through experimental observation alone. Beyond its analytical power, the model is designed to be accessible and interpretable for researchers outside computer science, including biologists, clinicians, and medical educators. Thanks to the visual and modular structure of Petri nets, the model provides an intuitive yet rigorous means of representing complex biological processes. This makes it a valuable educational tool and a potential foundation for broader system-level models, such as those involving incretins, stress hormones, or long-term glycaemic adaptation.
Importantly, the model captures not only the static states of the system – such as hormone readiness or channel open/closed status – but also the full spectrum of transitions between these states, reflecting the inherently dynamic and cyclical nature of endocrine regulation. This includes reversible mechanisms by which pancreatic cells return to their baseline after hormonal secretion. Such capability is critical for studying how the system adapts to physiological changes, how it responds to perturbations (e.g., ion imbalance, energy deficits), and what thresholds separate healthy behaviour from pathological scenarios like persistent hyperglycaemia or hormonal insuficiency. By simulating these transitions, the model enables a deeper understanding of how regulatory feedback fails in diabetes and may inform interventions aimed at restoring balance. In future research, we aim to incorporate empirical data to tailor the model to specific clinical contexts, enhancing its potential use in personalised medicine or treatment planning – particularly in the context of diabetes prevention, diagnosis, and therapy. One of the key contributions of this study is the integration of two formal modelling paradigms: Petri nets and Boolean networks. Although typically considered independently, we emphasise their complementary strengths in modelling the dynamics of biological systems. Petri nets are particularly well suited to representing asynchronous, concurrent, and potentially stochastic processes. They are especially valuable for modelling resource flows – such as biological molecules – and for visualising causal dependencies between events. Their capacity to depict mechanistic detail makes them a powerful tool for simulating cellular-level pathways.
Conversely, Boolean networks abstract the system to a logical level in which each component is either active or inactive. This simplification facilitates the analysis of global system properties, such as the identification of attractors and stable states, which often correspond to biological equilibria or phenotypic outcomes.
In our work, we adopted a two-step approach. First, we developed a detailed Petri net model that captures the causal-regulatory mechanisms underlying insulin and glucagon secretion. Subsequently, using a systematic transformation procedure, we converted this model into a Boolean network, enabling further dynamic analysis using logical tools.
This conversion preserves the logical structure and temporal constraints of the biological processes while providing access to advanced analytical techniques typical of Boolean modelling – such as symbolic analysis, graph traversal, and attractor detection via SAT-based methods. In doing so, we harness both the expressiveness of Petri nets and the analytical clarity of Boolean models.
By integrating these perspectives into a unified modelling framework, we enable a more comprehensive, multi-level understanding of biological regulation. The hybrid approach we propose holds promise for the development of more accurate and insightful models of glycaemic control and ofers valuable system-level insights into the mechanisms underlying diabetes onset and management.
The author(s) have not employed any Generative AI tools. 40–59
– [26] Charlie, https://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Charlie [27] Pipe2, https://pipe2.sourceforge.net/ [28] Snoopy, https://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Snoopy [29] https://www-users.mat.umk.pl/∼ leii/pnse25/