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

From LRDE

(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...")
 
(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 21:25, 14 June 2017