Biology Reference
In-Depth Information
In our model, a transition represents a chemical reaction. In chemical systems, usually more than one
reaction takes place over a given period of time. To model the concurrency of a chemical system, we
will use the notion of a case as introduced in Definition 8. So instead of firing one transition at a time
we will fire one case at a time. In this approach a
stationary state
can be viewed as a special marking
which is invariant with respect to cases of that marking. Definition 10 formalizes this notion.
Definition 10.
(Stationary state):
A marking
M
of a given net
N
is said to be
stationary
if for every case
P
in this marking we have
M
[
P
M
.
One must realize that the concept of a stationary state as introduced above is only a mathematical
model of a real world situation. The complexity of the model influences the computational complexity:
the more realistic the model is, the harder it is to analyze. Our Definition 10 is only an approximation of
what we observe in reality; however we think it might be useful.
The intuition behind Definition 10 is as follows: transitions correspond to chemical reactions and
cases correspond to maximal groups of reactions that can take place simultaneously. We assume that
reactions always take place in groups (case firing). With this in mind, a stationary state is a state that is
left unchanged no matter what group of reactions takes place. This reflects the concept of a chemical
equilibrium, reactions take place, but the quantities of reactants are left unchanged.
Presburger arithmetic
Once we have defined the notion of a stationary state in terms of Petri nets, we need a tool to find and
test such states. We propose an approach based on
Presburger arithmetic
formulae. For a given network
we describe a way to construct a formula with free variables
s
1
,
s
2
,
...
that correspond to places of the
network. Such a formula is satisfied if and only if the values assigned to the variables form a stationary
state. Hence, the satisfying valuations of the variables
s
1
,
s
2
,
...
correspond to all the stationary states.
We do not present any specific algorithm for constructing the formula, only an idea is given. However
the steps described here can be easily translated into an efficient automated procedure.
Presburger arithmetics has been chosen since it has decidable validity problem (see, for instance,
[Oppen, 1978]. Furthermore, the set of all valuations satisfying a given formula is a semi-linear set
[Ginsburg and Spanier, 1966], hence admits a finite representation. In addition, this semi-linear set
can be effectively constructed. In our setting this means that the set of all stationary states can be
effectively computed, by combining construction of the Presburger formula presented below and solving
this formula.
We give some basic definitions first, and then we describe the formula for a given network. At the end
of this section we introduce a variation of the semantics of Petri net and show that it is easy to extend the
formula to match the modified semantics.
Definition 11.
(Presburger arithmetic):
Presburger arithmetic is first order theory of natural number with
addition. The signature is
(
N
,
+
,
0
,
1
,
=
)
where “
+
” is a two argument function, “0”, “1” are constants
and “
=
” is the equality predicate. The formulae are built by first-order quantification
(
∀
x
φ,
∃
x
φ
)
and
boolean connectives
(
∧
,
∨
,
¬
, etc.)
from the atomic equality predicates.
Remark 1.
The inequality relation can be defined in Presburger arithmetic as:
x<y
⇔∃
z
y
=
x
+
z
+1
,
