Trois chercheurs récompensés pour leurs travaux sur la logique temporelle

Si de nombreux prix scientifiques célèbrent des travaux récents, certains laissent les années passer afin de constater les impacts à long terme sur la communauté des chercheurs. La conférence LICS (ACM–IEEE symposium on Logic in computer science) décerne ainsi chaque année un prix Test-of-Time pour distinguer les auteurs d’articles qui, vingt ans après leur publication, ont prouvé leur influence. Cette année, Philippe Schnoebelen, directeur de recherche CNRS au Laboratoire méthodes formelles (LMF, CNRS/ENS Paris-Saclay/Université Paris-Saclay), François Laroussinie, professeur à l’Université Paris Cité et membre de l’Institut de recherche en informatique fondamentale (IRIF, CNRS/Université Paris-Cité) et Nicolas Markey, directeur de recherche CNRS à l’Institut de recherche en informatique et systèmes aléatoires (IRISA, CNRS/Université Rennes 1), ont été récompensés pour leur article Temporal logic with forgettable past1  de juillet 2002.

Ces travaux s’inscrivent dans le domaine des méthodes formelles, qui permettent de raisonner sur des programmes avec des outils mathématiques. Il s’agit généralement de prouver de manière rigoureuse qu’ils vont s’exécuter correctement. « Comme quand un ingénieur veut construire un pont, la programmation comporte des aspects artisanaux et artistiques, mais il faut également une base scientifique rigoureuse pour empêcher que le tout s’effondre », commente Philippe Schnoebelen.

L’article traite plus précisément de la logique temporelle, qui permet de raisonner sur l’enchaînement des évènements qui surviennent lors de l’exécution d’un programme. Ce domaine a émergé dans les années 80, grâce notamment aux travaux de Joseph Sifakis, directeur de recherche émérite CNRS au laboratoire Verimag (CNRS/Université Grenoble Alpes) et premier français à avoir obtenu le prix Turing.

« Notre article s’inscrit dans cette continuité, explique Philippe Schnoebelen. Il a surtout apporté l’idée que la logique temporelle, qui ne s’intéressait alors qu’aux évènements futurs, devait aussi prendre en compte le passé, et ce à part à peu près égale. »

• 1F. Laroussinie, N. Markey and P. Schnoebelen. Temporal logic with forgettable past. Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 383-392, doi: 10.1109/LICS.2002.1029846.

Ces outils trouvent leur principale utilité lors de la définition, avant de commencer la programmation à proprement parler, d’un cahier des charges de ce que l’algorithme ou le programme doivent pouvoir faire. « Les méthodes formelles permettent de vérifier si on ne commet pas d’erreur à ce moment critique, précise Philippe Schnoebelen. Car si l’on en fait aussi tôt dans le processus, on risque de s’en rendre compte seulement après avoir déjà tout codé et de devoir reprendre la programmation de zéro. »

Ces travaux sont issus d’une forte émulation et collaboration entre les co-auteurs, qui étaient à l’époque tous membres du Laboratoire spécification et vérification (LSV), aujourd’hui fusionné au sein du LMF afin d’accompagner le développement des méthodes formelles en France. Philippe Schnoebelen a ainsi dirigé la thèse de doctorat de François Laroussinie, puis ils ont tous deux encadré celle de Nicolas Markey.

Ces liens ont permis de faire naître un article dont la clarté et l’élégance ont été mises en avant par le jury. « LICS est la conférence phare des méthodes formelles et je me reconnais tout à fait en elle, souligne Philippe Schnoebelen. Je suis donc très heureux que notre article ait été récompensé vingt ans plus tard, bien que j’ai entre-temps changé de sujet de recherche. »

Philippe Schnoebelen s’est en effet orienté, toujours dans les méthodes formelles, sur l’étude des systèmes infinis et ceux dits bien structurés. François Laroussinie et Nicolas Markey continuent quant à eux de développer la logique temporelle, par exemple en l’associant à la théorie des jeux dans des systèmes multi-agents où les participants ont des objectifs en partie antagonistes.