Deduction automatique pour le calcul des durees basee sur la methode des tableaux

Mardi 11 decembre 2001 a 14 heures

Salle des theses de l'Irit

Resume : Dans le cadre de la modelisation des systemes reactifs, des logiques temporelles ont ete developpees au cours des annees 1980. Ces logiques permettent d'exprimer des contraintes qualitatives entre les evenements mais ne permettent pas d'exprimer des contraintes quantitatives. La necessite de pouvoir exprimer de telles informations a amene a developper des logiques dites temps-reel, generalement des extensions de logiques temporelles existantes, a partir de la seconde moitie des annees 1980. C'est parmi ces logiques que se situe le calcul des durees dont la particularite est de permettre d'exprimer la duree pendant laquelle un systeme se trouve dans un etat donne, au cours d'un intervalle de temps. Plusieurs types de problemes peuvent etre etudies, telles la verification de modele qui consiste a verifier si un modele donne satisfait une formule donnee et la satisfaisabilite qui consiste a chercher si une formule donnee est satisfaite dans au moins un modele. Nous nous sommes interessee au probleme de la satisfaisabilite. Nous avons etudie deux fragments du calcul des durees pour lesquels nous avons developpe une methode de decision basee sur la methode des tableaux.

Retour a la page des seminaires