Biomedical Engineering Reference
In-Depth Information
is different on successive attempts because durations are random variables. The
continuity of the probabilistic distribution ensures that the probability two activities
ending simultaneously is zero. Furthermore, the exponential distributions enjoy the
memoryless
property: the time at which a transition of state occurs is independent
of the time at which the last transition occurred. Therefore there is no need to record
the time elapsed to reach the current state. The race condition is implemented by
the Gillespie stochastic algorithm [
12
,
13
], that computes the time evolution of
probability densities for chemical species concentrations. This algorithm models
the kinetics of a set of coupled chemical reactions, taking into account stochastic
effects from low copy numbers of the chemical species. In Gillespie's approach,
chemical reaction kinetics are modeled as a markov process in which reactions
occur at specific instants of time defining intervals that are Poisson-distributed, with
a mean reaction time interval that is recomputed after each chemical reaction occurs.
For each chemical reaction interval, a specific chemical reaction occurs, randomly
selected from the set of all possible reactions with a weight given by the individual
reaction rates.
The reduction semantics of BioSpi is the following
!
Q
j
P
n
z
=y
o
C
:::/
x;r
b
1
1
.:::
C
.x
h
z
i
;r/:Q/
j
..x.y/; r/:P
;
r
0
D
r
0
C
In
x
.Q/
r
1
D
r
1
C
O
u
t
x
.Q/
x;r
b
r
0
r
1
!
P
0
P
x;r
b
r
0
r
1
!
P
0
j
Q
P
j
Q
x;r
b
r
0
r
1
!
P
0
;P
0
Q
0
Q
x;r
b
r
0
r
1
!
P
0
P
Q
P;P
x;r
b
r
0
r
1
!
. x/P
0
x;r
b
r
0
r
1
!
Q
0
. x/P
A reaction is implemented by the three parameters r
b
, r
0
and r
1
,wherer
b
represents the basal rate, and r
0
and r
1
denote the quantities of interacting molecules,
and are computed compositionally by the two functions In
x
and O
u
t
x
.Thesetwo
functions inductively count the number of receive and send operations on a channel
x enable in a process. They are defined as follows
In
x
.
0
/
D
0
X
!
In
x
.
i
;r
i
/:P
i
Djf
.
i
;r
i
/
j
i
2
I
^
sbj.
i
/
D
x
gj
i
2
I
In
x
.P
1
j
P
2
/
D
In
x
.P
1
/
C
In
x
.P
2
/
In
x
.P / if
z
ยค
x
0
In
x
..
z
/P /
D
otherwise
O
u
t
x
is similarly defined, by replaci
ng
any occurrence of In with O
u
t and the
condition sbj.
i
/
D
x with sbj.
i
/
D
x.
