September 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

[Seminaire-LRDE] Merc. 7 oct. 2015: Tamy Boubekeur, Telecom ParisTech
by Akim Demaille 28 Sep '15

28 Sep '15

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 7 octobre 2015 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2015-10-07 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 7 octobre 2015 : * 11h00: Intégrales de Morton pour la Simplification Géométrique Haute Vitesse -- Tamy Boubekeur, Telecom ParisTech - CNRS - University Paris-Saclay http://perso.telecom-paristech.fr/~boubek/ Le traitement géométrique 3D temps-réel a progressivement atteint un niveau de performance rendant un grand nombre de primitives inspirées du traitement du signal compatible avec les applications interactives. Cela a souvent été rendu possible grâce à la co-conception des opérateurs, des structures de données et du support matériel d’exécution. Parmi les principales classes d'opérateurs géométriques, le filtrage et le sur-échantillonnage (par raffinement) ont été exprimés sous des contraintes temps-réel avec succès. Cependant, l'opérateur de sous-échantillonnage – la simplification adaptative – demeure un cas problématique pour les données non triviales. Dans ce contexte, nous proposons un nouvel algorithme de simplification géométrique rapide basé sur un nouveau concept : les intégrales de Morton. En sommant les quadriques d'erreurs associées aux échantillons géométriques selon leur ordre de Morton, notre approche permet d'extraire de manière concurrente les nœuds correspondants à une coupe adaptative dans la hiérarchie implicite ainsi définie, et d'optimiser la position des sommets du maillage simplifié en parallèle. Cette méthode est inspirée des images intégrales et exploite les avancées récentes en construction et parcours haute performance de hiérarchies spatiales. L'implémentation GPU de notre approche peut simplifier des maillages composés de plusieurs millions d'éléments à un taux de rafraîchissement interactif, tout en fournissant une géométrie simplifiée de qualité supérieure aux méthodes uniformes et en préservant notamment les structures géométriques saillantes. Notre algorithme est compatible avec les maillages indexés, les soupes polygonales et les nuages de points, et peut prendre en compte des attributs de surfaces (normal ou couleur par exemple) et des métriques d'erreurs alternatives. -- Tamy Boubekeur est Professeur en Science Informatique à Télécom ParisTech (Institut Mines-Télécom, CNRS UMR 5141, Université Paris-Saclay). Il mène ses activités de recherche dans le domaine de l’informatique graphique 3D, s'intéressant tout particulièrement à la modélisation et à la synthèse de formes, de matières et d’animation 3D numériques, mais également aux systèmes visuels interactifs à hautes performances. De 2004 à 2007, il a été membre de l’INRIA Bordeaux (France) et chercheur invité régulier à l’Université de Colombie Britannique à Vancouver (Canada). Il a obtenu son Doctorat en Informatique à l’Université des Sciences et Technologies de Bordeaux en 2007. Par la suite, il a rejoint l’Unversité Technique de Berlin (TU Berlin) comme chercheur associé. En 2008, il a rejoint le Département de Traitement du Signal et des Images de Télécom ParisTech comme Maître de Conférences et a créé le groupe d’informatique graphique. Il a obtenu son Habilitation à Diriger des Recherches (HDR) en Informatique à l’Université Paris XI en 2012 avant de devenir Professeur à Télécom ParisTech en 2013. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

L'air de rien 34.0
by Daniela Becker 11 Sep '15

11 Sep '15

Bonjour, nous avons le plaisir de vous annoncer la sortie du n°34 du bulletin du LRDE. C'est un numéro Spécial Rentrée qui présente l'ensemble des permanents 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 : https://www.lrde.epita.fr/wiki/Latest_issue -- Daniela Becker Responsable administrative du LRDE

1 0

publication: SAT-based Minimization of Deterministic ω-Automata (LPAR'15)
by Alexandre Duret-Lutz 01 Sep '15

01 Sep '15

I am happy to announce that the following papers has been accepted at the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) to be held at the University of the South Pacific (Suva, Fiji) on 24–28 November 2015. SAT-based Minimization of Deterministic ω-Automata Souheib Baarir¹, Alexandre Duret-Lutz¹ ¹LRDE, EPITA, Le Kremlin-Bicêtre, France https://www.lrde.epita.fr/wiki/Publications/baarir.15.lpar Abstract: We describe a tool that inputs a deterministic ω-automaton with any acceptance condition, and synthesizes an equivalent ω-automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exist. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal ω-automata equivalent to given properties, for different acceptance conditions. -- Alexandre Duret-Lutz

1 0