CSI Seminar 2017-07-04
From LRDE
%TOC%
---+ %BLUE%CSI Seminar: 4 July 2017, EPITA, 10h, Salle L0 - LRDE, KB %ENDCOLOR%
---++ SPOT
---+++ 10h00 : Un ensemble d'outils de conversion en automate de co-Büchi -- [[%MAINWEB%.AlexandreGbaguidiAisse][Alexandre Gbaguidi A¨isse]]
Grâce au format HOA, il y a de moins en moins de barrières entre des -automates avec différentes conditions d'acceptation. Spot, une bibliothèque manipulant les -automates supporte des conditions d'acceptations arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversions capables de convertir (quand c'est possible) n'importe quelle condition d'acceptation classique vers du co-Büchi déterministe. Boker and Kupferman ont mis au point des méthodes asymptotiquement optimales réalisant ces conversions. Nous avons implémenté leurs méthodes avec quelques optimisations et adaptations: nous supportons les conditions d'acceptations dites "Streett-like", celles écrites sous forme normale disjonctive (y compris celles dites "Rabin-like") ainsi que les acceptations basées sur les transitions ("transition-based"). Ces algorithmes peuvent être utilisés pour vérifier si une formule LTL est de la famille "persistence".
---+++ 10h30 : Test de vacuité bi-bande dans Spot -- [[%MAINWEB%.ClementGillard][Clément Gillard]]
Spot est une bibliothèque qui manipule des -automates dont les conditions d'acceptation sont exprimées avec au plus 32 ensembles d'acceptation. Puisque la condition d'acceptation du produit de deux automates doit utiliser la somme de leurs ensembles, on ne peut pas construire des produits dont les opérandes utilisent plus de 32 ensembles au total. Une opération typique sur les automates est de calculer
pour décider si intersecte .
Lorsqu'elle est implémentée par , le calcul du produit limite le nombre d'ensembles d'acceptation que A et B peuvent utiliser. On propose une nouvelle fonction qui réalise le test de vacuité de sans construire un automate et donc sans limite sur les conditions d'acceptation. L'outil ltlcross peut maintenant comparer des automates pour un total supérieur à 32 ensembles d'acceptation.
---+++ 11h00 : Réduction par simulation à pas -- [[%MAINWEB%.LaurentXU][Laurent XU]]
En vérification formelle à l'aide d'-automates, la construction d'automates plus petits réduit beaucoup le temps d'exécution et la consommation mémoire d'opérations coûteuses telles que le produit synchronisé. La minimisation d'-automates étant un problème NP-complet, nous concentrons notre travail sur les opérations de réduction. Spot possède déjà une méthode de réduction par simulation fonctionnant pour toutes conditions d'acceptation. Cette méthode utilise une simulation à un pas reposant sur la signature des états. L. Clemente et R. Mayr ont proposé une méthode de réduction par simulation à pas ne fonctionnant que pour les automates de Büchi et ils ont montré que l'augmentation de ce nombre de pas peut améliorer la réduction. Nous étudions une généralisation de l'opération de réduction existante dans Spot pour qu'elle fonctionne avec des simulations à pas reposant sur la signature des états.
---+++ 11h30 : Réduction d'ordre partiel dans SPOT -- [[%MAINWEB%.VincentTourneur][Vincent Tourneur]]
Les outils de vérification formelle souffrent actuellement d'un problième de passage à l'échelle, à cause de leur consommation de mémoire. La réduction d'ordre partiel est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Il en existe beaucoup d'algorithmes à l'état de l'art, et cette technique est utilisée dans plusieurs logiciels (comme SPIN ou LTSmin). Nous allons parler ici de l'implémentation de certains de ces algorithmes dans la bibliothèque Spot, puis de leur optimisation. Les résultats obtenus montrent une diminution notable de la consommation de mémoire, ce qui implique un gain pour toutes les étapes suivantes de la vérification.
---+++ 13h30 : Intégration de TChecker dans Spot -- [[%MAINWEB%.ArthurRemaud][Arthur Remaud]]
Un automate temporisé est un -automate représentant un modèle comportant des conditions de temps continu, ce qui peut aboutir à un espace d'états infini. Cependant, il est possible de le ramener à un automate fini, appelé graphe de zones, afin d'étudier ses propriétés. Dans ce rapport, nous montrons comment les automates temporisés sont intégrés à Spot.
Nous utilisons TChecker, qui est un programme conçu au LaBRI. Nous expliquons comment sont intégrés les représentations des graphes de zones qu'utilise TChecker pour travailler sur les automates temporisés dans Spot. Nous montrons ensuite comment les algorithmes de Spot lisent cette adaptation pour travailler sur des automates temporisés et des graphes de zones. Nous montrons enfin comment sont contournés certains inconvénients de TChecker afin de rendre plus simple son utilisation par Spot.
---+++ 14h00 : Synthèse LTL avec Spot -- [[%MAINWEB%.ThibaudMichaud][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é en exploitant la bibliothèque Spot pour manipuler efficacement les -automates. Deux méthodes ont été implémentées pour la résolution du jeu: l'algorithme récemment découvert par Calude et al., qui a la meilleure compléxité théorique connue pour ce problème, et l'algorithme récursif de Zielonka, connu pour ses bonnes performances pratique. Finalement, la stratégie gagnante est traduite en un circuit Et-Inverseur qui modélise la formule LTL d'origine.
---++ OLENA
---+++ 14h45 : L'Arbre de partition binaire pour le traitement d'images -- [[%MAINWEB%.FabienHOUANG][Fabien HOUANG]]
L'arbre binaire de partition est une structure qui permet un traitement d'images, une segmentation et une recherche d'informations efficaces dans une image. C'est une structure hiérarchique qui permet de simplifier les opérations et la reconnaissance sur une image. Il peut utiliser différents models région et fonctions de calcul de distance pour se créer. La construction de cet arbre se fait habituellement à partir d'une image pré-segmentée pour des questions de performances et de gain de temps. Tous ces paramètres peuvent varier et changer la représentation de l'image par le BPT. La résistance de l'arbre au bruit peut aussi être étudiée, par exemple trouver quel niveau de l'arbre sera influencé par le bruit.
---+++ 15h15 : Calcul du Complexe de Morse-Smale à l'aide de coupe de ligne de partage des eaux -- [[%MAINWEB%.VictorCollette][Victor Collette]]
Le complexe de Morse-Smale est un outil utile pour analyser la topologie d’une image. Cependant, son calcul est onéreux et il existe plusieurs algorithmes qui possdent des différences dans la définition du complexe. D’un autre côté, l’algorithme de coupe de ligne de partage des eaux est un algorithme morphologique qui découpe des images en niveaux de gris. Il interprète les images comme des graphes valués sur les arrêtes, les poids étant donnés par le gradient de l’image. Lidija Comic était la première à mettre en avant une possible équivalence entre l’algorithme de calcul du Morse-Smale et l’algorithme de ligne de partage des eaux, avec des marqueurs spécifiques sur les maxima et les minima de l’image. Dans ce document, nous parlons de cette possibilité et nous proposons une implémentation d’une version modifiée de l’algorithme de coupe de ligne de partage des eaux, qui fonctionne sur un graphe valué sur les sommets pour calculer le complexe de Morse-Smale.
---+++ 15h45 : Méthode d'évaluation d'évaluateur d'algorithme de détection de texte -- [[%MAINWEB%.AlionaDangla][Aliona Dangla]]
Plusieurs méthodes d'évaluations des algorithmes de détection de texte existent. Cependant, elles donnent des résultats différents, il est donc difficile d'estimer la pertinence de celles-ci. 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 obtenir cette référence, un site internet à été réalisé de façon à ce qu'un grand nombre d'utilisateurs puissent classer de façon simple les résultats d'un grand nombre d'algorithmes de détection de texte sur des grandes bases d'images. L'interface utilisateur a été développée pour minimiser le nombre de comparaison que l'utilisateur doit réaliser afin d'obtenir un classement cohérent. Nous l'appliquerons sur les résultats du concours ICDAR 2013 (8 méthodes sur un lot de 233 images).