Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures

Finding mathematical models satisfying a specification built from the formalization of biological experiments, is a common task of the modeler that techniques like model-checking help solving, in the qualitative but also in the quantitative case. In this article we define a continuous degree of satisfaction of temporal logic formulae with constraints. We show how such a satisfaction measure can be used as a fitness function with state-of-the-art evolutionary optimization 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 temporal specification. These methods are evaluated on models of the cell cycle and of the MAPK signaling cascade. (C) 2010 Elsevier B.V. All rights reserved.