Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

12 octobre 2020

Simulation et synthèse garantie de Systèmes Cyber-Physiques

Adrien Le Coënt (LACL)

Les systèmes cyber-physiques, faisant interagir des éléments informatiques et des éléments physiques, sont un des modèles majeurs de ces dernières années, pour lesquels la modélisation et la vérification formelle sont encore des challenges actuels.

Les difficultés majeures rencontrées actuellement dans l’étude formelle de ces systèmes sont: 1. La complexité des algorithmes de synthèse, limitant fortement la dimension des systèmes que l’on peut concevoir 2. La difficulté du calcul de l’ensemble atteignable, limitant le type de dynamique continue que l’on peut considérer dans ces modèles.

Nous présenterons des études de cas qui illustrent ces difficultés, et proposerons des méthodes qui tentent de répondre à ces difficultés. Plus précisément, nous proposons une méthode de synthèse compositionnelle qui permet de casser la complexité algorithmique de la recherche de contrôleur. Nous présenterons également comment utiliser une méthode de simulation garantie dans un outil de synthèse de contrôleur.

5 octobre 2020

La réalisabilité, de Curry Howard au Forcing

Laura Fontanella (LACL)

Attention salle inhabituelle : salle MSE 007.

La réalisabilité vise à extraire le contenu computationnel des preuves mathématiques en établissant une correspondance entre formules d’un système logique et programmes de telle manière que les `réalisateurs’ d’une formule démontrable dans le système (c. à d. les programmes qui sont associés à une telle formule via cette correspondance) nous fournissent des informations sur sa preuve.

Dans ce sens, la correspondance de Curry Howard peut être vu comme un résultat de réalisabilité. L’isomorphisme de Curry Howard établit une correspondance entre logique intuitionniste et lambda calcul simplement typé. Grâce aux travaux de Griffin et Krivine, la réalisabilité a ensuite évolué jusqu’à englober la logique classique d’abord, puis la théorie des ensembles. Les techniques développées par Krivine pour définir des modèles de réalisabilité pour la théorie des ensembles généralisent la méthode de Forcing, en fait les modèles de forcing sont des cas particulier de modèles de réalisabilité.

Nous allons aborder ces techniques et nous allons discuter les difficultés liées à la construction d’un modèle pour l’Axiome du Choix, je vous présenterai ainsi mes derniers résultats dans ce contexte fruit d’une collaboration avec Guillaume Geoffroy.