After 9 years of releases with a leading "0." in their version number,
this might be unexpected:
We are pleased to announce the release of Spot 1.0.
Spot is a model-checking library developed collaboratively by LRDE
and LIP6. It provides algorithms and data structures to implement
the automata-theoretic approach to LTL model checking.
This major new releases features a set of completely rewritten
command-line tools, an implementation of reverse simulation,
and support for testing automata.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.0.tar.gz
A more detailed listing of the changes follows.
New in spot 1.0 (2012-10-27):
* License change: Spot is now distributed using GPL v3+ instead
of GPL v2+. This is because we started using some third-party
files distributed under GPL v3+.
* Command-line tools
Useful command-line tools are now installed in addition to the
library. Some of these tools were originally written for our test
suite and had evolved organically into useful programs with crappy
interfaces: they have now been rewritten with better argument
parsing, saner defaults, and they come with man pages.
- genltl: Generate LTL formulas from scalable patterns.
This offers 20 patterns so far.
- randltl: Generate random LTL/PSL formulas.
- ltlfilt: Filter lists of formulas according to several criteria
(e.g., match only safety formulas that are larger than
some given size). Besides being used as a "grep" tool
for formulas, this can also be used to convert
files of formulas between different syntaxes, apply
some simplifications, check whether to formulas are
equivalent, ...
- ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA,
BA, or Monitor). A fundamental change to the
interface is that you may now specify the goal of the
translation: do you you favor deterministic or smaller
automata?
- ltl2tgta: Translate LTL/PSL formulas into Testing Automata.
- ltlcross: Compare the output of translators from LTL/PSL to
Büchi automata, to find bug or for benchmarking. This
is essentially a Spot-based reimplementation of LBTT
that supports PSL in addition to LTL, and that can
output more statistics.
An introduction to these tools can be found on-line at
http://spot.lip6.fr/userdoc/tools.html
The former test versions of genltl and randltl have been removed
from the source tree. The old version of ltl2tgba with its
gazillion options is still is src/tgbatest/ and is meant to be
used for testing only. Although ltlcross is meant to replace
LBTT, we are still using both tools in this release; however this
is likely to be the last release of Spot that redistributes LBTT.
* New features in the Spot library:
- Support for various flavors of Testing Automata.
The flavors are:
+ "classical" Testing Automata, as used for instance by
Geldenhuys and Hansen (Spin'06), using Büchi and
livelock acceptance conditions.
+ Generalized Testing Automata, extending the previous
with multiple Büchi acceptance sets.
+ Transition-based Generalized Testing Automata moving Büchi
acceptance to transitions, and getting rid of livelock
acceptance conditions by expliciting stuttering self-loops.
Supporting algorithms include anything required to run
the automata-theoretic approach using testing automata:
+ dedicated synchronized product
+ dedicated emptiness-check for TA and GTA, as these
may require two passes because of the two kinds of
acceptance, while a TGTA can be checked for emptiness
with the same one-pass algorithm as a TGBA.
+ conversion from a TGBA to any of the above kind, with
options to reduce these automata with bisimulation,
and to produce a BA/GBA that require a single pass
(at the expense of determinism).
+ output in dot format for display
A discussion of these automata, part of Ala Eddine BEN SALEM's
PhD work, should appear in ToPNoC VI (LNCS 7400). The web-based
interface and the aforementioned ltl2tgta tool can be used
to build testing automata.
- TGBA can now be reduced by Reverse Simulation (in addition to
the Direct Simulation introduced in 0.9). A function called
iterated_simulations() will alternate direct and reverse
simulations in a loop as long as it diminishes the size of the
automaton.
- The enumerate_cycles class implements the Loizou-Thanisch
algorithm to enumerate elementary cycles in a SCC. As an
example of use, is_weak_scc() will tell whether an SCC is
inherently weak (all its cycles are accepting, or none of them
are).
- parse_lbt() will parse an LTL formula expressed in the prefix
syntax used (at least) by LBT, LBTT and Scheck.
to_lbt_string() can be used to print an LTL formula using this
syntax.
- to_wring_string() can be used to print an LTL formula into
Wring's syntax.
- The LTL/PSL parser now has a lenient mode that can be useful
to interpret atomic proposition with language-specific constructs.
In lenient mode, any (...) or {...} block that cannot be parsed
as formula will be assumed to be an atomic proposition.
For instance the input (a < b) U (process[2]@ok), normally
flagged as a syntax error, is read as "a < b" U "process[2]@ok"
in lenient mode.
- minimize_obligation() has a new option to disable WDBA
minimization it cases it would produce a deterministic automaton
that is bigger than the original TGBA. This can help
choosing between less states or more determinism.
- new functions is_deterministic() and count_nondet_states()
(The count of nondeterministic states is now displayed on
automata generated with the web interface.)
- A new class, "postprocessor", makes it easier to apply
all available simplification algorithms on a TGBA/BA/Monitors.
* Minor changes:
- The '*' operator can (again) be used as an AND in LTL formulas.
This is for compatibility with formula written in Wring's
syntax. However inside SERE it is interpreted as the Kleen
star.
- When printing a formula using Spin's LTL syntax, we don't
double-quote complex atomic propositions (that was not valid
Spin input anyway). For instance F"foo == 2" used to be
output as <>"foo == 2". We now output <>(foo == 2) instead.
The latter syntax is understood by Spin 6. It can be read
back by Spot in lenient mode (see above).
- The gspn-ssp benchmark has been removed.
Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 17 octobre 2012 (10h00-12h00), Salle Alpha du LRDE.
Au programme:
* 10h: Systèmes d'exploitation en dur: une clef du passage de 10 à 1000 cœurs
-- Raphael Poss - University of Amsterdam
http://staff.science.uva.nl/~poss
Afin d'exploiter le potentiel des puces multi-cœurs pour une performance
évolutive et à haut rendement énergétique, le projet Apple-CORE a
co-conçu un modèle général d'architecture matérielle et une interface de
contrôle de parallélisme. Cette interface, appelée SVP, est réalisée par
du matériel sur puce dédié à la gestion de la concurrence de programmes
parallèles exécutés sur plusieurs cœurs. SVP se base sur les principes
de synchronisation de flux de données («data flow»), de programmation
impérative et d'exécution efficace du parallélisme en termes de budget
temps et énergie. Les composants matériels correspondants peuvent
coordonner plusieurs cœurs RISC équipés de multi-threading matériel,
organisés en clusters de calcul sur puce, dits «Microgrids».
Comparés à l'approche traditionnelle «accélérateurs», les Microgrids
sont destinés à être utilisés comme composants dans les systèmes
distribués sur puce contenant à la fois des grappes de petits cœurs et
optionnellement de gros cœurs –optimisés pour l'exécution séquentielle–
disponibles en tant que «services» pour les applications. Les principaux
aspects de cette architecture sont l'asynchronisme, c'est-à-dire la
capacité à tolérer les opérations irrégulières avec des temps de latence
longs, un modèle de programmation à échelle invariante, une vision
distribuée de la puce, et une mise à l'échelle transparente de la
performance d'un seul code binaire à plusieurs tailles de grappes de
cœurs.
Cette présentation décrit le modèle d'exécution, la micro-architecture
des cœurs, sa réalisation au sein d'une plateforme et son environnement
logiciel.
-- Diplômé CSI en 2003, Raphael est resté actif à l'EPITA jusqu'en 2004,
puis a travaillé en tant qu'ingénieur logiciel à Paris puis Rotterdam.
Il rejoint en 2008 le groupe Computer Systems Architecture à
l'Université d'Amsterdam en tant que chef de projet et
enseignant-chercheur, où il reçoit un doctorat en septembre 2012. Il
donne des cours d'architecture matérielle à Amsterdam et Leiden, et
continue de coordonner des activités de recherche au croisement entre
architecture, compilateurs et systèmes d'exploitation.
* 10h45: Platform and Research overview on the Intel Single-chip Cloud Computer
-- Roy Bakker - University of Amsterdam
http://www.science.uva.nl/~bakkerr
The Single-chip Cloud Computer (SCC) is a 48-core experimental processor
created by Intel Labs targeting the many-core research community. The
6x4 mesh Network-on-Chip provides 24 tiles with 2 cores each. All cores
are independent and run their own instance of an operating system. It
has hardware support (local buffers on the tiles) for sending short
messages between cores, and allows for voltage and frequency control at
8 and 2 cores respectively.
We have already modified the SVP runtime system to use these on-chip
buffers for the communication between threads executed on separate
cores. We also created a visual application for manual process migration
and scheduling on the SCC as well as a library for customized voltage
and frequency scaling on the chip.
Currently we focus on automated parallelization and mapping of one or
multiple sequential programs onto the 48 cores by modifying the daedalus
framework to target the SCC. The daedalus framework parallelizes
sequential C programs using Kahn Process Networks (KPNs) and generates
code to run the KPN on multiple hardware platforms like for example an
FPGA, SMP CPU or GPU. The SCC backend, which is work in progress, should
result in a tool that utilizes the SCC cores in an optimal way by means
of performance and energy consumption. It should also allow the system
to dynamically adapt on changes in the computational or communicational
needs of the processes by scaling frequency and migrating processes.
-- Roy Bakker is a PhD student in the Computer Systems Architecture group
at the University of Amsterdam, where he also graduated for his
Bachelor's (2008) and Master's (2011) degree. His current work is funded
by the Netherlands Organisation for Scientific Research (NWO) project on
Smart Energy Systems (SES).
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://www.lrde.epita.fr/mailman/listinfo/seminaire
Bonjour,
nous avons le plaisir de vous annoncer la sortie du n°26 du bulletin du LRDE.
C'est un numéro Spécial Rentrée qui présente l'ensemble des membres du LRDE.
Vous y trouverez également un aperçu des activités du LRDE et de la majeure CSI
dont font partie tous les élèves épitéens intégrant le labo.
Vous pouvez télécharger le bulletin en couleur à la page suivante :
http://publis.lrde.epita.fr/201209-l-air-de-rien-26
--
Daniela Becker
Responsable administrative du LRDE
We are happy to announce that the following paper has been
published in the Proceedings of the Workshop on Applications of
Discrete Geometry and Mathematical Morphology (Springer LNCS
volume 7346). This paper is an extended version of the initial
WADGMM 2010 paper.
Nous avons le plaisir de vous annoncer que l'article suivant a
été publié dans les actes du Workshop on Applications of Discrete
Geometry and Mathematical Morphology (Springer LNCS volume 7346).
Cet article est une version étendue de l'article originel de
WADGMM 2010.
Roland Levillain (1,2), Thierry Géraud (1,2) and Laurent Najman (2)
Writing Reusable Digital Topology Algorithms in a Generic Image
Processing Framework
http://publis.lrde.epita.fr/201206-WADGMM-LNCS
(1) EPITA Research and Development Laboratory (LRDE)
(2) Université Paris-Est, Laboratoire d'Informatique Gaspard-Monge,
Equipe A3SI, ESIEE Paris
Digital Topology software should reflect the generality of the
underlying mathematics: mapping the latter to the former requires
genericity. By designing generic solutions, one can effectively
reuse digital topology data structures and algorithms. We
propose an image processing framework focused on the Generic
Programming paradigm in which an algorithm on the paper can be
turned into a single code, written once and usable with various
input types. This approach enables users to design and implement
new methods at a lower cost, try cross-domain experiments and
help generalize results.
--
Roland Levillain
EPITA Research and Development Laboratory (LRDE)
14-16, rue Voltaire - FR-94276 Le Kremlin-Bicêtre Cedex - France
Phone: +33 1 53 14 59 45 - Fax: +33 1 53 14 59 22 - www.lrde.epita.fr
Chers collègues,
L'édition 2011-2012 du séminaire de recherche du LRDE, consacré
au thème cher à notre laboratoire – Performances et Généricité –
vient de s'achever.
Cette année encore nous avons eu le plaisir d'accueillir des
orateurs de qualité, renommés dans leur domaine. Vous trouverez
ci-dessous une liste thématique des différents exposés. Les
hyperliens vous conduirons non seulement à leur résumé détaillé,
mais également aux planches des exposés, et aux vidéos pour certaines
séances.
Nous remercions chaleureusement les orateurs qui nous ont
honorés de leur présence. Merci également aux visiteurs !
Nous prenons d'ores et déjà rendez-vous pour une reprise à la
rentrée prochaine. N'hésitez pas à nous proposer un exposé,
ou à nous indiquer des orateurs potentiels.
Bonnes vacances à tous,
Akim, pour le Laboratoire de R&D de l'EPITA
* Langages, paradigmes de programmation
=======================================
* GPU Computing : début d'une ère ou fin d'une époque ?
Eric Mahé -- Responsable du projet OpenGPU
http://seminaire.lrde.epita.fr/2012-06-20.php
* Reusable Generic Look Ahead Multithreaded Cache:
A case study for a high resolution player
Guillaume Chatelet -- Ingénieur R&D à Mikros Image
http://seminaire.lrde.epita.fr/2012-03-14.php
* Des performances dans les nuages avec la virtualisation des langages
Yann Régis-Gianas -- Maître de conférence à l'université Paris Diderot
http://seminaire.lrde.epita.fr/2012-02-15.php
* Certification d'annotations de coût dans les compilateurs
Nicolas Ayache -- Post-doc au laboratoire PPS de l'université Paris Diderot
http://seminaire.lrde.epita.fr/2012-02-15.php
* Pourquoi Javascript est-il aussi rapide/lent ?
Nicolas Pierron -- Ingénieur R&D, Mozilla Paris
http://seminaire.lrde.epita.fr/2011-10-26.php
* Traitement d'image
====================
* Un modèle générique de traitement et de représentation des images
Antoine Manzanera -- Enseignant-Chercheur à l'ENSTA-ParisTech
http://seminaire.lrde.epita.fr/2012-05-09.php
* Analyse des mouvements apparents dans un flux vidéo
Matthieu Garrigues -- Ingénieur Recherche à l'ENSTA-ParisTech
http://seminaire.lrde.epita.fr/2012-05-09.php
* Filtrage morphologique dans les espaces de formes :
Applications avec la représentation d'image par arbres
Yongchao Xu -- Doctorant LRDE/ESIEE
http://seminaire.lrde.epita.fr/2012-07-04.php
* Le point de vue d'un théoricien sur l'intérêt de la généricité
pour le traitement d'images
Laurent Najman -- Professeur à l'ESIEE
http://seminaire.lrde.epita.fr/2012-03-21.php
* Interactive 2D and 3D Segmentation with ilastik
Ullrich Köthe -- Senior Researcher, University of Heidelberg
http://seminaire.lrde.epita.fr/2012-11-16.php
* Model checking
================
* Vérification efficace de propriétés insensibles au bégaiement
Ala Eddine Ben Salem -- Doctorant LRDE/LIP6
http://seminaire.lrde.epita.fr/2012-07-04.php
* Composition dynamique de techniques pour le model checking efficace
Étienne Renault -- Doctorant LRDE/LIP6
http://seminaire.lrde.epita.fr/2012-07-04.php
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://www.lrde.epita.fr/mailman/listinfo/seminaire
The Vaucanson team is pleased to announce the release of Vaucanson 1.4.1,
just in time for the fireworks.
Vaucanson is a platform for manipulating weighted finite state
automata. It includes a C++ generic library and a command-line
interface (TAF-Kit).
http://www.lrde.epita.fr/cgi-bin/twiki/view/Vaucanson/Vaucanson141
Vaucanson 1.4.1 is a maintenance release that fixes a handful of bugs,
and introduce a few simple new features.
- New TAF-Kit commands:
+ ``coquotient``
+ ``alphabet``
+ ``partial-erase``
+ ``gui``
- Bug fixes:
+ never create 0-labeled transitions in ``proper``.
+ fix support of transitions that are linear combinations of pairs
in FMP transducers
- A new TAF-Kit option ``--list-all-commands-json`` outputs the list of
all command in a format (json) that may be parsed by third-party
tools to interface with TAF-Kit.
You can find the new release here:
http://www.lrde.epita.fr/dload/vaucanson/1.4/vaucanson-1.4.1.tar.gz (63MB)
http://www.lrde.epita.fr/dload/vaucanson/1.4/vaucanson-1.4.1.tar.bz2 (54MB)
MD5:
fb904d35e2d0ba70977289e6fb4f39f9 vaucanson-1.4.1.tar.gz
aafb84b15bb90a2fdbdeed96dedc1c94 vaucanson-1.4.1.tar.xz
Please send bug reports to <vaucanson-bugs(a)lrde.epita.fr> and other
inquiries to <vaucanson(a)lrde.epita.fr>.
--
Alexandre Duret-Lutz
Bonjour,
nous avons le plaisir de vous inviter au séminaire des étudiants du
LRDE. Il aura lieu le mercredi 11 juillet 2012 à partir de 9h30 en Amphi
3 (KB).
-----------------------------------------------------------------------
Au programme :
*SPOT, VERIFICATION DU LOCUTEUR, CLIMB, VAUCANSON, OLENA*
http://publis.lrde.epita.fr/Seminar-2012-07-11
SPOT
* 9h30 : Méthodes de réduction par ordre partiel dans Spot -- Pierre Parutto
* 10h00 : Réduction par simulation directe pour les TGBA -- Thomas Badie
VERIFICATION DU LOCUTEUR
* 10h30 : Séparation de locuteur -- Victor Lenoir
11h - 11h15 : PAUSE
* 11h15 : Modèles de mélanges de gaussiennes fondés sur des matrices de
covariance pleines -- Benjamin Roux
CLIMB
* 11h45 : Optimisation en Common Lisp et son application à Climb --
François Ripault
* 12h15 : Construction d’une interface pour et avec Climb -- Laurent Senta
* 12h45 - 14h00 : PAUSE DEJEUNER
VAUCANSON
* 14h00 : Vers Vaucanson 2.0 -- David Moreira
OLENA
* 14h30 : Approche parallèle pour le calcul de l'arbre des formes en
n-dimensions -- Sébastien Crozet
* 15h00 : Extraction de texte avec des ondelettes -- Raphael Boissel
* 15h30 - 15h45 : PAUSE
* 15h45 : Améliorer Horn-Schunck -- Sylvain Lobry
* 16h15 : Inpainting rapide préservant la structure -- Coddy Levi
Les Résumés des exposés :
**************************
SPOT
* 9h30 : Méthodes de réduction par ordre partiel dans Spot -- Pierre Parutto
Spot est une bibliothèque de model checking implémentant
une approche par automates. Pour le moment les algorithmes
de vérification de propriétés dans Spot utilisent l’espace d’états
sans réduction du système. Ils souffrent donc de l’explosion
combinatoire de la taille de ce dernier. Une manière de résoudre
ce problème est d’utiliser des méthodes de réduction
par ordre partiel. Ces méthodes permettent d’ignorer certains
comportements équivalents du système pour une certaine propriété.
Ainsi il est possible de réduire la taille de l’espace
d’états généré tout en conservant le même comportement général.
Le but de ce travail est d’évaluer comment ces méthodes
d’ordre partiel peuvent être intégrées dans Spot.
* 10h00 : Réduction par simulation directe pour les TGBA -- Thomas Badie
L’approche par automates du model checking s’appuie traditionnellement
sur des Automates de Büchi (BA) qu’on souhaite
les plus petits possible. Etessami et al. ont présenté une méthode
de réduction d’un BA basée sur une relation de simulation
(dite directe) entre ses états. Spot, bibliothèque de model
checking, utilise principalement des TGBA qui généralisent les
BA. Nous montrons qu’en adaptant cette simulation aux TGBA
on obtient des automates plus concis que les BA équivalents.
Cette nouvelle technique est incluse dans Spot 0.9 et a permis
de produire des automates plus petits que dans les précédentes
versions.
VERIFICATION DU LOCUTEUR
* 10h30 : Séparation de locuteur -- Victor Lenoir
La séparation de locuteur et la détection de voix jouent un important
rôle dans les systèmes de reconnaissance du locuteur,
principalement dans le cas d’un signal à plusieurs locuteurs.
Nous allons présenter une méthode de séparation de locuteur
basée sur des méthodes variationnelles et sur les speaker factors
tel que décrite dans l’état de l’art de systèmes de reconnaissance
du locuteur. Afin de tester les performances de cette
méthode un ensemble de tests sera effectué sur les données interview
de NIST-SRE 2010.
11h - 11h15 : PAUSE
* 11h15 : Modèles de mélanges de gaussiennes fondés sur des matrices de
covariance pleines -- Benjamin Roux
Le modèle du monde représenté par les mélanges de gaussiennes
(UBM - GMM) est l’approche état de l’art pour les systèmes
de vérification du locuteur. On utilise généralement des
matrices de covariance diagonale. Cette simplification permet
d’avoir un apprentissage rapide des différents modèles. Nous
allons explorer le cas des matrices de covariance pleines. On
va présenter la complexité additionelle et les gains en termes
de performances. Toutes les expériences seront menées sur des
données issues de NIST-SRE 2010.
CLIMB
* 11h45 : Optimisation en Common Lisp et son application à Climb --
François Ripault
Common Lisp est un langage de programmation dynamique.
Bien qu’il ne soit pas a priori axé sur la performance, il s’avère
que le langage offre certaines fonctionnalités liées à l’optimisation.
Cependant, le gain en performance a un impact sur
la généricité du code, l’optimisation limitant celle-ci. Climb
est une bibliothèque de traitement d’image écrite dans ce langage,
ayant pour objectif de se comparer à des équivalents
écrits dans des langages statiques tels que C++. L’objectif est
de profiter de la généricité qu’offre Common Lisp pour l’écriture
d’une bibliothèque de traitement d’image. Mais une telle bibliothèque
a également des contraintes de performance, il s’agit donc de trouver un
terrain d’entente entre ces deux aspects. Nous présenterons les
différentes fonctionnalités qu’offre Common Lisp pour optimiser un
programme, et leur utilisation dans Climb pour rendre la bibliothèque
plus rapide, sans pour autant diminuer sa généricité.
Nous présenterons également les premiers résultats du travail
d’optimisation dans Climb, le travail restant et les apports de
l’utilisation de Common Lisp pour une telle tâche.
* 12h15 : Construction d’une interface pour et avec Climb -- Laurent Senta
Climb est une bibliothèque de traitement d’image générique.
Encore à l’état de prototype, Climb fournit déjà un certain
nombre d’outils comme les morphers et l’opérateur $ qui permettent
de simplifier la définition de chaînes d’algorithmes.
Afin de prolonger cet aspect, une interface graphique a été
développée. Celle-ci permet de construire des chaînes de traitement
d’image sans connaissance en programmation, tout
en offrant un retour à la fois visuel et interactif. Notre approche
utilise les algorithmes et outils définis dans la bibliothèque
pour construire la logique interne de l’application ainsi
que ses différents aspects interactifs. La généricité étant l’une
des caractéristiques principales de Climb, nous avons été capables
d’étendre son champ d’application au-delà du traitement
d’image et ainsi montrer qu’elle peut être utilisée dans
des situations différentes telles que la construction d’une interface
graphique.
* 12h45 - 14h00 : PAUSE DEJEUNER
VAUCANSON
* 14h00 : Vers Vaucanson 2.0 -- David Moreira
Vaucanson est une plate-forme de manipulation d’automates
et de transducteurs dont l’interface et le développement se
sont montrés complexes et inefficaces. Des travaux de spécifications
et de design ont été effectués afin d’avoir un coeur efficace
en terme de développement et de vitesse. Cette version
2.0 de Vaucanson est actuellement en développement. Ce rapport
présente la version 2.0 de Vaucanson et son utilisation par
le portage de deux algorithmes : l’évaluation d’un mot par un
automate et la déterminisation d’automates. Dans une seconde
partie, nous montrerons si Vaucanson 2.0 tient ses promesses
en termes de vitesse d’exécution.
OLENA
* 14h30 : Approche parallèle pour le calcul de l'arbre des formes en
n-dimensions -- Sébastien Crozet
L’arbre des formes est une transformée d’image utile pour effectuer
des traitements sur des images discrètes de façon auto-duale.
Un algorithme (non publié), travaillant sur des images
n-dimensionnelles dans l’espace des complexes cellulaires,
nous permet déjà de construire un arbre des formes en temps
quasi-linéaire. Cependant, cet algorithme reste souvent largement
plus lent que d’autres approches en temps (n log(n)) sur
des images naturelles en 2D ou 3D, le nombre de cellules à traiter
dans l’espace des complexes étant très élevé. En vue d’améliorer
ces temps de calculs, nous présentons une approche pour
paralléliser l’algorithme de calcul d’arbre quasi-linéaire en exhibant
des propriétés topologiques et algorithmiques qui ne
peuvent être facilement obtenues par les autres approches existantes.
* 15h00 : Extraction de texte avec des ondelettes -- Raphael Boissel
Nous allons présenter une méthode permettant de différencier
le texte du non-texte dans une image en utilisant des descripteurs
inspirés des algorithmes de compression de données.
L’objectif principal de cette approche est de calculer un signal
qui va permettre à des systèmes d’apprentissage supervisés
(comme des kppv ou des machines à vecteurs de support) de
classifier le texte et le fond d’une image. Afin de calculer ce
signal, nous utiliserons des méthodes à base d’ondelettes similaires
à celles utilisées dans les formats de compression jpeg
ou png. Nous allons également étudier quelles ondelettes produisent
les meilleurs résultats, avec quel système d’apprentissage
et comparer cela avec d’autres descripteurs, qui ne sont
pas à base d’ondelettes. Enfin, nous verrons comment il est
possible de diminuer le temps de calcul nécessaire pour ces
descripteurs en utilisant l’élévation en ondelette et des méthodes
optimisées pour calculer l’image polaire.
* 15h30 - 15h45 : PAUSE
* 15h45 : Améliorer Horn-Schunck -- Sylvain Lobry
Calculer le flux optique a de nombreuses applications telles
que l’estimation de mouvement ou un premier pas vers l’inpainting
vidéo. L’équation du flux optique ne peut pas être résolue
telle quelle à cause du problème de fenêtrage (deux inconnues
pour une seule équation). Un ensemble d’algorithme
essaie de résoudre cette équation en se basant sur une stratégie
globale, c’est-à-dire en essayant d’avoir des petites variations
dans le flux. Le premier d’entre eux est l’algorithme d’Horn-
Schunck. Celui-ci, même s’il marche dans de nombreux cas, a
plusieurs inconvénients, y compris celui d’être lent et de ne pas
pouvoir trouver les grands déplacements. Dans le but de résoudre
ces problèmes, plusieurs stratégies ont été développées.
Nous présenterons la méthode et analyserons les bénéfices apportés
en appliquant une stratégie multi-échelle à l’algorithme
d’Horn-Schunck.
* 16h15 : Inpainting rapide préservant la structure -- Coddy Levi
L’inpainting consiste à réparer des parties d’une image de façon
visuellement plausible. Son but peut être de réparer des
régions endommagées, ou de supprimer des objets tels que du
texte superposé à une vidéo. De nombreuses approches ont été
proposées pour répondre au problème dans le cas de petites
ou de larges régions. Cependant la plupart d’entre elles ne sont
pas adaptées à des applications en temps réel. Nous proposons
une méthode plus simple basée sur la reconstruction de structure
et la diffusion des couleurs afin de répondre au problème
dans une optique de temps réel.
--
Daniela Becker
Responsable administrative du LRDE
Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 4 juillet 2012 (14h00-17h00).
Au programme:
* 14h: Vérification efficace de propriétés insensibles au bégaiement.
-- Ala Eddine Ben Salem (doctorant)
Le model checking est une technique de vérification formelle
automatique. Prenant en entrée un modèle décrivant toutes les exécutions
possibles du système et une propriété exprimée sous la forme d'une
formule de logique temporelle, un algorithme de model checking répond si
le modèle satisfait ou non la formule. Le problème principal du
model-checking est l'explosion combinatoire de l'espace d'états
décrivant le système.
Afin d'améliorer les performances, on a apporté les contributions
suivantes à l'approche automate du model checking. D'abord
l'amélioration de l'algorithme de vérification en deux passes de
l'approche basée sur les automates Testeur TA (Testing Automaton).
Ensuite la proposition d'une méthode permettant de transformer un
automate TA en un automate vérifiable en une seule passe, qu'on a appelé
STA (Single-pass Testing Automaton). Enfin, la contribution la plus
significative est un nouveau type d'automate baptisé TGTA
(Transition-based Generalized Testing Automaton). L'apport principal de
cette nouvelle approche consiste à proposer une méthode permettant de
supprimer les transitions bégayantes dans un TGTA sans avoir besoin, ni
d'ajouter une seconde passe comme dans l'approche TA, ni d'ajouter un
état artificiel comme dans l'approche STA.
-- A.E. Ben Salem est ingénieur ENSEEIHT-2005 en Informatique et
Mathématiques Appliquées, il a obtenu en parallèle un Master Recherche
Sûreté du Logiciel et Calcul à haute Performance à l’INP Toulouse.
Depuis 2011, il est doctorant au LRDE et au LIP6 sur la vérification
formelle de propriétés sur des systèmes logiciels, en lien avec le
projet Spot.
* 14h30: Composition dynamique de techniques pour le model checking efficace
-- Étienne Renault (doctorant)
Le model checking est une technique qui permet de s'assurer qu'un
système vérifie un ensemble de caratéristiques appelées propriétés. Le
système et la négation de la formule sont ensuite représentés de manière
abstraite (ici un automate) pour pouvoir détecter des comportements
incohérents. Ces propriétés ont été classifiées et possèdent des
particularités qui peuvent être exploitées afin de réduire la complexité
du processus de vérification. Nous montrerons ici comment tirer parti
dynamiquement des différentes classes de formules.
-- E. Renault est diplômé de Paris VI en système et applications
réparties, il s'intéresse à la vérification formelle des systèmes
concurents. Il a intégré cette année le LRDE dans le cadre de sa thèse
portant sur la composition dynamique de techniques pour le model
checking efficace. Ce travail, en collaboration avec l'équipe MoVe du
Lip6, s'intègre au projet Spot.
* 15h30: Filtrage morphologique dans les espaces de formes : Applications avec la représentation d'image par arbres
-- Yongchao Xu (doctorant)
(Morphological Filtering in Shape Spaces: Applications using Tree-Based
Image Representations)
Connected operators are filtering tools that act by merging elementary
regions of an image. A popular strategy is based on tree-based image
representations: for example, one can compute a shape-based attribute on
each node of the tree and keep only the nodes for which the attribute is
sufficiently strong. This operation can be seen as a thresholding of the
tree, seen as a graph whose nodes are weighted by the attribute. Rather
than being satisfied with a mere thresholding, we propose to expand on
this idea, and to apply connected filters on this latest graph.
Consequently, the filtering is done not in the image space, but in the
space of shapes built from the image. Such a processing is a
generalization of the existing tree-based connected operators. Indeed,
the framework includes classical existing connected operators by
attributes. It also allows us to propose a class of novel connected
operators from the leveling family, based on shape attributes. Finally,
we also propose a novel class of self-dual connected operators that we
call morphological shapings.
-- Yongchao Xu received the B.S. degree in optoelectronic engineering from
Huazhong University of Science and Technology, China, in 2008, the
"diplôme d'ingénieur" in electronic & embedded system at Polytech'
Paris-Sud and the M.S. degree in signal & image processing from
Université Paris Sud, in 2010. He is currently a PhD student at
Université Paris Est working on image segmentation, morphological image
analysis and, especially shape-based connected morphology.
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
Hello,
it is my pleasure to announce that I will hold a 2 hours tutorial on
Lisp extensibility and its impact on DSL implementation at the next
International Lisp Conference, Kyoto, Japan, October 2012.
For more information, please consult:
http://international-lisp-conference.org/2012/tutorials.html
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22