On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology

Finding mathematical models satisfying a specification built from the formalization of biological experiments, is a common task of the modeller that techniques like model-checking help solving, in the qualitative but also in the quantitative case. In this article we propose to go one step further by defining a continuous degree of satisfaction of a temporal logic formula with constraints. We show how such a satisfaction measure can be used as a fitness function with state-of-the-art search methods in order to find biochemical kinetic parameter values satisfying a set of biological properties formalized in temporal logic. We also show how it can be used to define a measure of robustness of a biological model with respect to some specification. These methods are evaluated on models of the cell cycle and of the MAPK signalling cascade.