Model checking has been attracting attention to analyze signaling pathways. There are two or more, i.e. multiple, signals flowing in a signaling pathway. Most of previous work, however, have treated only one, i.e. single, signal. To analyze a signaling pathway more precisely, it is necessary to treat multiple signals. There is few previous work treating multiple signals. It is known that a primary issue in model checking is the state-space explosion. Multiple signals make it difficult to analyze by model checking. In this paper, we propose two modeling methods for signaling pathways with multiple signals. These methods transform a Petri net model of a signaling pathway to an automaton model of UPPAAL. The first method uses multiple automata as a model of UPPAAL. The second method uses a single automaton as a model of UPPAAL. We apply these methods to an example. And we find that the single automaton modeling method is more effective than the multiple automata modeling method from the viewpoint of the number of signals, the number of states explored, and checking time. These results show that the model size to be analyzed is improved by devising of modeling method.
Signaling pathway is a signaling mechanism to unify the behavior of cells. Since a
pathway is large and complex, there are unknown mechanisms and components.
Some researchers have applied model checking to analysis of signaling pathways.
Model checking is an automatic and usually quite fast verification technique
for finite state concurrent systems. In 2003, Chabrier et al.[
There are two or more, i.e. multiple, signals in a signaling pathway because
a ligand joins a receptor repeatedly. To analyze the signaling pathway more
precisely, it is necessary to treat multiple signals. There is few previous work
treating multiple signals. Kwiatkowska et al.[
In this paper, we propose two modeling methods for signaling pathways with
multiple signals. These methods transform a Petri net model of a signaling
pathway to an automaton model of UPPAAL. Cassez et al.[
In Sect.2, we present a Petri net model of signaling pathways and an automaton model of UPPAAL. In Sect.3, we propose two modeling method for a signaling pathway with multiple signals. In Sect.4, we apply the two proposed methods to an example and evaluate the two methods. Finally, Sect.5 gives a conclusion and some future work. 2 2.1
Matsuno et al.[
The formal definition of a Petri net model of a signaling pathway is as follows. De nition 1. A Petri net model of a signaling pathway is a 5-tuple T P N R = (T, P, E , D, R).
T : A set of transitions {t1, t2, · · · , tjT j}
P : A set of places {p1, p2, · · · , pjP j}
E : A set of directed arcs between the places and the transitions
D : T → N : A function to assign a ring delay time to a transition
R : T → [
Note that ∑t2p• R(t) = 1. □ There are one or more source transitions and one or more sink transitions. Every node is on a path from a source transition to a sink transition. If a firing of a transition ti is decided, tokens required for the firing are reserved. We call these tokens as reserved tokens. When D(ti) passes, ti fires to remove the reserved tokens from each input place of ti and put non-reserved tokens into each output place of ti. If a place pi has two or more output transitions, each output transition can’t fire over R(ti). Let X (t) be the firing count of t. Then, ∀t ∈ p
X(t)
: ∑t′∈p• X(t′) ≤ R(t). Figure 1 is a Petri net model of a part of IL-1 signaling
pathway[
UPPAAL[
De nition 2. A timed automaton is a 6-tuple (L, l0, C, Act, E, I ).
L : A set of locations l0 ∈ L : The initial location C : A set of clocks Act : A set of actions E ⊆ L × Act × B(C) × 2C × L : A set of edges between locations with an action, a guard and a set of clocks to be reset
I : L → B(C) : A function to assign to an invariant to a location □
Timed automata often form a network over a common set of clocks and actions,
consisting of n timed automata Ai = (Li, li0, C, Act, Ei, Ii), 1 ≤ i ≤ n. For the
semantics of the automaton model, refer to [
t64 D(t64)=12
t69
D(t69)=15 t65 D(t64)=30 R(t64)=0.4 t66 D(t66)=20 R(t66)=0.6
t70 D(t70)=30 R(t70)=0.5 t71 D(t71)=30 R(t71)=0.5
In model checking in UPPAAL, we describe a property to be analyzed in Timed Computation Tree Logic (TCTL) and we can verify whether the model with clock variables satisfies the property by running model checking. TCTL on UPPAAL includes E<> p (There exists a path where p eventually holds) and A[] p (For all paths p always holds).
A Petri net model representing a signaling pathway must be correct. We use UPPAAL to verify whether a Petri net model is correct, because the Petri net model includes time concept. The model used in this paper is timed Petri net, but it is easy to extend our method to time Petri nets.
It is known that model checking is powerful but may cause the state-space
explosion. The more signals are, the more the problem becomes severe. Kwiatkowska
et al.[
We give the representation model used in each modeling method. Both models have the same expressive power as a Petri net model; provided that the Petri net model has no transition branches. Note that those models can treat transition joins. We give a simple example to show the difference between the multiple automata model and the single automaton model.
t1 D(t1)=12 p1
t2 D(t2)=9 p2
t3
D(t3)=12 (a) A Petri net model time:0 0 0 t1
t2 time:12 1 0 time:21 0 1
t1 t3 time:24 1 1 (1) Multiple automata model
The multiple automata model preserves the structure of a given Petri net model as much as possible. A Petri net model with n signals is represented as the following: • The multiple automata model of the Petri net model consists of n automata. • Each automaton represents the state transition of a single signal. • A place or a transition is represented as a location. • An arc is represented as an edge. • Firing delay time is implemented by using a location invariant and a guard.
In this example, we use a Petri net model, T P N R1, which is shown in Fig.2. Figure 2(a) is a Petri net model and Fig.2(b) is a state transition of the case t1 fires twice. Since T P N R1 is state machine, the reachability graph has a similar structure as the net. Figure 3 shows the multiple automata model of T P N R1. In this example, we assume that source transition t1 fires twice. There are two signals in this model. The two signals are represented as two automata. Two places and three transitions are represented as five locations. Four arcs are represented as four edges. Firing delay time D(t1) = 12 is implemented by using location invariant (gc1<=12) of t1 and guard (gc1>=12) of edge (t1,p1), where gc1 denotes a global clock. Similarly, firing delay time D(t2) = 9 is implemented by using location invariant (c<=9) of p1 and t2 and guard (c>=9) of edge (p1,t2), where c denotes a local clock. D(t3) is implemented by a similar way. A current state of the automata represents where the signals are now. (2) Single automaton model
The single automaton model represents a given Petri net model as a single automaton with only one location even if there are two or more signals. A Petri net model with n signals is represented as the following: • The single automaton model consists of a single automaton with only one location. • The automaton represents multiple signals by using clocks c[] and variables xf[]. • The markings of the places are represented as variables mp1, mp2, · · ·, mp|P |. • A firing of each transition is represented as a self loop of the location. • Firing delay time is implemented by using a location invariant and a guard.
Figure 4 shows the single automaton model of T P N R1. Figure 5 is the state
transition of the single automaton model. Places p1, p2 are represented as
a single location with variables mp1, mp2, where mpi denotes the marking
of pi. The state transition of marking is same as Fig.2(b). Table 1 is the
variables used in single automaton model. A firing of t1, t2, t3 is
represented as edge (A), (B), (C). A global clock gc1 is assigned for the source
transition t1. Clocks c[] and variables xf[] are assigned for signals. k is
the maximum number of signals in the pathway. xf[i] denotes the firing
delay time of the i -th signal. Multiple signals are represented as a single
location with c[] and xf[]. Firing delay time of the i -th signal is
implemented by using location invariant (c[i]<=xf[i]) and guard (c[i]>=xf[i]).
In a firing of transition t1 (Edge (A)), action (xf[tf1]:=9) means setting
the firing delay time of next transition t2. tfi denotes the signal ID of the
first reserved signal in transition ti. Action (tx2[i2]:=tf1) means
reserving the signal that fires on t1 to next transition t2. txi[k] stores signal
IDs reserved in transition ti. (tf2:=tx2[0]) removes the first reserved
signal ID of transition t2. In a firing of the transition t2 (Edge (B)), action
(mp1--, mp2++, c[tf2]:=0, xf[tf2]:=0, tx3[i3]:=tf2, tf3:=tx3[0])
time:0
mp1=0
mp2=0
gc1=0
c[
In this subsection, we give, for each modeling method, an algorithm for
transforming a Petri net to an automaton model. Due to limitations of space, we
restrict the algorithm to the modeling of a single path Petri net model.
(1) Multiple automata modeling method
<<Transformation to Multiple Automata Model>>
Input: Petri net model T P N R = (P, T, E, D, R), number n of signals
Output: Multiple automata model A1, A2, · · ·, An
Foreach i = 1 to n, make Ai according to the following:
1. L ← P ∪ T
2. C ← {gc1, ci}
3. E ← {(p, ∅,(ci>= D(t)), ∅, t)| (p, t) ∈ A}
∪ {(t, (gc1:=0, ci:=0), (gc1>=D(t)), {gc1, ci}, p)| | t| = 0, (t, p) ∈ A}
∪ {(t, (ci := 0), ∅, {ci}, p)| |t | > 0, (t, p) ∈ A}
4. I ← {(t, (gc1<=D(t1)))| t ∈ T, | t| = 0}
∪ {(t, (ci<=D(t)))| t ∈ T, |t | > 0}
∪ {(p, (ci<=D(t)))| p ∈ P, t is the output transition of p}
(2) Single automaton modeling method
<<Transformation to Single Automaton Model>>
Input: Petri net model T P N R = (P, T, E, D, R), number n of signals
Output: Single automaton model A, variables mp1, mp2, · · ·, mp|P |, tf1, tf2,
· · ·, tf|T|, xf[], tx1[], tx2[], · · ·, tx|T |[].
1. L ← {l0}
2. C ← {gc1, c[
∪ ∪ i=2tojT j 1{(l0, (mp(i−1)--, mpi++, c[tfi]:=0, xf[tfi]:=D(t(i+1)),tx (i + 1)[i(i + 1)]:=tfi,i(i + 1)++, tf(i + 1):=tx(i + 1)[0], freetxi(), tfi:=txi[0]), (c[tfi]>=xf[tfi]&&xf[tfi]==D(ti)), {c[tfi]}, l0)} t1res() resets c[] and xf[].
freetxi() organizes reserved signal IDs of transition ti.
4. I ← {(l0, (c[0]<=xf[0]&&c[
We give the pattern lists of transforming TPNR to multiple automata model and single automaton model to ease the transformation. Multiple automata model multiple automata model and single automaton model can be created by combination of these patterns. Table 2 is the pattern list of transforming TPNR to multiple automata model. c is a local clock and gc is a global clock. { The first column is for multiple source transitions. Location source is a global source. This location implements all of the firing delay times of source transition with global clocks, gc1, gc2. { The second column is for a place branch. A place branch is implemented by using l and r. l denotes the firing count of t2, and r denotes the firing count of t3. And guard ((l+r)*40>=l*100) limits that firing count of t2. t3 is implemented by a similar way of t2 but firing delay time of t3 is longer than that of t2. So, the blacken location is added to implement the firing delay time. { The third column is for a transition join. A transition join is implemented by channels t1fire! and t1fire?. A signal on p1 and a signal on p2 are synchronized, then two signals fires on t1. The blacken location is added to abandon the signal on p2. { The fourth column is for a place join. A place join is implemented by a similar way of <<Transformation to Multiple Automata Model>>.
{ The first column is for multiple source transitions. Edge (A) implements a firing of t1 and edge (B) implements a firing of t2. Firing delay times of t1 and t2 are implemented by global clocks gc1 and gc2. { The second column is for a place branch. Edge (A) implements the firing of transition t1 with substituting 0 in xf[] and tf2bra3 stores the signal ID that isn’t reserved. Edges (B) and (D) are limiting the firing count by similar way of multiple automata model and reserve a signal to transition t2 or t3. Edges (C) and (E) implement the firing of transitions t2 and t3. { The third column is for a transition join. A transition join is implemented by only updating variables mp1 and mp2. { The fourth column is for a place join. A place join is implemented by a similar way of <<Transformation to Single Automaton Model>>. Edge (A) implements the firing of transition t1 and edge (B) implements the firing of transition t2. 4
In this section, we apply the proposed modeling methods to IL-1 signaling pathway. And we compare the obtained models and discuss the merits and demerits of the modeling methods.
IL-1 is a proinflammatory cytokine, and plays an important role in regulating
the mechanism of proinflammatory. There cause multiple signals flowing in the
signaling pathway because a ligand joins a receptor repeatedly. The whole Petri
net model of IL-1 signaling pathway is shown in Fig.3 of [
The correctness of the model must be examined. We can check the correctness of the model by model checking. For example, { We can check the reachability with time concept. Checking the reachability helps us to understand signaling pathways. Let c be a clock, we write a TCTL expression of this property as E<> M (p1)>0 && c==30. This expression means there exists a path where a signal is on p1 when c is 30. { We can also check that there is no retention in the model. Retention means that signals are accumulated at any place. We write a TCTL expression of this property as A[] M (p1)<=5. This expression means that the number M (p1) of signals for place p1 is always 5 or less.
In this paper, we focus on checking the retention. If there is retention in the Petri net model, we consider the error in the Petri net model or the possible of unknown paths in the signaling pathway.
We apply two modeling methods to a part of IL-1, which is shown in Fig.1. The size of the Petri net model is |P | = 7, |T | = 12. Figure 6 shows the multiple automata model of Fig.1. Figure 7 shows the single automaton model of Fig.1.
This Petri net model includes three source transitions, therefore we applied the first column of each pattern list at the case of three source transitions. Places e1, e2, and e3 have two output transitions, therefore we applied the second column of each pattern list. We applied the third column of each pattern list for transition t72 because t72 has two input places. And we applied the fourth column of each pattern list for place e7 because e7 has two input places.
Table 4 shows the size and the number of clocks and variables of the obtained models. The size of each automaton of the multiple automata model is |L| = 23, and |E| = 26. In comparison, the size of the single automaton model is |L| = 1, and |E| = 19. The number of clocks of the multiple automata model is 3+n, and the number of variables is 6, where n is the number of signals. The number of clocks of the single automaton model is 48, and the number of variables is 40. In addition, the number of arrays is 13. The number of clocks continue to increase according to the number of signals n in the multi automata model, but the number of clocks is constant in the single automaton model. The size of the single automaton model is smaller than the size of the multiple automata model, but the number of variables of single automaton model is larger than that of the multiple automata model under the same expressive power.
We can analyze the retention property by using those automaton models. Table 4 shows the number of signals, the number of states explored, checking time. Model checking is performed on the PC with CPU Xeon 2.13GHz and memory 3.2Gbyte. We could check the retention property of the multiple automata model until the number of signals is 128. Meanwhile we could check that of the single automaton model until the number of signals is 702. The single automaton model enables us to analyze more signals than the multiple automata model. The number of states explored of the single automaton model is smaller than the multiple automata model, and checking time is also shorter. 5
In this paper, we proposed two modeling methods for signaling pathways with multiple signals. Those modeling methods use different representation model. Next we gave for each representation model, a transformation algorithm, and a pattern list. Then we applied these proposed methods to the IL-1 signaling pathway. The results show that signaling pathway with multiple signals should be represented as not automata but variables, and the model size to be analyzed can be increased by devising of modeling method. We have also applied these method to endocytosis signaling pathway, and a similar trend have been obtained.
As future work, we plan to develop a method treating transition branches. An approach is to prepare child process for implementing parallel part and devising the clock handling. And we think that it is easy to extend our method to time Petri net model. We will verify that our method can be applied to time Petri net model.
The authors would like to thank Prof. Hiroshi Matsuno, Prof. Qi-Wei Ge, and Mr. Yuki Murakami for their valuable advices.