Informations générales
Intitulé de l'offre : Post-doctorant (H/F) Analyse de la "decisiveness" des systèmes temporisés probabilisés
Référence : UMR9021-MARGRA0-001
Nombre de Postes : 1
Lieu de travail : GIF SUR YVETTE
Date de publication : lundi 27 janvier 2025
Type de contrat : Chercheur en contrat CDD
Durée du contrat : 8 mois
Date d'embauche prévue : 1 avril 2025
Quotité de travail : Complet
Rémunération : Entre 3081,33€ et 4291,26€ bruts mensuels selon l'expérience
Niveau d'études souhaité : Doctorat
Expérience souhaitée : 5 à 10 années
Section(s) CN : 6 - Sciences de l'information : fondements de l'informatique, calculs, algorithmes, représentations, exploitations
Missions
Dans le cadre de l'ANR MAVERIQ, nous souhaitons étudier la propriété de "decisiveness" dans les systèmes probabilisés temporisés du double point de vue sémantique et algorithmique.
Activités
- Comparaison des différentes sémantiques des systèmes probabilisés temporisés
- Algorithmique efficace de vérification des les systèmes probabilisés temporisés décisifs
Compétences
La personne recrutée devra posséder des compétences en :
- Probabilité
- Logique et systèmes temporisés
- Algorithmique de la vérification probabiliste
Contexte de travail
Le post-doctorant recruté travaillera au sein du laboratoire LMF. Le Laboratoire Méthodes Formelles (LMF) est un laboratoire d'informatique spécialisé dans le développement de méthodes formelles. Il a trois tutelles principales (CNRS, Université Paris-Saclay, ENS Paris-Saclay) et deux partenaires (Inria, CentraleSupélec). Son ambition est d'éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d'analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l'informatique quantique. Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves et langages » et « Modèles » ; le troisième, « Interactions », est une ouverture à d'autres domaines tels que l'intelligence artificielle ou la biologie. Il est l'un des laboratoires leaders mondiaux dans son domaine.
Le LMF est localisé sur le plateau du Moulon (91), dans les locaux de l'ENS Paris-Saclay et dans le bâtiment 650 de l'Université Paris-Saclay. Le laboratoire est composé d'une centaine de membres, dont une cinquantaine de chercheurs (CNRS, Inria) ou d'enseignants-chercheurs (Université Paris-Saclay, ENS Paris-Saclay, CentraleSupélec).
Le post-doctorant recruté travaillera au sein de l'équipe Model Checking and Synthesis du LMF.
Cette équipe s'intéresse aux fondements des modèles de calcul. Les modèles formels de calcul comprennent les classes de langages et de machines tels que les automates finis, les jeux, les systèmes à piles et à compteurs, les automates pondérés, les systèmes temporisés (continus), les processus stochastiques.
Contraintes et risques
Travail sur écran