paradise Parameter Scanning by Parallel Model Checking with applications in Systems Biology HIBI 2010 University of Twente David Šafránek with Jiˇrí Barnat, Luboš Brim, Martin Vejnár Masaryk University Brno 1st October, 2010 Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 1 / 27 paradise Outline 1 Motivation and Background 2 Method Description 3 Case Study Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 2 / 27 paradise Outline 1 Motivation and Background 2 Method Description 3 Case Study Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 3 / 27 paradise Motivation Tuning the Biological Models complex system biological model S M in vitro/in vivo formal in silico model parameters scanning of the proper parameter values the set of unknown model parameters χ traditional methods of fitting models to in vitro data property-driven parameter scanning ⇒ find the parameter values exibiting the given dynamic phenomena To learn the rat dancing... Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 4 / 27 paradise Modeling Approach How to obtain a finite abstraction? [ECMOAN (BioDiVinE, GNA), RoVerGeNe] continuous trajectories overapproximation discrete abstraction ODE model Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 5 / 27 paradise Modeling Approach How to obtain a finite abstraction? [ECMOAN (BioDiVinE, GNA), RoVerGeNe] continuous trajectories overapproximation discrete abstraction num. simulation [COPASI, BioCHAM, BioNessie] underapproximation ODE model Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 5 / 27 paradise Modeling Approach How to obtain a finite abstraction? continuous trajectories overapproximation discrete abstraction approximate finite time series local view (initial condition) num. simulation [COPASI, BioCHAM, BioNessie] underapproximation ODE model Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 5 / 27 paradise Modeling Approach How to obtain a finite abstraction? continuous trajectories overapproximation rectangular abstraction [BioDiVinE, GNA, RoVerGeNe] num. simulation [COPASI, BioCHAM, BioNessie] underapproximation ODE model Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 5 / 27 paradise Modeling Approach How to obtain a finite abstraction? continuous trajectories overapproximation rectangular abstraction global view finite automaton [BioDiVinE, GNA, RoVerGeNe] num. simulation [COPASI, BioCHAM, BioNessie] underapproximation ODE model Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 5 / 27 paradise Modeling Approach Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 6 / 27 paradise Modeling Approach different parameter values lead to different transitions Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 6 / 27 paradise Problem Definition Robustness Given a dynamic (temporal) property ϕ and a parameterized model M(χ) check if M(p) |= ϕ holds for all possible parameterizations p (valuations of χ). Parameter Scanning Problem Given a dynamic (temporal) property ϕ and a parameterized model M(χ) find the maximal set P of parameterizations of χ such that M(p) |= ϕ for all p ∈ P. Problem Reduction Robustness is reduced to Parameter Scanning Problem by taking the set of all possible parameterizations as P. Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 7 / 27 paradise Related Work BioCHAM [Fages et.al.] based on numerical simulation LTL with constraints interpreted over simulations notion of “satisfaction degree” defined analysis dependent on precise initial conditions RoVerGeNe [Batt et.al.] model checking over a finite discrete abstraction properties “decidable” globally BDD representation of parameter space w.c.s.: two model checking operations per each parameterization computationaly hard (3 variable model hours-days of computing) our contribution revisit the latter approach new algorithm based on enumerative LTL model checking parallel implementation Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 8 / 27 paradise Rectangular Abstraction B A A B 0 2 3 5 B: 0 1065 A: Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 9 / 27 paradise Supported Classes of Models Mass Action Kinetics biochemical reactions modeled by mass action kinetics the supported format of reactions: γ1X1 + · · · + γmXm k → δ1Y1 + · · · + δnYn, γi ∈ {0, 1} resulting ODE system describes dynamics of each variable (chemical species): ∀i ∈ {1, ..., n}. dYi dt = f(X1, ..., Xm) = kXγ1 1 Xγ2 2 · · · Xγm m ∀i ∈ {1, ..., m}. dXi dt = f(X1, ..., Xm) = −kXγ1 1 Xγ2 2 · · · Xγm m k ∈ R+ is kinetic parameter Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 10 / 27 paradise Supported Classes of Models Regulatory Kinetics protein dynamics driven by protein-regulated transcription Hill kinetics approximated in terms of ramp functions X −→ Y dY dt = kr+ (X, xt1, xt2) k ∈ R+ is kinetic parameter xt1, xt2 determine the partitioning of X xt1 xt2 1 0 [X] r+(X,xt1,xt2) Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 11 / 27 paradise Supported Classes of Models Mixing the Both we combine both kinetics aspects under one ODE formalism right-hand side of any ODE is a function f(X, p) where p is a vector of unknown parameters (piece-wise) multi-affine in X affine in p these properties enable us to (are necessary to): make a discrete finite overapproximation of the system dynamics finitely represent the parameter space – possible values of p linear combinations of unknown parameters not considered ⇒ at most one unknown parameter per equation ⇒ simple manipulation with the parameter space Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 12 / 27 paradise The Principle of Rectangular Abstraction approach of Belta, Habets, van Schuppen continuous solutions abstracted by a non-deterministic automaton A B Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 13 / 27 paradise The Principle of Rectangular Abstraction approach of Belta, Habets, van Schuppen continuous solutions abstracted by a non-deterministic automaton A B Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 13 / 27 paradise The Principle of Rectangular Abstraction approach of Belta, Habets, van Schuppen continuous solutions abstracted by a non-deterministic automaton A B Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 13 / 27 paradise Analysed Properties reasoning about concentration levels (up-to the abstraction) reachability global: regardless the initial state, B eventually falls below 2 local: if B initally below 2 then B does not exceed 2 temporal properties there is no initial state from which A falls below 6 before A exceeds 6 time progress 0 5 10 6 A(t): properties can be formulated in Linear Temporal Logic (LTL) Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 14 / 27 paradise Outline 1 Motivation and Background 2 Method Description 3 Case Study Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 15 / 27 paradise Computing the Parameter Space k2 = 0.8 k1 =? [A] [B] 1 2 3 45 (0.8,1.6) value of k1: (1.6,max)(0.4,0.8)(0,0.4) 1 2 3 4 5 Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 16 / 27 paradise Effect of Parameters on Abstraction Automaton [A] [B] 5 0 2.5 5 2.5 [A] [B] 5 0 2.5 5 2.5 [A] [B] 5 0 2.5 5 2.5 [A] [B] 5 0 2.5 5 2.5 Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 17 / 27 paradise Parameter Scanning by LTL Model Checking [A] [B] 5 0 2.5 5 2.5 x we compute all parameterizations together check if the product accepts an empty language normally for each parameterization separately YES NO counterexample may be a false positive is the maximal set of valid parameters may be underapproximated never claim Buchi automatonparameterized Kripke structure of the model set of parameter values P violating the property inverse of P in entire parameter space property is robust GF ([A]>2.5 | [B]>2.5) FG ([A]<=2.5 & [B]<=2.5) Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 18 / 27 paradise Model Checking on Coloured Graphs Idea represent each parameterization by a distinct colour assume all transitions for each parameterization adequately coloured find accepting cycles and get colours enabling accepting runs Procedure 1 compute initial mapping of colours to states ⇒ propagate colours through the entire graph (BFS reachability) ⇒ states on accepting cycles know all colours by which they are reached 2 for each reachable accepting cycle aggregate (scan) the valid colours Complexity Issues worst case: O(|S| · |E| · |F| · |P|) |S|...states, E...edges, F...accepting states, P...colours in expected cases |S| is reduced (levels of BFS) Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 19 / 27 paradise Parallel Implementation Problem number of states exponential w.r.t. number of variables size of the parameter space exponential w.r.t. number of unknown parameters many computations performed on a single graph Solution multi-core data-parallel implementation of colour mapping propagation states evenly distributed among threads by a hash-function each thread responsible for a unique partition of colour mapping threads communicate via a colour mapping update qeue implemented as a set of lock-free qeues one qeue per thread threads synchronize on BFS levels Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 20 / 27 paradise Outline 1 Motivation and Background 2 Method Description 3 Case Study Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 21 / 27 paradise Case Study I – E. Coli Ammonium Transport Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 22 / 27 paradise E. Coli Ammonium Transport: Model Settings Settings mass action kinetics ⇒ multi-affine ODE model abstraction – number of discrete concentration levels considered: AmtB AmtB : NH3 AmtB : NH4 NH3in NH4in 7 9 3 8 26 initial conditions set to impose low external ammonium conditions Experiments find the maximal set of parameter values for the given uknown parameter ensuring the maximal reachable level of internal NH3 is 1.1 · 106 mol the employed LTL property: G(NH3in < 1.1 · 106 ) Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 23 / 27 paradise E. Coli Ammonium Transport: Experiments χ intervals of validity time k4 (1 · 10−12, 2.7 · 106) 30 s k6 (5.2 · 106, 1 · 1012) 22 s k7 (1 · 10−12, 3.3 · 106) 33 s k9 (1 · 10−12, 2.7 · 106) 20 s k1,6,10 see the paper 19 min Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 24 / 27 paradise Case Study II – Genetic Regulation of G1/S Transition central module controlling G1/S transition of mammalian cells bistability w.r.t. setting of γpRB parameter in the range [0.01, 0.1] liveness property FG[E2F1] > 8 many false-positive runs arise due to time-convergent behaviour introduced by abstraction in the paper we present a (non-universal) solution Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 25 / 27 paradise Conclusions new algorithm introduced (model checking on coloured graphs) scalability achieved on a multi-core implementation full support of multi-affine ODE models case studies show practicability for common models large-scale models still a challenge for simple parameter scanning problems effective alternative to RoVerGene future work reduction of false-positives distributed implementation computation of more complicated parameter spaces other application of the idea of model checking on coloured graphs Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 26 / 27 paradise Thank you for your attention! Šafránek et al. (FI MU Brno) Parameter Scanning by PMC 27 / 27