No Slide Title - the Department of Computer and Information Science
Download
Report
Transcript No Slide Title - the Department of Computer and Information Science
Hybrid Systems Modeling and Analysis
of Regulatory Pathways
Rajeev Alur
University of Pennsylvania
www.cis.upenn.edu/~alur/
LSB, August 2006
Hybrid Systems
State machines + Dynamical systems
on
dx/dt=kx
x<70
Automotive
x>68
x<63
Coordination
Protocols
off
dx/dt=-k’x
x>60
Robotics
Computer Science
Automata/Logic
Concurrency
Formal verification
+ Control Theory
Optimal control
Stability analysis
Discrete-event system
Software + Environment
Animation
Systems
Biology
Talk Outline
1.
A brief tour of hybrid systems research
2.
Application to regulatory pathways
Thanks to many colleagues in Penn’s Bio-Hybrid Group, including
Calin Belta (Boston U)
Franjo Ivancic (NEC Labs)
Vijay Kumar
Harvey Rubin
Oleg Sokolsky …
See http://www.cis.upenn.edu/biocomp/
Hybrid Automata
Set L of of locations, and set E of edges
Set X of k continuous variables
State space: L X Rk, Region: subset of Rk
For each location l,
Initial states: region Init(l)
Invariant: region Inv(l)
Continuous dynamics: dX in Flow(l)(X)
For each edge e from location l to location l’
Guard: region Guard(e)
Update relation over Rk X Rk
Synchronization labels (communication information)
(Finite) Executions of Hybrid Automata
State: (l, x) such that x satisfies Inv(l)
Initialization: (l,x) s.t. x satisfies Init(l)
Two types of state updates
Discrete switches: (l,x) –a-> (l’,x’) if there is an a-labeled
edge e from l to l’ s.t. x satisfies Guard(e) and (x,x’)
satisfies update relation Jump(e)
Continuous flows: (l,x) –f-> (l,x’) where f is a continuous
function from [0,d] s.t. f(0)=x, f(d)=x’, and for all t<=d, f(t)
satisfies Inv(l) and df(t) satisfies Flow(l)(f(t))
CHARON Language Features
Individual components described as agents
Composition, instantiation, and hiding
Individual behaviors described as modes
Encapsulation, instantiation, and Scoping
Support for concurrency
Shared variables as well as message passing
Support for discrete and continuous behavior
Differential as well as algebraic constraints
Discrete transitions can call Java routines
Walking Model: Architecture and Agents
• Input
– touch sensors
• Output
– desired angles of each
joint
• Components
– Brain: control four legs
– Four legs: control servo
motors
• Instantiated from the
same pattern
Walking Model: Behavior and Modes
v
x
dx = -v
x > stride /2
dy = kv
L1
L2
j1
j2
y
dy = -kv
dx = kv
x < stride /2
(x, y)
CHARON Toolkit
Reachability Analysis for Dynamical Systems
Goal: Given an initial region, compute whether a bad state can be
reached
Key step: compute Reach(X) for a given set X under dx/dt = f(x)
Reach(X)
X
Polyhedral Flow Pipe Approximations
t3
t4
t5
t6
t7
t8
t2
t1
X0
t9
• divide R[0,T](X0) into [tk,tk+1] segments
• enclose each segment with a convex polytope
• RM[0,T](X0) = union of polytopes
Abstraction and Refinement
Abstraction-based verification
Given a model M, build an abstraction A
Check A for violation of properties
Either A is safe, or is adequate to indicate a bug in M, or gives
false negatives (in that case, refine the abstraction and repeat)
Many projects exploring abstraction-based verification
for hybrid systems
Predicate abstraction (Charon at Penn)
Counter-example guided abstraction refinement (CEGAR at CMU)
Qualitative abstraction using symbolic derivatives (SAL at SRI)
Predicate Abstraction
Input is a hybrid automaton and a set of k boolean
predicates, e.g. x+y > 5-z.
The partitioning of the concrete state space is specified by
the user-defined k predicates.
x
t
Concrete Space:
LxRn
Abstract Space:
L x {0,1} k
Overview of the Approach
Hybrid
system
Safety
property
Boolean
predicates
additional
predicates
Search in abstract space
No!
Counter-example
Real
counterexample
found
Property
holds
Analyze counter-example
Hybrid Systems Wrap-up
Efficient simulation
Accurate event detection
Symbolic simulation
Computing reachable state-space
Many new techniques emerging: level sets, Zenotopes,
dimensionality reduction..
Scalability still remains a challenge
Cellular Networks
Networks of interacting biomolecules carry out many
essential functions in living cells (gene regulation, protein
production)
Both positive and negative feedback loops
Design principles poorly understood
Large amounts of data is becoming available
Beyond Human Genome: Behavioral models of cellular
networks
Modeling becoming increasingly relevant as an aid to narrow
the space of experiments
Model-based Systems Biology
Goal A: Provide notations for describing complex systems
in a modular, structured manner
Principles of concurrency theory (e.g. compositionality)
Hierarchy, encapsulation, reuse
Visual programming tools
Goal B: Simulation and analysis for better understanding
Classical debugging tools
Reachability and stability analysis
Model-based experiments to combat the combinatorial explosion
due to multiplicity of parameters
What to Model ?
Cellular networks exhibit a complex mix of features
Discrete switching as genes are turned on/off
High degree of concurrency
Stochastic behavior (particularly at low concentrations)
Chemical reactions
Models possible at different levels of abstractions
Discrete graph models capturing dependencies
Boolean models capturing qualitative states
Purely continuous models
Hybrid systems
Stochastic models
Location-aware models
Regulatory Networks
gene expression
-
negative
gene
START
regulation
positive
+
transcription
translation
nascent
protein
cell-to-cell
signaling
chemical
reaction
STOP
Luminescence / Quorum Sensing
in Vibrio Fischeri
Hybrid Modeling
d ( LuxR ) biological systems
LuxR are modeled using smooth functions.
Traditionally,
Tl luxR
dt
H sp
d[ x]
synthesis decay transform
transport
( X , , )
dt
b
d
rLuxR
Ai
LuxR
r
Co kG LuxR
1
/ Ai
LuxR / Ai
Xm
CRP
+
negative
0.5
Xm
Xm
1 Xm
2
X sw
X sw
START
luxR gene
X
STOP
regulation
positive
transcription
translation
-
protein
LuxR
Ai
chemical
reaction
d ( luxR )
Tc [ ( CRP , CRP , CRP )
dt
( 1 ( LuxR Ai , LuxR Ai , LuxR Ai )) b )
Ai
luxR
kG luxR
H RNA
Hybrid Modeling
Essentially
hybrid
system
Discrete jump
(mRNA)
regulatory
protein/complex
mode
high conc
continuous model
Nonlinear dynamics
(proteins involved in
chemical reactions)
Linear dynamics
(proteins not involved
in chemical reactions)
At low
concentrations,
a continuous
approximation
model might
not be
appropriate.
Instead, a
stochastic
model should
be used.
low conc
stochastic model
In some cases,
the biological
description of
a system is
itself hybrid.
Luminescence Regulation
+
CRP
cAMP
OL
OR
lux box
luxR
luxICDABEG
CRP binding site
LuxR
-
+
Ai
LuxI
LuxA
LuxR
LuxB
Ai
Substrate
luciferase
Reachability
lum
x Ax b10
x8 x8 sw
non-lum
x8 x8 sw
x Ax b00
x8 x8 sw
x8 x8 sw
x Ax bi0
c0 0 , c1 1
Under what conditions
x4 bacteriumswitch
H RNATlon
Tc (the
ci light?
b )
can the
x x7
x8
bi0
0
0
x8 ( Co )
lum dynamics
x8 sw
switching surface
nonlum dynamics
x4 ( LuxI )
x7 ( Ai )
Simulation Results
external Ai
(input)
luminesence
(output)
switch
history
switch
history
concentrations
for various
entities
BioSketchPad
Interactive tool for graphical models of biomolecular and
cellular networks
Nodes and edges with attributes
Hierarchical
Intended for use by biologists
Compiler to translate BioSketchPad models to Charon
BioSketchPad Concepts
Species nodes
Name (e.g. Ca, alcohol dehydrogenase, notch)
Type (e.g. gene, protein)
Location (e.g. cell membrane, nucleus)
N-mer polymerization, electrical charge
Initial concentration
Reaction nodes
Input and output connectors
Type (e.g. transformation, transcription)
Parameters for rate laws
Regulation nodes
Connected to species nodes and/or reaction nodes to modulate the
rate of reaction by concentration of species
Weighted sum, tabular, product forms
Summary
Hybrid systems are useful to model some biological
regulatory networks.
The simulation/reachability results of the luminescence
control in Vibrio fischeri are in accordance with phenomena
observed in experiments.
Modeling concepts such as hierarchy, concurrency, reuse,
are relevant for modular specifications
BioSketchPad integrates many of these ideas
Challenges
Finding all the information needed to build a model is
difficult
Finding people who can build models is even more difficult
Finding a common format for exchanging models among tools
can make more models available
Scalability of analysis