La logique temporelle et le model-checking ont fait leurs preuves pour formaliser des propriétés biologiques de systèmes biochimiques complexes et vérifier automatiquement leur satisfaction sur des modèles quantitatifs ou qualitatifs. Dans cet article, nous allons au delà du model-checking en présentant un algorithme de résolution de contraintes pour les formules de logique temporelle du premier ordre sans quantificateur avec contraintes sur les réels. Cet algorithme calcule le domaine des variables réelles apparaissant dans une formule pour lequel la formule est satisfaite pour un modèle donné. Nous illustrons cette approche pour la génération automatique de spécification en logique temporelle à partir de données biologiques. Nous fournissons un ensemble de motifs de formules biologiquement pertinentes et les appliquons sur des données simulées d'un modèle du cycle cellulaire. Nous montrons sur ces exemples que cette approche permet d'inférer automatiquement, des propriétés semi-qualitatives, semi-quantitatives sur les seuils de concentration, l'amplitude d'oscillations, les propriétés de stabilité, de point de passage et d'influence entre molécules.