Description

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 exécution possible, mais plutôt pour ses exécutions 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 le stage :

  • 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

Références (non exhaustives) :

  1. O. Arieli and A. Avron. General patterns for nonmonotonic reasoning : From basic entailments to plausible relations. Logic Journal of the IGPL. Volume 8, Pages 119-148. 2000.

  2. M. Ben-Ari. Mathematical Logic for Computer Science. 3rd edition. Springer-Verlag. 2012.

  3. J. van Benthem. Modal Logic for Open Minds. Center for the Study of Language and Informa- tion. 2010.

  4. D. Harel and J. Tiuryn and D. Kozen. Dynamic Logic. MIT Press. 2000.

  5. D. Makinson. Bridges from Classical to Nonmonotonic Logic. King’s College Publications. Volume 5 in Texts in Computing. 2005.

  6. D. Makinson. How to go nonmonotonic. Handbook of Philosophical Logic, Volume 12. Pages 175-278. 2005.

  7. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Vol. I : Specification. Springer, New York, NY, 1992.

  8. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Vol. II : Safety. Springer, New York, NY, 1995.