LINARD Alban

Docteur
Équipe : MoVe
Date de départ : 30/09/2009
https://lip6.fr/Alban.Linard

Direction de recherche : Fabrice KORDON

Co-encadrement : PAVIOT-ADET Emmanuel

Sémantique paramétrable des Diagrammes de Décision : une démarche vers l'unification

Les Diagrammes de Décision sont des structures de données compactes, qui représentent efficacement des ensembles de données de taille importante sous forme d'un graphe, dont les parties communes sont partagées. Cette efficacité se traduit, lors de la manipulation de ces structures, aussi bien dans la mémoire consommée que dans le temps d'exécution. Elle est toutefois dépendante des données représentées : le gain peut varier en pratique de très faible à exponentiel. Ainsi, des techniques récentes ont permis d'atteindre plus de 10^2500 états différents dans 1 Go de mémoire en environ une minute. De nombreuses variantes ont été définies depuis le début des années 90 à partir des Diagrammes de Décision Binaire (BDD), à l'origine de ces structures de données. Les évolutions sont très variées, allant d'optimisations de la structure à l'extension hiérarchique des Diagrammes de Décision. Il existe ainsi actuellement plusieurs dizaines de variantes. Malgré leur utilisation dans de nombreux domaines, les Diagrammes de Décision sont à ce jour différentes structures, qui évoluent indépendamment les unes des autres. Il n'existe pas de théorie unifiée, ce qui a certes permis des évolutions rapides de ces structures, mais est un frein à la réutilisation des résultats obtenus dans le domaine. Nous proposons un cadre unifiant la majeure partie des Diagrammes de Décision existants à l'heure actuelle, le grand nombre de variantes ne permettant pas d'espérer tous les couvrir. Nous montrons que cette généralisation se fait sans perte d'efficacité, en fournissant un moyen de récupérer les optimisations de structure définies dans certains évolutions. De plus, en important ces optimisations dans le cadre unifié, nous permettons leur application pour certains Diagrammes de Décision pour lesquels elles n'étaient jusqu'à présent pas définies. L'unification réalisée permet de mélanger, au sein d'un même Diagramme de Décision, les spécificités de variantes jusque là séparées.

Soutenance : 29/09/2009

Membres du jury :

Didier Buchs Professeur à l’Université de Genève [Rapporteur]
Jean-Michel Couvreur, Professeur à l’Université d’Orléans [Rapporteur]
Béatrice Bérard, Professeur à l'université P. & M. Curie
Olivier H. Roux, Maître de Conférences HDR à l’IUT de Nantes
Alexandre Duret-Lutz, Maître de Conférences à l’EPITA
Fabrice Kordon, Professeur à l'université P. & M. Curie
Emmanuel Paviot-Adet, Maître de Conférences à l’Université Paris Descartes

Date de départ : 30/09/2009

Publications 2006-2016

  • 2016
  • 2013
    • É. André, B. Barbot, C. Démoulins, L. Hillah, F. Hulin‑Hubard, F. Kordon, A. Linard, L. Petrucci : “A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems”, 15th International Conference on Formal Engineering Methods (ICFEM'13), vol. 8144, Lecture Notes in Computer Science, Queenstown, New Zealand, pp. 199-214, (Springer Berlin Heidelberg) (2013)
    • É. André, Y. Lembachar, L. Petrucci, F. Hulin‑Hubard, A. Linard, L. Hillah, F. Kordon : “CosyVerif: An Open Source Extensible Verification Environment”, 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'13), Singapore, Singapore, pp. 33-36, (IEEE Computer Society Press) (2013)
    • F. Kordon, A. Linard, M. Becutti, D. Buchs, L. Fronc, L. Hillah, F. Hulin‑Hubard, F. Legond‑Aubry, N. Lohmann, A. Marechal, E. Paviot‑Adet, F. Pommereau, C. Rodríguez, Ch. Rohr, Y. Thierry‑Mieg, H. Wimmel, C. Wolf : “Web Report on the Model Checking Contest @ Petri Net 2013”, (2013)
  • 2012
    • F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, K. Lampka, N. Lohmann, E. Paviot‑Adet, Y. Thierry‑Mieg, H. Wimmel : “Report on the Model Checking Contest at Petri Nets 2011”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 7400 (VI), Lecture Notes in Computer Science, pp. 169-196, (Springer) (2012)
  • 2010
    • A. Linard, E. Paviot‑Adet, F. Kordon, D. Buchs, S. Charron : “polyDD: Towards a Framework Generalizing Decision Diagrams”, 10th International Conference on Application of Concurrency to System Design (ACSD'2010), Braga, Portugal, pp. 124-133, (IEEE) (2010)
    • A. Hamez, S. Hostettler, A. Linard, A. Marechal, E. Paviot‑Adet, M. Risoldi : “Specification of Decision Diagram Operations”, International Workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency (SUMo'2010 associated with Petri Nets 2010), vol. 827, CEUR-WS, Braga, Portugal, pp. 437-451, (CEUR) (2010)
  • 2009
  • 2006
    • F. Kordon, A. Linard, E. Paviot‑Adet : “Optimized Colored Nets Unfolding”, International Conference on Formal Methods for Networked and Distributed Systems (FORTE '06), vol. 4229, Lecture Notes in Computer Science, Paris, France, pp. 339-355, (Springer-Verlag) (2006)
    • A. Hamez, L. Hillah, F. Kordon, A. Linard, E. Paviot‑Adet, X. Renault, Y. Thierry‑Mieg : “New Features in CPN-AMI 3 : Focusing on the Analysis of Complex Distributed Systems”, 6th International Conference on Application of Concurrency to System Design (ACSD '06), Turku, Finland, pp. 273-275, (IEEE Computer Society) (2006)
Mentions légales
Carte du site