Difference between revisions of "CSI Seminar 2017-07-04"
From LRDE
Laurent Xu (talk | contribs) (Created page with "<center> <img src="%WWWLRDE%images/lrde_big.png"> </center> %TOC% ---+ %BLUE%CSI Seminar: 4 July 2017, EPITA, 10h, Salle L0 - LRDE, KB %ENDCOLOR% ---++ SPOT ---+++ 10h00...") |
Laurent Xu (talk | contribs) (Blanked the page) |
||
Line 1: | Line 1: | ||
− | <center> <img src="%WWWLRDE%images/lrde_big.png"> </center> |
||
− | |||
− | %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). |