Biology Reference
In-Depth Information
introduced variables determines a subset of
T
, which includes the subset determined by the valuation of
t
1
,
...
,
t
n
. The formula for case(
s
1
,
...
,
s
m
,
t
1
,
...
,
t
n
)
is given by:
non conflicting
(
s
1
,...,s
m
,t
1
,...,t
n
)
∧
∀
t
1
,...,t
n
1
j
n
t
j
t
j
1
j
n
t
j
<t
j
1
j
n
t
j
1
∧
∧
∧
∧
∨
⇒
(5)
.
¬
non conflicting
(
s
1
,...,s
m
,t
1
,...,t
n
)
To present the formula non conflicting (
s
1
,
...
,
s
m
,
t
1
,
...
,
t
n
) we need a special ordering over the
variables corresponding to transitions. For every place
s
∈
S
we assume the permutation
σ
s
of
{
1,
...
,
n
}
such that in the induced ordering of transitions
t
σ
s
(1)
,...,t
σ
s
(
n
)
,
transitions with a negative balance with respect to
s
, precede the remaining transitions. Formally, this
condition can be expressed by:
s
−
.
t
σ
s
(1)
,...,t
σ
s
(
|s
−
|
)
∈
(6)
The formula for non conflicting (
s
1
,
...
,
s
m
,
t
1
,
...
,
t
n
) is based on Lemma 1, as follows:
∧
1
i
m
∧
1
j
n
(7)
⎛
⎝
⎞
⎠
s
i
+
t
σ
s
i
(1)
(
s
i
)
∗
t
σ
s
i
(1)
+
...
+
t
σ
s
i
(
|
s
i
)
(
s
i
)
∗
t
σ
s
i
(
|s
i
−
t
j
(
s
i
)
∗
t
j
W
(
s
i
,t
j
)
∗
t
j
.
|
|
)
s
i
if
t
j
∈
2
It is easy to see that the length of the Eq. (7) is proportional to
|
S
||
T
|
. This parsimony was achieved
thanks to Lemma 1.
The complexity of the whole stationary state(
s
1
,
...
,
s
m
) formula is therefore
2
proportional to
|
S
||
T
|
as well.
Petri nets with bounds
The above reasoning was true for a general type of Petri nets. In some cases however, the use of
modified Petri nets is necessary. In particular this is the case in modeling gene regulatory networks,
when the level of gene expression is bound and discrete. To model such situations we slightly modify
the classical semantics of Petri nets, by introducing the notion of
bounds
. We also show that it is easy to
alter the previously introduced formulae to allow for the changes in the semantics.
The necessary change in semantics will be accomplished by introduction of the
bounding function
,
L
:
S
→
N
, which specifies the upper bounds, imposed on places. At any time, the following condition
must be met by each place
s
:
M
(
s
)
L
(
s
)
(8)
Once the bounds are introduced, an issue arises how does the net behave when the bound is reached in
one or more output places of a case. One option is to consider the case inactive, while the alternative is
