Transcript Model Checking Genetic Regulatory Networks with Parameter

Model Checking Genetic
Regulatory Networks with
Parameter Uncertainty
Grégory Batt, Calin Belta, Ron Weiss
HSCC 2007
Presented by Spring Berman
ESE 680-003: Systems Biology
Motivation

Uncertainty in biological parameters limits the
development and analysis of models of genetic
regulatory networks
- Sources: gene expression noise, mutation, cell death,
changing intra- and extra-cellular environments
- Direct determination of rate constants in vivo is still
inaccurate and nontrivial [1]

Network tuning is a central problem in synthetic biology
- Most initial attempts at building gene networks fail to
produce the desired behavior [1]
[1] E. Andrianantoandro, S. Basu, D. Karig, R. Weiss: Synthetic biology: New
engineering rules for an emerging discipline. Mol. Syst. Biol. (2006)
Objective
Problem 1: [Robustness analysis]
Check whether a dynamical property is satisfied by
every parameter in a given set and for every initial
state in a given region.
Problem 2: [Parameter constraint synthesis]
Find a subset of a given parameter set that satisfies a
certain dynamical property.
* Assume no sliding modes
Approach
1) Model genetic network with piecewisemultiaffine (PMA) differential equations
2) Formulate the property to be checked in
Linear Temporal Logic (LTL)
3) Define an embedding transition system for
the PMA model and its discrete
abstraction
4) Define a hierarchy of parameter
equivalence classes
5) Explore the parameter space efficiently
Approach
1) Model genetic network with piecewisemultiaffine (PMA) differential equations
2) Formulate the property to be checked in
Linear Temporal Logic (LTL)
3) Define an embedding transition system for
the PMA model and its discrete
abstraction
4) Define a hierarchy of parameter
equivalence classes
5) Explore the parameter space efficiently
PMA models of genetic networks
State vector:
n genes; xi = concentration of protein encoded by gene i
Parameter vector:
Network dynamics:
Production rate
possibly uncertain
Degradation rate
parameters
Regulation function (products of ramp functions)
Example: Toggle Switch
repressor
protein
repressor
protein
gene
gene
Approach
1) Model genetic network with piecewisemultiaffine (PMA) differential equations
2) Formulate the property to be checked in
Linear Temporal Logic (LTL)
3) Define an embedding transition system for
the PMA model and its discrete
abstraction
4) Define a hierarchy of parameter
equivalence classes
5) Explore the parameter space efficiently
Dynamical Property as LTL Formula

Temporal Logic : System for describing how the truth of
assertions changes over time

Linear: Events occur along a single timeline

Dynamical property of a gene network can be expressed as an
LTL formula, which is built from:
- Atomic propositions; in this case:
,
,
- Boolean operators
not ( ),
and ( ), or ( )
- Temporal operators [2]
Fp = eventually p, Gp = always p, p U q = p until q
[2] E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, ed., Handbook of
Theoretical Computer Science, vol B, pp. 995-1072. MIT Press, 1990.
Example: Toggle Switch
Bistability property expressed in LTL:
If concentration of A is low and B is high, then
the system always remains in this state
If concentration of A is high and B is low, then
the system always remains in this state
Approach
1) Model genetic network with piecewisemultiaffine (PMA) differential equations
2) Formulate the property to be checked in
Linear Temporal Logic (LTL)
3) Define an embedding transition system for
the PMA model and its discrete
abstraction
4) Define a hierarchy of parameter
equivalence classes
5) Explore the parameter space efficiently
Embedding Transition System

PMA system:
= PMA function;
Partition
= set of all atomic propositions
into rectangles:
is a threshold constant or atomic proposition constant

Embedding Transition System associated with
:
Parameter vector
Union of all rectangles in
Transition relation:
iff a path from x to x’ ,
where x and x’ are in the same or adjacent rectangles
Satisfaction relation:
iff x satisfies proposition π
Discrete abstraction

Finite transition system preserving dynamical
properties of

Discrete abstraction of
:
Set of rectangles (equivalence classes)
Transition relation:
iff R = R’ , or R is adjacent to
R’ and there is a vertex v on the shared facet such that:
(exploits convexity property of MA functions on rectangles)
Satisfaction relation:
iff for every
Example: Toggle Switch
Continuous dynamics
Discrete abstraction
Property Verification

A parameter set P is valid for an LTL formula 
iff
for almost all
:


Can compute
whether

If
and use model checking to test
, no conclusion on validity of p…
Approach
1) Model genetic network with piecewisemultiaffine (PMA) differential equations
2) Formulate the property to be checked in
Linear Temporal Logic (LTL)
3) Define an embedding transition system for
the PMA model and its discrete
abstraction
4) Define a hierarchy of parameter
equivalence classes
5) Explore the parameter space efficiently
Parameter equivalence classes

f is a piecewise-affine, continuous function of p
partition the parameter space into polyhedra;
represent these regions by Boolean numbers

Define parameter sets:

If for some
then for all
; just need to test a random p per
(but exponential increase with number of predicates)
Example: Toggle Switch
32 affine expressions, only 4 non-constant ones
Parameter
space
Example: Toggle Switch
Hierarchy among parameter sets
Parameter equivalence classes
Valid for
bistability property
Approach
1) Model genetic network with piecewisemultiaffine (PMA) differential equations
2) Formulate the property to be checked in
Linear Temporal Logic (LTL)
3) Define an embedding transition system for
the PMA model and its discrete
abstraction
4) Define a hierarchy of parameter
equivalence classes
5) Explore the parameter space efficiently
System over- and under-approximations
Contains all transitions present in at least one
Contains only transitions present in all
(A)
(B)
(C)
or
, inspect subsets of P
 Algorithm: Recursively explore the tree of parameter sets,
starting from
; stop search at condition (A) or (B)
Computation of
,
iff R = R’ , or R is adjacent to R’ and
iff R = R’ , or R is adjacent to R’ and

f is affine in p 
Computation of
of polytopes

are unions of polytopes
,
= intersections and inclusions
Implementation in RoVerGene
(Robust Verification of Gene Networks)
Grégory Batt, Calin Belta
http://iasi.bu.edu/~batt/rovergene/rovergene.htm
 Multi-Parametric
Toolbox for polyhedral operations
 Library matlabBGL for graph operations
 CTL/LTL model checker NuSMV
Tuning of a transcriptional cascade


Analysis of steady-state input/output behavior of synthetic
transcriptional cascade made of 4 genes
PMA model of system; 5-D state space (4 states, 1 input)
input
output

EYFP should increase at least 1000x for a 2x increase in aTc
Results


Actual network does not meet specifications;
used RoVerGeNe to find a valid parameter set by
tuning 3 production rates
1500 rectangles, 18 affine predicates, >200,000 equivalence
classes, 350 parameter sets analyzed, < 2 hours runtime