Résumé : De nombreuses contraintes restreignant le résultat de certains calculs sur une séquence entière peuvent être représentées de manière compacte par des automates à registres. Nous améliorons la propagation de la conjonction de telles contraintes portant sur une même séquence en synthétisant une base de données d’invariants linéaires et non linéaires à partir de la représentation de ces contraintes en termes d’automates à registres. Les invariants obtenus sont paramétrés par la longueur de la séquence et sont vérifiés pour toute séquence suffisamment longue. Pour évaluer la qualité de ces invariants linéaires, nous avons développé une méthode permettant de vérifier si un invariant linéaire généré est une facette de l’enveloppe convexe des points réalisables. Cette méthode, ainsi que la preuve d’invariants non linéaires, sont basées sur la génération systématique d’automates finis déterministes de taille constante qui acceptent toutes les séquences entières dont le résultat vérifie une condition simple. Nous appliquons cette méthodologie à un ensemble de 44 contraintes de séries temporelles et obtenons 1400 invariants linéaires dont 70% définissent des facettes, et 600 invariants non linéaires, qui ont été testés sur des problèmes de production électrique à court terme.
Bio: Nicolas Beldiceanu est professeur en informatique à IMT Atlantique, LS2N-CNRS à Nantes (France) depuis 2003. Il a auparavant été chercheur senior au SICS à Uppsala (Suède), responsable de la recherche à COSYTEC dans la région parisienne (France), ainsi que chercheur au Centre européen de recherche sur les industries informatiques à Munich (Allemagne). Ses travaux portent sur la programmation par contraintes : contraintes globales et contraintes structurelles de séries chronologiques ; algorithmes de filtrage efficaces décrivant les contraintes (avec métadonnées, graphique, automates, transducteurs) ; synthèse / apprentissage des cartes de connaissances combinatoires ; modèles de contraintes d’apprentissage.
Calendrier des séminaires
