Abstract

Biochemical systems are characterised by complexity – highly-dimensional state space, non-linear and stochastic dynamics. Different formalisms have been proposed in order to capture the knowledge about the system. Moreover, when a model of a bio-molecular system is written in a formal language, it can be executed and it is amenable to formal verification-type of analysis. We present two research stories of applying techniques from formal verification to modelling biochemical systems. First, we show how to use the principle of static analysis with abstract interpretation in order to automatically reduce highly dimensional, stochastic rule-based models of signalling pathways; The reductions are performed with respect to three kinds of guarantees: (i) soundness, (ii) upped error bound and (iii) limit approximations (ie. quasi-stationary assumption). Second, we use SAT /SMT solvers to, for Wagner’s model of a gene regulatory network and a temporal property of interest, synthesise the parameters for which a given formula holds; Then, quantities such as the mutational robustness of a GRN can be computed more efficiently and more accurately than with the statistical-sampling approach commonly used by evolutionary biologists.