From Model-Checking to Temporal Logic Constraint Solving

Abstract. In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain D, and by computing a validity domain for the variables rather than a truth value for the formula. This allows us to define a continuous degree of satisfaction for a temporal logic formula in a given structure, opening up the field of model-checking to optimization. We illustrate this approach with reverseengineering problems coming from systems biology, and provide some performance figures on parameter optimization problems with respect to temporal logic specifications.

• Type: Conference
• Year: 2009
• Where: CP
• Authors: Aurélien Rizk, François Fages
• Keywords: CP 2009, Programming Languages, Temporal Logic Constraint, Temporal Logic Formula, Temporal Logic Formulae