Karoliina Lehtinen, logique et théorie des automates
Karoliina Lehtinen a rejoint le Laboratoire d'Informatique et Systèmes (LIS - CNRS/Aix-Marseille Université) en 2020 en tant que chargée de recherche CNRS.
Quel est votre domaine de recherche ?
Karoliina Lehtinen : Mes principaux intérêts de recherche sont la logique, les jeux et la théorie des automates, en particulier dans le contexte de la vérification et de la synthèse. Plus précisément, je m'intéresse aux différentes représentations de spécifications. Certains formalismes ont de meilleures propriétés algorithmiques que d'autres, mais peuvent nécessiter une formule ou un automate beaucoup plus grand pour décrire le même langage. Un des enjeux principaux de ma recherche consiste à comprendre ces compromis afin de faire des meilleurs choix de représentation dans les protocoles de vérification.
En général, je travaille avec des formalismes reconnaissant des langages réguliers et hors-contexte sur des mots et arbres finis ou infinis, tel que le mu calcul modal, LTL, les automates de parité, ainsi que les jeux que l’on retrouve dans les problèmes de vérification et de synthèse de ces formalismes.
Qu’avez-vous fait avant d’entrer au CNRS ? Pourquoi avoir choisi le CNRS ?
K. L. : J'ai étudié au Royaume-Uni, d'abord à Cambridge puis à Edimbourg, où j'ai obtenu mon doctorat en mu calcul avec Julian Bradfield. J'ai ensuite travaillé deux ans en tant que post-doc à Kiel, en Allemagne, dans le groupe Systèmes Fiables de Dirk Nowotka, ponctués de quelques mois à Herzeliya, en Israël, où j'ai travaillé avec Udi Boker. En 2019, j'ai déménagé à Liverpool pour rejoindre Sven Schewe dans le groupe Vérification où j'ai également travaillé sur une bourse Marie Skłodowska-Curie.
Compte tenu du poids de la communauté automates et langues formelles en France, postuler au CNRS me convenait tout naturellement.
Qu’est-ce qui vous a amené à faire de l’informatique et/ou des sciences du numérique ?
K. L. : Au lycée, je me suis dit que, puisque je ne connaissais rien à l'informatique, ce serait une bonne idée de l'étudier à l'université. C'est la théorie de la calculabilité en première année qui m'a convaincu que j'avais eu raison.