Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mardi 4 juillet 2017 à partir de 10h00 en L0 au LRDE (KB). -------------------------------------------- Au programme : SPOT — BIBLIOTHÈQUE DE MODEL CHECKING 10h00 : Un ensemble d’outils de conversion en automate de co-Büchi – ALEXANDRE GBAGUIDI AÏSSE Spot supporte des conditions d’acceptation arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversion capables de convertir (quand c’est possible) n’importe quel automate avec une condition d’acceptation classique vers du co-Büchi déterministe. Nous présenterons ces algorithmes mis au point par Boker et Kupferman en explicitant les améliorations apportées durant leur implémentation. 10h30 : Test de vacuité bi-bande dans Spot – CLÉMENT GILLARD Lorsqu’on fait de la vérification de modèle à l’aide d’ω- automates, une opération typique est le calcul de L(AxB) ≠ Ø. Son implémentation par empty(product(A,B)) pose problème, car le produit utilise autant d’ensembles d’acception qu’il y en a dans A et dans B et ce nombre d’ensembles ne peut excéder 32 dans Spot. On propose empty(A,B) qui ne construit pas d’automate et retire cette contrainte sur les automates en entrée. 11h00 : Réduction par simulation à n pas – LAURENT XU En vérification formelle à l’aide d’ω-automates, il est utile de réduire la taille des automates. L. Clemente et R. Mayr présentent une méthode de réduction par simulation à n pas ne fonctionnant que pour les automates de Büchi et montrent que l’augmentation de ce nombre de pas améliore la réduction. Nous étudions une généralisation de la réduction d’ω- automates par simulation reposant sur la signature des états à un pas de Spot afin qu’elle fonctionne également à n pas. 11h30 : Réduction d’ordre partiel dans SPOT – VINCENT TOURNEUR Les outils de vérification formelle souffrent actuellement d’un problème de passage à l’échelle. La réduction d’ordre partiel (POR) est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Nous allons parler de l’implémentation de certains de ces algorithmes de POR dans la bibliothèque Spot, puis de leur optimisation. 13h30 : Intégration de TChecker dans Spot – ARTHUR REMAUD Les automates temporisés sont un type d'ω-automate représentant des modèles comportant des conditions de temps continu. Spot ne gère actuellement pas ce type d’automates. TChecker est un outil développé par le LaBRI travaillant sur des automates temporisés. Plutôt que réimplémenter tous les algorithmes, TChecker a été intégré dans Spot via un nouvel exécutable. 14h00 : Synthèse LTL avec Spot – THIBAUD MICHAUD Nous présentons un nouvel outil de synthèse de circuit à partir de spécifications LTL. Il réduit le problème de synthèse à un jeu à parité, qui est résolu grâce à l’un des deux algorithmes implémentés. Finalement, la stratégie gagnante est traduite en un circuit Et-Inverseur qui modélise la formule LTL d’origine. OLENA — TRAITEMENT D’IMAGES GÉNÉ- RIQUE ET PERFORMANT 14h45 : L’Arbre de partition binaire pour le traitement d’images – FABIEN HOUANG L’arbre de partition binaire est, en traitement d’images, une structure qui permet la segmentation et la recherche efficace d’information dans une image. Il peut être créé à partir de différents modèles de région et fonctions de calcul de distance entre ces régions. La construction de cet arbre se fait habituellement à partir d’une image pré-segmentée pour des questions de performance. La sensibilité de l’arbre au bruit dans l’image peut aussi être étudiée, pour trouver par exemple quels niveaux de l’arbre sont influencés par ce dernier. 15h15 : Calcul du Complexe de Morse- Smale à l’aide de coupe de ligne de partage des eaux – VICTOR COLLETTE Le complexe de Morse-Smale est un outil utile pour analyser la topologie d’une image. Son calcul étant onéreux avec un algorithme classique, L. Comic a émis l’hypothèse que son calcul pouvait être réalisé à l’aide d’un algorithme de coupe de ligne de partage des eaux. Nous parlerons donc de cette possibilité et des différents problèmes que cette solution engendre. 15h45 : Méthode d’évaluation d’évaluateur d’algorithme de détection de texte – ALIONA DANGLA Plusieurs méthodes d’évaluations des algorithmes de détection de texte existent. Cependant, elles donnent des résultats différents. Afin d’évaluer ces méthodes, la solution proposée est de confronter les évaluations automatiques avec l’évaluation humaine en considérant celle-ci comme référence. Pour l’obtenir, un site internet à été réalisé afin d’obtenir un classement cohérent. -- Daniela Becker Responsable administrative du LRDE