Chercheur post-doctoral au LAAS-CNRS, équipe VERTICS, Toulouse

Activités



Je suis actuellement chercheur post-doctoral au Laboratoire d'Analyse et d'Architecture des Systèmes (LAAS-CNRS) à Toulouse, équipe Vérification de Systèmes Temporisés Critiques (VERTICS).

Je m'intéresse à la modélisation, à l'analyse et à la synthèse efficaces de systèmes concurrents et distribués, avec et sans temporisation, de sorte à garantir les propriétés qualitatives et  quantitatives désirées pour les applications. Non-exhaustivement, j'étudie :
  • la modélisation par réseaux de Petri pondérés et leurs diverses extensions : temporisées, stochastiques... ;

  • la modélisation par automates et leurs extensions temporisées ;

  • la détermination de conditions suffisantes efficaces garantissant des propriétés qualitatives fondamentales pour de nombreux systèmes réels tels que les systèmes embarqués ; les problèmes que j'attaque sont souvent expspace-hard, tandis que les conditions suffisantes sont assurées en temps polynomial, tout en s'appliquant à un très grand nombre de cas ;

  • l'ordonnancement de systèmes temporisés et l'analyse de leurs performances, typiquement via le modèle réseau de Petri pondéré ;

  • les logiques temporelles, en lien avec les techniques de classification et d'abstraction des traces ;

  • la simulation de systèmes.

Auparavant, je fus :

  • chercheur post-doctoral à ONERA Toulouse, DTIS, Équipe Systèmes embarqués, autonomes et sûrs – 2018

  • professeur assistant en Allemagne à l'université d'Oldenburg, Département d'informatique, Équipe Systèmes parallèles – Oct. 2015 à Sept. 2017

  • ATER à l'université Paris 7, IRIF – Oct. 2014 à Août. 2015.


Thèse de doctorat

Contribution à l'étude des réseaux de Petri généralisés  

Université Paris 6, LIP6, Octobre 2014

Directeurs:
                  Alix Munier-Kordon         LIP6, Univ. Paris 6
                  Jean-Marc Delosme       IBISC, Univ. Evry-val-d'Essonne

Publications




Articles soumis


On the Petri Nets with a Single Shared Place and Beyond.  43 pages :   Lien arXiv
avec Bernard Berthomieu, Silvano Dal Zilio et Didier Le Botlan.


Checking marking reachability with the state equation in Petri net subclasses.  44 pages :   Lien arXiv
avec Bernard Berthomieu, Silvano Dal Zilio et Didier Le Botlan.



Revues internationales avec comité de lecture


Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond. ToPNoC 2020, accepté, 26 pages,   
avec Raymond Devillers et Evgeny Erofeev.

Analysis and Synthesis of Weighted Marked Graph Petri Nets: Exact and Approximate Methods. Fundamenta Informaticae 2019, p. 1-30,  
avec Raymond Devillers.
Version finale : https://content.iospress.com/articles/fundamenta-informaticae/fi1837

Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach. ToPNoC 2019, p. 172-191,  
avec Raymond Devillers et Evgeny Erofeev.
Version finale : https://link.springer.com/chapter/10.1007%2F978-3-662-60651-3_7

Sufficient conditions for the marked graph realisability of labelled transition systems. Theoretical Computer Science 2018: 750: p. 101-116 
avec Eike Best et Harro Wimmel.
Version finale :  https://www.sciencedirect.com/science/article/pii/S0304397517307181

On Deadlockability, Liveness and Reversibility in Subclasses of Weighted Petri Nets. Fundamenta Informaticae 2018: 161(4): p. 383-421 
avec Raymond Devillers.
Version finale :  https://content.iospress.com/articles/fundamenta-informaticae/fi1708

On Liveness and Reversibility of Equal-Conflict Petri Nets. Fundamenta Informaticae 2016: 146(1):  p. 83-119  
avec Jean-Marc Delosme et Alix Munier-Kordon.
Version finale :  https://content.iospress.com/articles/fundamenta-informaticae/fi1376

Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri Nets. TECS 2014: 141: p. 1-25  
avec Jean-Marc Delosme et Alix Munier-Kordon.
Version finale :  https://dl.acm.org/citation.cfm?doid=2601432.2627349




