From Model-Checking to Temporal Logic Constraint Solving

13 years 10 months ago
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.
Aurélien Rizk, François Fages
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where CP
Authors Aurélien Rizk, François Fages
Comments (0)