Biology Reference
In-Depth Information
and the non-strict inequality as:
x
y
⇔∃
z
y
=
x
+
z.
Remark 2.
Presburger arithmetics contains no multiplication
(
adding this operator would make the
validity problem undecidable
)
. But we can still speak about multiplication by a constant. For
c
∈
N
,
we will use a shorthand:
c
∗
x
=
x
+
.
..
+
x
.
ctimes
Logical description of stationary states
Let
N
=
(
S
,
T
,
F
,
W
,
M
0
)
be a fixed Petri net in the sequel. Without loss of generality we assume
S
=
{
s
1
,
...
,
s
m
}
and
T
=
{
t
1
,
...
,
t
n
}
, where
m
=
|
S
|
and
n
=
|
T
|
are cardinalities of
S
and
T
,
respectively.
Below we show how to construct a formula with free variables
s
1
,
...
,
s
m
such that for a given
valuation
v
the formula is satisfied if and only if corresponds to a stationary state. We allow ourselves
to use the same symbol
s
i
S
, depending on the context, either to denote the place of , or as a variable
in the formula that corresponds to that place. Similarly for transitions
t
j
∈
∈
T
. We hope that such an
overloading of symbols does not lead to confusion but improves readability.
A straightforward approach is to directly translate the definition of a stationary state to a Presburger
arithmetic formula. Unfortunately such an approach yields a formula of exponential size. But a more
sophisticated approach, proposed below, allows one to construct a formula of polynomial size.
Definition 12.
For a given place
s
∈
S
the following two sets are defined:
s
−
=
{
•
t
∈
T
|
t
(
s
)
<
0
}
,
s
+
s
−
.
•
=
T
\
Set
s
−
contains the transitions with negative balance with respect to the place
s
, and
s
+
contains the
remaining transitions.
Lemma 1.
For a given net
N
and its marking
M
, a set
A
⊆
T
is non-conflicting if and only if the
following condition is met, for each
s
∈
S
and
t
∈
A
:
t
(
s
)
M
(
s
)+
W
(
s, t
)
.
t
∈
(
s
−
∩
A
)
\{
t
}
Proof
: For a non-conflicting set
A
, transitions can be fired sequentially, regardless of the order of firing.
In particular, if we choose some
t
∈
A
and a place
s
∈
S
we can enforce the following order of transition
firing:
(
s
−
∩
s
−
)
\{
A
)
\{
t
}
,t,
(
A
\
t
}
In other words, first we fire the transitions with a negative balance (except for the chosen one) in any
order, then the chosen one, and at last, the remaining transitions in any order. The condition from the
lemma states, that when we are to fire
t
, we can do so with respect to
s
. But since
A
is non-conflicting,
