M. Shibashis Guha, professeur invité du LMF
Shibashis Guha
Shibashis Guha est lecteur au Tata Institute of Fundamental Research de Mumbai. Ses recherches portent sur les méthodes formelles, la vérification, la synthèse réactive, la logique et la théorie des automates.
Shibashis a fait ses études doctorales à l'Indian Institute of Technology Delhi, après quoi il a effectué ses recherches postdoctorales à l'Université hébraïque de Jérusalem et à l'Université libre de Bruxelles.
Le Laboratoire Méthodes Formelles (LMF)
Le Laboratoire Méthodes Formelles (LMF) est le laboratoire d'informatique de l’École normale supérieure Paris-Saclay, de l’université Paris-Saclay et du Centre National de la Recherche Scientifique (CNRS) en tant qu'UMR 9021.
Il ambitionne 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 Modèles" et le troisième, "Interactions", est une ouverture à d’autres domaines tels que l’intelligence artificielle et la biologie.
Les conférences
Strategy synthesis for global window PCTL
Date : 21 juin, 14h
Salle : Amphi Lagrange (1Z14)
Résumé
Étant donné un processus de décision markovien (PDM) M et une formule Phi, le problème de la synthèse de stratégie demande s'il existe une stratégie sigma telle que la chaîne de Markov résultante M[sigma] satisfasse Phi. Ce problème est connu pour être indécidable pour la logique temporelle probabiliste PCTL. Nous étudions une classe de formules qui peuvent être considérées comme un fragment de PCTL où une propriété locale d'horizon borné est appliquée tout au long de l'exécution. De plus, nous permettons des expressions linéaires dans les inégalités probabilistes. Cette logique est à la frontière de la décidabilité, selon le type de stratégies considérées. En particulier, il est démontré que la synthèse de stratégies est décidable lorsque les stratégies sont déterministes, alors que le problème est indécidable pour des stratégies arbitraires.
A Game of Pawns
Date : 28 juin, 14h
Salle : Amphi Lagrange (1Z14)
Résumé
Nous introduisons et étudions les jeux de pions, une classe de jeux de graphes à deux joueurs à somme nulle et à tour de rôle. Un jeu de graphe à tour de rôle consiste à placer un pion sur un sommet initial, et celui qui contrôle le sommet sur lequel se trouve le pion choisit son prochain emplacement. Il en résulte un chemin dans le graphe, qui détermine le vainqueur. Traditionnellement, le contrôle des sommets est prédéterminé et fixe. La nouveauté des jeux de pions réside dans le fait que le contrôle des sommets change dynamiquement tout au long du jeu, comme suit. Chaque sommet d'un jeu de pions appartient à un pion. À chaque tour, les pions sont répartis entre les deux joueurs et le joueur qui contrôle le pion qui possède le sommet sur lequel se trouve le jeton choisit le prochain emplacement du jeton.
Le contrôle des pions change dynamiquement tout au long du jeu selon un mécanisme fixe. Plus précisément, nous définissons plusieurs mécanismes basés sur la saisie dans lesquels le contrôle d'au plus un pion est transféré à la fin de chaque tour. Nous étudions la complexité de la résolution des jeux de pions, en nous concentrant sur les objectifs d'accessibilité et en paramétrant le problème par le mécanisme utilisé et par des restrictions sur la propriété des pions sur les sommets. D'un point de vue positif, même si les jeux de pions sont des jeux à tour de rôle exponentiellement succincts, nous identifions plusieurs classes naturelles qui peuvent être résolues en PTIME. Du côté négatif, nous identifions plusieurs classes EXPTIME-completes, où nos preuves de dureté sont basées sur une nouvelle classe de jeux appelés jeux Lock & Key, qui peuvent être d'un intérêt indépendant.