November 2015 - Annonce

publications: two papers accepted at Spin'15
by Alexandre Duret-Lutz 20 Jun '16

20 Jun '16

I am happy to announce that the following two papers have been accepted at the 22nd International SPIN Symposium on Model Checking of Software (SPIN 2015) to be held in Stellenbosch, South Africa on 24–26 August 2015. --- On Refinement of Büchi Automata for Explicit Model Checking František Blahoudek¹, Alexandre Duret-Lutz², Vojtěch Rujbr¹, and Jan Strejček¹ ¹Faculty of Informatics, Masaryk University, Brno, Czech Republic ²LRDE, EPITA, Le Kremlin-Bicêtre, France https://www.lrde.epita.fr/wiki/Publications/blahoudek.15.spin Abstract: In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand andmore importantly, for which the explicit model checking process performs better. --- Practical Stutter-Invariance Checks for ω-Regular Languages Thibaud Michaud and Alexandre Duret-Lutz LRDE, EPITA, Le Kremlin-Bicêtre, France https://www.lrde.epita.fr/wiki/Publications/michaud.15.spin Abstract: We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns out, implementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant. -- Alexandre Duret-Lutz

3 2

Soutenance de thèse d'Edwin Carlinet - vendredi 27 novembre (Paris Est)
by Thierry Géraud 16 Nov '15

16 Nov '15

Bonjour à tous, Nous avons le plaisir de vous inviter à la soutenance de thèse d'Edwin Carlinet intitulée ``Un arbre des formes pour des images multi-variées''. Celle-ci aura lieu le vendredi 27 novembre 2015 à 14h00 en amphi 210 à l'ESIEE Paris, situé au 2 boulevard Blaise Pascal, Cité Descartes, à Noisy-le-Grand (93). Vous trouverez un plan d'accès à l'école à l'adresse suivante : http://www.esiee.fr/Infos-pratiques/acces.php La soutenance sera suivie d'un pot. Manuscrit de thèse ------------------ Téléchargeable à cette adresse : http://www.lrde.epita.fr/wiki/Affiche-these-EC Composition du jury de thèse ---------------------------- Rapporteurs : Coloma Ballester (Universitat Pompeu Fabra) Philippe Salembier (Universitat Politècnica de Catalunya) Ludovic Macaire (Université Lille 1) Examinateurs : Jesús Angulo (Mines ParisTech) Pascal Monasse (Ecole des Ponts ParisTech) Directeurs de thèse : Jean Serra (ESIEE Paris - Université Paris-Est Marne-la-Vallée) Thierry Géraud (EPITA) Résumé de la thèse ------------------ De nombreuses applications issues de la vision par ordinateur et de la reconnaissance des formes requièrent une analyse de l'image multi-échelle basée sur ses régions. De nos jours, personne ne considérerait une approche orientée « pixel » comme une solution viable pour traiter ce genre de problèmes. Pour répondre à cette demande, la Morphologie Mathématique a fourni des représentations hiérarchiques des régions de l'image telles que l'Arbre des Formes (AdF). L'AdF représente l'image par un arbre d'inclusion de ses lignes de niveaux. L'AdF est ainsi auto-dual et invariant au changement de contraste, ce qui fait de lui une structure bien adaptée au traitements d'images de haut niveau. Néanmoins, il est seulement défini aux images en niveaux de gris et la plupart des tentatives d'extension aux images multivariées (en imposant un ordre total « arbitraire ») ne sont pas satisfaisantes. Dans ce manuscrit, nous présentons une nouvelle approche pour étendre l'AdF scalaire au images multivariées : l'Arbre des Formes Multivarié (AdFM). Cette représentation est une « fusion » des AdFs calculés marginalement sur chaque composante de l'images. On vise à fusionner les formes marginales de manière « sensée » en préservant un nombre maximal d'inclusion. La méthode proposée a des fondements théoriques qui consistent en l'expression de l'AdF par une carte topographique de la variation totale curvilinéaire depuis la bordure de l'image. C'est cette reformulation qui a permis l'extension de l'AdF aux données multivariées. De plus, l'AdFM partage des propriétés similaires avec l'AdF scalaire ; la plus importante étant son invariance à tout changement ou inversion de contraste marginal (une sorte d'auto-dualité dans le cas multidimensionnel). Puisqu'il est évident que, vis-à-vis du nombre sans cesse croissant de données à traiter, nous ayons besoin de techniques rapides de traitement d'images, nous proposons un algorithme efficace qui permet de construire l'AdF en temps quasi-linéaire vis-à-vis du nombre de pixels et quadratique vis-à-vis du nombre de composantes. Nous proposons également des algorithmes permettant de manipuler l'arbre, montrant ainsi que, en pratique, l'AdFM est une structure facile à manipuler, polyvalente, et efficace. Finalement, pour valider la pertinence de notre approche, nous proposons quelques expériences testant la robustesse de notre structure aux composantes non-pertinentes (avec du bruit ou à faible dynamique) et nous montrons que ces défauts n'affectent pas la structure globale de l'AdFM. De plus, nous proposons des applications concrètes utilisant l'AdFM. Certaines sont juste des modifications mineures aux méthodes employant d'ores et déjà l'AdF scalaire mais adaptées à notre nouvelle structure. Par exemple, nous utilisons l'AdFM à des fins de filtrage, segmentation, classification et de détection d'objet. De ces applications, nous montrons ainsi que les méthodes basées sur l'AdFM surpassent généralement leur analogue basé sur l'AdF, démontrant ainsi le potentiel de notre approche.

