I NTRODUCTION
P RELIMINARIES
M APPING TO HA
Hybrid approximation of
stochastic Concurrent Constraint Programming
Luca Bortolussi1
Alberto Policriti2,3
1 Dipartimento
di Matematica ed Informatica
Università degli studi di Trieste
2 Dipartimento di Matematica ed Informatica
Università degli studi di Udine
3 Istituto di Genomica Applicata (IGA)
PASTA, London, July 26th-27th, 2007
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
1/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
O UTLINE
1
From SPA to ODE;
2
Behavioral equivalence issues;
3
Being more “discrete” in the translation: SPA to Hybrid
Automata.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
2/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
T HE GENERAL PICTURE
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
3/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
D ISTILLED S CCP
Variables: X = {X , Y , . . .}, real valued.
Updates: X = X + 1, constant update.
Basic actions: π = (X > 0 → X = X − 1), guarded
updates.
Functional rates: λ : Rk → R+ , depending on some
variables of the system
Stochastic actions: [π]λ
Sequential Agents: defined using choice, sequential
composition, and constants.
System or network: parallel composition of sequential
agents.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
4/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
G ENERATING ODE S : EXAMPLE
E XAMPLE
A :- [true → X = X + 1]λ1 .B
B :- [true → X = X − 1]λ2 .A
T HE RTS
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
5/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
F ROM S CCP TO ODE: EXAMPLE
I NTERACTION MATRIX AND REACTION VECTOR
t1
t2
X 1 −1
I=
A −1 1
B 1 −1
r=
λ1 · A
λ2 · B
ode = I · r

 Ẋ = λ1 · A − λ2 · B
ode
Ȧ = −λ1 · A + λ2 · B

Ḃ = λ1 · A − λ2 · B
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
6/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
T HE STRANGE BEAST OF REPRESSILATOR
M ODELING 3 N EGATIVE G ENE G ATES
Neg(X , R) :-
[true → X = X + 1]kp .Neg(X , R)
+ [R ≥ 1 → ∅]kb R .[true → ∅]ku .Neg(X , R)
Degrade(X ) :- [X > 0 → X = X − 1]kd X .Degrade(X )
Neg(A, C) k Neg(B, A) k Neg(C, B) k Degrade(A) k Degrade(B)
k Degrade(C)
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
7/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
ODE FOR S CCP-R EPRESSILATOR





























L. B ORTOLUSSI
Ȧ = kp YA − kd A
Ḃ = kp YB − kd B
Ċ = kp YC − kd C
Ẏ1 = ku ZA − kb YA C
Ẏ2 = ku ZB − kb YB A
Ẏ3 = ku ZC − kb YC B
Ż1 = kb YA C − ku ZA
Ż2 = kb YB A − ku ZB
Ż3 = kb YC B − ku ZC
H YBRID APPROXIMATIONS
8/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
T HE STRANGE BEAST OF REPRESSILATOR
Repressilator with gene gates
Repressilator in sCCP
Repressilator: ODE from sCCP
Repressilator: average of sCCP model
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
9/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
H YBRID AUTOMATA - I NTUITIVELY
Intuitively, a hybrid automaton is a finite state automaton H with
continuous variables Z such that:
H evolves from Z to Z0 in time T according to differential
equations Ż = f(Z)
Z must always satisfy invariant conditions in each state
H can cross an edge e only when guards on Z are true
(activation conditions)
when H crosses e, some variables may be reset.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
10/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
F ROM S CCP TO H YBRID AUTOMATA
W HAT ?
We want to associate an hybrid automaton to a “sCCP network”.
W HY ?
The mixed discrete/continuous dynamics of HA is more natural, as it
can preserve the logical structure of sCCP models.
Hybrid automata are equipped with well developed analysis methods.
H OW ?
The separation between constraint store (variables) and logical
description of agents makes easy to identify (discrete) modes of the
automata
Activation conditions need to look at the temporal semantics of
stochastic actions.
L. Bortolussi, A. Policriti. Hybrid approximation of Stochastic Concurrent Constraint Programming, 2007.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
11/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
E XAMPLE : A “ DISTILLED ” R EPRESSILATOR
+
+
[true → X = X + 1]k+ .A
[X > 0 → X = X − 1]k X .A
−
[true → ∅]k .B
+
+
[true → X = X + 1]k .B
−
[X > 0 → X = X − 1]k+ X .B
[true → ∅]k .A
A :-
B :-
0
0
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
12/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
HA ASSOCIATED TO AN S CCP- NETWORK
I DEAS : States and Flows
States of the HA correspond to
products of states of the RTS:
Σ = (σ1 , . . . , σn ).
Flows for system variables are
obtained localizing the
construction of ODEs to looping
edges.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
13/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
HA ASSOCIATED TO AN S CCP- NETWORK
I DEAS : HA-edges
HA-edges change the state of
just one RTS.
Associate variables Yij to edges
for activation conditions.
The flow for Yij is given by the
non constant rate: Ẏij = λij (X)
Activation conditions take into
account the guard of the
RTS-edge plus Yij ≥ 1.
Resets correspond to updates of
the RTS-edge.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
14/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
W HY Y ≥ 1
Non-homogeneous Poisson process, with rate λ = λ(t).
Rt
Cumulative rate: Λ(t) = t0 λ(s)ds
Average number of firings at time t: Λ(t).
At least one firing on average: Λ(t) ≥ 1.
Λ̇(t) = λ(X(t))
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
15/19
I NTRODUCTION
P RELIMINARIES
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
M APPING TO HA
16/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
H YBRID R EPRESSILATOR
Repressilator with gene gates
Repressilator in sCCP
Repressilator: ODE from sCCP
Hybrid Repressilator from sCCP
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
17/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
A NALYSIS OF H YBRID R EPRESSILATOR
Determinism vs non-determinism
L. B ORTOLUSSI
Stability
H YBRID APPROXIMATIONS
18/19
I NTRODUCTION
P RELIMINARIES
M APPING TO HA
C ONCLUSIONS
sCCP to ODE: problems (the stochastic component
averaged away).
Localize the above technique and keep a discrete portion
from the network: Hybrid Automata (with the right control
variables).
N EXT STEPS
Relax the definition of sCCP-networks for which the
technique works.
Define a lattice of HAs.
Formalize the behavioral properties to guide/determine the
level of discreteness to maintain.
L. B ORTOLUSSI
H YBRID APPROXIMATIONS
19/19