Abstract

Finding mathematical models satisfying a specification built from the formalization of biological experiments is a common task of the modeler. We show that the formalization of biological temporal properties of systems, as observed in experiments, in temporal logics specifications enable the transposition of programming concepts and tools, like model-checking, to the analysis of living processes at the cellular level. Also as temporal logics allow one to express both qualitative (e.g. some protein is eventually produced) and quantitative (e.g. a concentration exceeds 10) information they are well suited to the increasingly quantitative, yet incomplete, uncertain and imprecise information now accumulated in the field of quantitative systems biology. We define a continuous degree of satisfaction of temporal logic formula and show how it can be used as a fitness function for continuous optimization methods to provide a parameter search procedure for biochemical reaction networks with respect to temporal specifications. Then we describe how we can use such a satisfaction measure for the robustness analysis of biological models. Finally we apply these methods for the analysis of a cell cycle model, on a coupled model of the cell cycle and the circadian clock to search for optimal injections schedule of anticancer drugs, and on a synthetic biology system to find kinetic parameter values that make a given temporal specification robust in a population of cells despite variability.