Evènement pour le groupe Modélisation et Verification


Date 2007-04-05  11:00-12:15
TitreDécidabilité et contrôle de logiques temps-réel 
RésuméLa logique temporelle MTL (Metric Temporal Logic) est une extension de LTL avec des contraintes quantitatives : elle permet par exemple d'exprimer qu'un événement se produira dans moins de 5 unités de temps. MTL a longtemps été supposée indécidable; ce n'est que récemment que Ouaknine et Worrel ont montré que la décidabilité de MTL dépend en fait de la sémantique considérée ("pointwise" ou "interval-based"). Nous revisiterons les résultats d'indécidabilité de MTL et étudierons la synthèse de contrôleur pour des spécifications MTL.  
Lieusalle 076, LaBRI, rez-de-chaussée 
OrateurFabrice Chevalier 
Emailfabrice.chevalier@lsv.ens-cachan.fr 
UrlLSV, Cachan, France 



Aucun document lié à cet événement.

Retour
Retour à l'index