Trois chercheurs récompensés pour leurs travaux sur la logique temporelle
Vingt ans après la publication d’un article sur la logique temporelle, Philippe Schnoebelen du LMF, François Laroussinie de l'IRIF et Nicolas Markey de I'Institut de recherche en informatique et systèmes aléatoires (IRISA, CNRS/Université de Rennes 1 ) ont été récompensés par la conférence LICS, qui fait référence en logique informatique. Ces travaux ont ouvert la voie à l’expression d’événements passés dans la logique temporelle et les méthodes formelles.
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 past 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.