Difference between revisions of "CSI Seminar 2017-07-04"

From LRDE

(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).

Revision as of 14:30, 15 June 2017

<img src="%WWWLRDE%images/lrde_big.png">

%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).
Retrieved from "https://www.lrde.epita.fr/index.php?title=CSI_Seminar_2017-07-04&oldid=118510"