Probabilistic verification and analysis of biopathway dynamics

Abstract

Computational systems biology deals with the systematic application of computational methods to model and analyze biological systems (often referred as biopathways). Two main paradigms exist for modeling biopathways, the deterministic and the stochastic. In the deterministic approach ordinary differential equations (ODEs) are commonly used while in the stochastic approaches, Markov chains are common. Our focus is mainly on models that arise in stochastic settings. Our goal in the thesis is to use a formal verification technique called probabilistic model checking to verify and analyze the dynamics of stochastic models.

The main challenge of verifying and analyzing Markov chains that arise in the context of biological pathways is the state space explosion. In many applications a probabilistic graphical model called dynamic Bayesian network (DBN) can be a more natural and succinct model to work with.

Consequently, our work concerns the analysis of DBN models of biopathways from a model checking point of view. Specifically, we first consider the problem of probabilistic model checking on DBNs based on probabilistic inference. However, exact inference is hard for large DBNs. To get around this, in the first part of the thesis, we present a new improved approximate inference method for DBNs called hybrid factored frontier.

We then formulate, for DBNs, a new probabilistic temporal logic called bounded linear time probabilistic logic. We develop an --approximate-- model checking framework based on DBN inference algorithms. We then verify interesting dynamical properties of biological systems.

The second part of the thesis focuses on using another scalable probabilistic model checking approach called statistical model checking for calibration and analysis of ODE based models. The uncertainty concerning the initial states is modeled via a prior distribution over an interval of values. The noisiness and the cell-population-based nature of the experimental data are captured by the confidence level and strength of the statistical test. The experimental data as well as qualitative properties of the pathway are encoded as the specification formula in temporal logic formalism. In this setting, we use optimized versions of statistical model checking algorithms for the task of parameter estimation. Specifically, we build a statistical model checking based parameter estimation framework by coupling it with standard global optimization techniques. Our results suggests that this framework is efficient, useful and scales well.

Finally, we apply our statistical model checking framework to build and calibrate an ODE model for the Toll like receptor (TLR) 3 and TLR7 pathways. We investigate specific crosstalk mechanisms that lead to synergy when the TLR3 and TLR7 receptors are stimulated together in a specific order and a specific time gap. Our analysis leads to interesting insights regarding the potential crosstalk mechanisms.