1 0

Poster accepted at TPNC 2015
by Didier Verna 10 Nov '15

10 Nov '15

Dear collegues, I am happy to inform you that my poster submission to TPNC 2015 (Theory and Practice of Natural Computing, Mieres, Spain, 15-16 December) has been accepted. The poster's abstract is given below: Scientists have been drawing bridges between Computer Science and Biology for a long time now. Biologists make a constant use of tools from Computer Science to gain a better understanding of their research field (genetics, systems biology etc.). Conversely, many ideas and models from Biology are used in Computer Science (artificial intelligence, neural networks, genetic algorithms etc.). In every such case however, these bridges are intentional: there is always the will to grab a model here, and apply it there. But what if other connections existed before we even realized it? What if common, inherent behavioral patterns were to be found in both Computer Science and Biology? In other words, are there any bridges to be discovered rather than invented? This poster will exhibit one such bridge, discovered almost by accident: the behavioral equivalence of LaTeX, a software typesetting system, and unicellular life, in terms of evolution. In Biology, evolution is usually seen as a tinkering process, different from what an engineer does when he plans the development of his systems. Recently however, studies have shown that even in Biology, there is a part of good engineering. On the other hand, computer scientists have much more difficulty to admit that there is also a great deal of tinkering in what they do, and that their software systems behave more and more like tinkered, biological realms every day. The LaTeX world is probably one of the best examples of this. It is composed of thousands of software components in constant evolution, most notably documents, classes and styles. Classes and styles are born, evolve or die, interact with each other, compete or cooperate, very much like living organisms do at the cellular level. By considering LaTeX documents as unicellular organisms, classes as their initial genetic material and styles as viruses that infect them, we are able to exhibit a fascinating number of behavioral patterns common to both worlds. We analyze infection methods, types and cures, and we show how both LaTeX and unicellular organisms are able to survive in a world of perpetual war, by using the same techniques. This work may be the very first example of software "reverse-tinkering", and may help to eventually realize that the silicon-based world is much more biological than we ever would have thought. As such, and in light of recent work that tend to consider cells as proper genetic computers, it is also time to consider than maybe we haven't actually invented Computer Science; only discovered it. -- My new Jazz CD entitled "Roots and Leaves" is out! Check it out: http://didierverna.com/records/roots-and-leaves.php Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0