Bonjour,
Nous proposons une offre de contrat de thèse de doctorat en représentation des connaissances et formalisation du raisonnement au Centre de Recherche en Informatique de Lens (CRIL) pour démarrer en septembre 2018.
L’équipe d’encadrement est composée par :
– Fahima Cheikh-Alili (http://www.cril.univ-artois.fr/~cheikh/)
– Jean-François Condotta (HDR) (http://www.cril.univ-artois.fr/~condotta/)
– Ivan Varzinczak (http://ijv.ovh)
Nous invitons les candidats à nous envoyer par e-mail (cheikh@cril.fr, condotta@cril.fr, varzinczak@cril.fr) leur dossier de candidature composé de :
– CV
– Lettre de motivation
– Relevé de notes du M1 et du M2
La date limite pour l’envoie du dossier est le lundi 28 mai 2018 à midi (heure de Paris).
Ci-dessous vous trouverez plus de détails sur le sujet de thèse proposé.
** Sujet de thèse de doctorat **
* Titre :
Defeasible Temporal Logic pour la spécification et la vérification des systèmes tolérants aux exceptions
* Descriptif :
La spécification et la vérification des systèmes informatiques ayant un comportement dynamique sont des tâches toujours importantes, compte tenu du nombre de plus en plus grand des nouvelles technologies informatiques qui sont conçues. Comme exemples récents, on peut citer la technologie blockchain et les différents outils existants pour la domotique ou encore les différentes chaînes de production prévues par l’Industrie 4.0. Par conséquent, il est fondamental de s’assurer que des systèmes basés sur ceux-ci ont le comportement désiré mais, surtout, satisfont des normes de sécurité de plus en plus exigeantes. Cela devient encore plus critique avec le déploiement croissant de techniques d’intelligence artificielle ainsi que le besoin d’expliquer leurs comportements.
Plusieurs approches pour l’analyse qualitative des systèmes informatiques ont été développées. Parmi les plus fructueuses, on peut citer les différentes familles de logiques temporelles. Le succès de celles-ci est dû principalement à leur syntaxe simplifiée (comparée à celle de la logique du premier ordre), leur sémantique intuitive, basée sur les systèmes de transitions et les automates, leurs bonnes propriétés de calcul, et au fait qu’elles soient plus facilement implémentables. Cela est confirmé par l’existence de plusieurs outils basés sur ces logiques.
Malgré le succès et la large utilisation des logiques temporelles, celles-ci restent limitées pour la modélisation et le raisonnement à propos des aspects réels des systèmes informatiques ou de ceux qui en dépendent. En effet, les systèmes informatiques ne sont pas soit 100 % sûrs soit 100 % défectifs, et les propriétés qu’on souhaite vérifiées peuvent avoir des exceptions anodines et tolérables, ou au contraire, des exceptions devant être soigneusement traitées afin de garantir la fiabilité générale du système. De même, le comportement espéré d’un système peut s’avérer correct non pas pour toute execution possible, mais plutôt pour ses executions les plus normales ou probables. De plus, des exceptions prévues à l’avance par le concepteur peuvent, elles aussi, en avoir des cas exceptionnels.
Il se trouve que les logiques temporelles, du fait qu’elles soient des formalismes logiques du type dit classique, c’est-à-dire, dont le raisonnement sous-jacent est celui des mathématiques et pas celui du sens commun, ne permettent pas du tout de formaliser les différentes nuances des exceptions et encore moins de les traiter. Techniquement la raison étant que ces logiques-là (1) au niveau de propositions, sont souvent basées sur deux valeurs de vérité (vrai ou faux), (2) au niveau du langage objet (celui des symboles logiques), ont des opérateurs se comportant de manière monotone, et (3) au niveau du raisonnement, possèdent une notion de conséquence logique qui, elle aussi, est monotone et, par conséquent, n’est pas adaptée à l’évolution des faits déductibles.
Le raisonnement dit non monotone, permettant de formaliser et de raisonner avec des exceptions et le dynamisme de l’information, a été largement étudié par la communauté en IA depuis bientôt 40 ans. Cependant, les contributions majeures dans ce domaine se limitent au cadre propositionnel, donc peut expressif pour les tâches ci-dessus. Ce n’est que récemment que certaines approches pour le raisonnement non monotone, comme la circonscription, les règles par défaut et les approches préférentielles, ont été étudiées pour des logiques plus expressives que la logique propositionnelle, notamment les logiques modales et de description, mais dans des cadres autres que celui de la spécification et la vérification. Le pont entre les formalismes temporels pour la spécification et la vérification des systèmes informatiques et les différentes approches pour le raisonnement non monotone, permettant de résoudre de façon satisfaisante les limitations soulevées ci-dessus, reste à bâtir. Celui-ci est l’objectif général de ce sujet de thèse de doctorat.
* Connaissances requises :
– Logique propositionnelle et du premier ordre
* Compétences techniques à développer pendant la thèse :
– Logique modale
– Logiques temporelles
– Approches pour le raisonnement non monotone
– Théorie des modèles et théorie de la preuve liées aux formalismes ci-dessus
Bien cordialement,Ivan