Biology Reference
In-Depth Information
this condition is met. Since the choice of
s
and
t
was arbitrary, the condition is met for all pairs of
s
and
t
.
Now let's suppose that the condition from the lemma is met. In that case for any chosen
s
and
t
, the
following is true:
(
W
(
t
,s
)
−
W
(
s, t
))
W
(
s, t
)
.
M
(
s
)+
(1)
t
∈
s
−
)
(
A
∩
\{
t
}
The value of the left-hand side of Eq. (1) is the smallest reachable marking of
s
, before
t
is fired,
when firing the transitions from
A
in marking
M
. Since the choice of
s
was arbitrary,
t
will be fireable
regardless of the firing order of transitions in
A
. And, since the choice of
t
was also arbitrary, this
reasoning applies to all transitions in
A
. Therefore
A
is non-conflicting.
To avoid the exponential growth of the size of formula, we use the condition from Lemma 1 to express
that a set is non-conflicting. But instead of writing a single sub-formula for every possible subset of
T
, we quantify over variables
t
1
,
...
,
t
n
, which correspond to transitions in
T
. There are 2
n
possible
valuations of these variables and each valuation represents a different subset
A
⊆
T
.
That is
t
i
=
1
⇔
A
.
Note that, depending on the context,
t
i
and
s
j
denote either variables or elements of the net.
A condition for a marking to be a stationary is expressed by the following stationary state(
s
1
,
...
,
s
m
)
formula:
t
i
∈
∀
t
1
,...,t
n
(
t
1
1
∧
...
∧
t
n
1)
∧
case
(
s
1
,...,s
m
,t
1
,...,t
n
)
⇒
balance
(
t
1
,...,t
n
)
.
(2)
Below we use
1
i
m
p
(
s
i
)
∧
and
1
j
n
p
(
t
j
)
∧
as a shorthand for
p
(
s
1
)
∧
...
∧
p
(
s
m
)
and
p
(
t
1
)
∧
...
∧
p
(
t
n
)
, respectively. For instance, Eq. (2) can be
rewritten as:
t
1
,...,t
n
∀
∧
n
t
j
1
∧
case
(
s
1
,...,s
m
,t
1
,...,t
n
)
⇒
balance
(
t
1
,...,t
n
)
.
(3)
1
j
The subformula balance (
t
1
,
...
,
t
n
)
is standing for:
1
i
m
(
t
1
(
s
i
)
∗
∧
t
1
+
...
+
t
n
(
s
i
)
∗
t
n
=0)
.
(4)
The intuition for balance (
t
1
,
...
,
t
n
)
is that transitions belonging to the set determined by the valuation
of
t
1
,
...
,
t
n
must have balance equal to 0. The size of the formula is proportional to
|
|
.
Note that
t
j
(
s
i
)
may be of negative value. However this is not a problem because the negative values
can be moved to the right-hand side of the equality predicate.
The formula case (
s
1
,
...
,
s
m
,
t
1
,
...
,
t
n
) is more complicated. Its intended meaning is that in the
marking determined by valuation of variables
s
1
,
...
,
s
m
, the set of transitions determined by valuation
of variables
t
1
,
...
,
t
n
is a case. To guarantee that the latter set is maximal, we introduce additional
variables:
S
||
T
t
1
,
...
,
t
n
∈{
0, 1
}
, such that for
i
t
i
.
∈{
1,
...
,
n
}
,
t
i
The valuation of the newly
