26 Janvier - 1 Février


Retour à la vue des calendrier
Lundi 26 Janvier
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Apprentissage faiblement supervise d'un etiqueteur morpho-syntaxique par transfert cross-lingue
Description: Guillaume Wisniewski Les méthodes de transfert cross-lingue permettent
partiellement de pallier l'absence de corpus annotés, en particulier
dans le cas de langues peu dotées en ressources linguistiques. Le
transfert d'étiquettes morpho-syntaxiques depuis une langue riche en
ressources, complété et corrigé par un dictionnaire associant à
chaque mot un ensemble d'étiquettes autorisées, ne fournit cependant
qu'une information de supervision incomplète. Dans ce travail, nous
reformulons ce problème dans le cadre de l'apprentissage
ambigu et proposons une nouvelle méthode pour apprendre un
analyseur de manière faiblement supervisée à partir d'un modèle à
base d'historique. L'évaluation de cette approche montre une amélioration
sensible des performances par rapport aux méthodes de l'état de
l'art.
Mardi 27 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Soutenance de thèse (AOC-RCLN)
Description: Nada Mimouni
Vendredi 30 Janvier
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Une introduction à la théorie de Squier
Description: Yves Guiraud Un monoïde ayant une présentation par un système de réécriture convergent
fini a un problème du mot décidable. Dans les années 1980, Jantzen
s'interroge sur la réciproque : un monoïde ayant un problème du mot
décidable admet-il toujours une présentation par un système de réécriture
convergent fini ? Squier a répondu négativement à cette question en reliant
des propriétés algorithmiques des systèmes de réécriture, comme la
terminaison et la confluence, à des invariants algébriques, comme
l'homologie ou l'homotopie.

Dans cet exposé, je présenterai le résultat initial de Squier, dans le
formalisme de la réécriture de dimension supérieure. Puis, nous verrons
comment le travail de Squier permet aujourd'hui d'utiliser la réécriture
comme méthode constructive pour calculer des invariants de structures
algébriques.
Heure: 14:00 - 14:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Cost Linear Temporal Logic for Verification
Description: Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties.

We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata.
Heure: 14:40 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Vérification de Spécifications EB-3 à l'aide de Techniques de Model Checking
Description: Dimitrio Vekris EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3 comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cet exposé, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking.

En se basant sur une sémantique opérationnelle de EB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées, on définit une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 tous les outils de vérification fonctionnelle disponible dans CADP.