Conférences internationales avec comité de lecture


Synthesis of Weighted Marked Graphs from CIrcular Labelled Transition Systems. ATAED@Petri Nets/ACSD 2019: p. 6-22 
avec Raymond Devillers et Evgeny Erofeev.

Analysis and Synthesis of Weighted Marked Graph Petri Nets. Petri Nets 2018: p. 19-39 
avec Raymond Devillers.
Version finale :  https://link.springer.com/chapter/10.1007%2F978-3-319-91268-4_2

Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems. ATAED@Petri Nets/ACSD 2018: p. 75-90 
avec Raymond Devillers et Evgeny Erofeev.

Proposition of an Action Layer for Electrum. ABZ 2018: p. 397-402 
avec Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo et Jeanne Tawa.
Version finale :  https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_30

On Liveness and Deadlockability in Subclasses of Weighted Petri Nets. Petri Nets 2017: p. 267-287 
avec Raymond Devillers.
Version finale :  https://link.springer.com/chapter/10.1007%2F978-3-319-57861-3_16

On the Reversibility of Live Equal-Conflict Petri Nets. Petri Nets 2015: p. 234-253 
avec Jean-Marc Delosme et Alix Munier-Kordon.
Version finale :  https://link.springer.com/chapter/10.1007%2F978-3-319-19488-2_12

On the Reversibility of Well-Behaved Weighted Choice-Free Systems. Petri nets 2014: p. 334-353 
avec Jean-Marc Delosme et Alix Munier-Kordon.
Version finale :  https://link.springer.com/chapter/10.1007%2F978-3-319-07734-5_18

Liveness evaluation of a cyclo-static DataFlow graph. DAC 2013: 3: p. 1-7
avec Mohamed Benazouz, Alix Munier-Kordon et Bruno Bodin.
Version finale :  https://dl.acm.org/citation.cfm?doid=2463209.2488736

Polynomial Sufficient Conditions of Well-Behavedness for Weighted Join-Free and Choice-Free Systems. ACSD 2013: p. 90-99 
avec Jean-Marc Delosme et Alix Munier-Kordon.
Best Paper Award
Version finale :  https://ieeexplore.ieee.org/document/6598344/

Enseignement




Enseignant vacataire, INSA Toulouse, 2019 - 2020 : niveau M1, totalisant environ 40 heures équiv. TD

Model-checking : TP.

Modèles temporels : TP.

Modélisation de systèmes concurrents : TP.



Professeur assistant en Allemagne, univ. Oldenburg, 2015 - 2017, en anglais et allemand : niveaux L2 / L3 / M1, totalisant environ 256 heures équiv. TD

Théorie de la complexité : niveau M1, TD.

Réseaux de Petri : niveau L3, TD.

Séminaires de programmation fonctionnelle, encadrement pour l'étude d'articles publiés : niveau L3.

Bases de l’informatique théorique, en amphithéâtre : niveau L2.

Encadrement du stage d'une étudiante de licence de l'université, niveau L3.



ATER temps plein à l'université Paris 7, 2014 - 2015, niveaux L1 / L3 / M2 informatique/Mathématiques, totalisant environ 192 heures équiv. TD


Introduction aux systèmes d’exploitation, principes de base des systèmes UNIX : niveau L1, Cours-TP.

Introduction à la programmation orientée objets et interfaces graphiques, Java, Swing et projet : niveau L3, TD et TP.

Programmation synchrone (environnement Scade), encadrement de projet : niveau M2 ingénierie, TP.

Initiation à la programmation 2, Java : niveau L1, TD et TP.



Moniteur à l'université Paris 6, 2011 - 2014, niveau L2 informatique, totalisant environ 192 heures équiv. TD

 
Machine et représentation : TD/TP.
 
Algorithmique élémentaire :  TD.

 

Contact



http://homepages.laas.fr/thujsa

 

Distinctions