IRIT - UMR 5505

L’équipe LILaC étudie des modèles formels de l’interaction, où interaction comprend à la fois des actions physiques et linguistiques (actes de langage). LILaC a adopté une approche normative, et focalise sur des modèles de la logique formelle, en intégrant :

• la sémantique du contenu des actions linguistiques (sémantique formelle),
• une logique de l’action intégrant la théorie des actes de langage,
• une théorie des états mentaux (logique épistémique, logique de l’intention),
• des théories de la structure de l’interaction : jeux de dialogue, théories formelles du discours (SDRT).

Les axes de LILaC interviennent sur les points-clés de ces modèles, avec une considération particulière pour l’aspect démonstration automatique et l’application à la sécurité.

Action et évolution des croyances

Un des aspects importants de l’interaction est la dynamique du monde, qui évolue sous le coup des évènements et actions qui eux se répercutent sur les états mentaux des agents.

Nous étudions entre autres :

• les logiques d’action telle que la logique dynamique dont nous étudions les propriétés formelles (complétude, décidabilité, complexité) ;
• la révision et la mise à jour, afin de prendre en compte de nouvelles informations, en particulier dans un cadre multi-agent (cadre qui était jusque-là exclusivement mono-agent) ;
• l’algorithmique du raisonnement sur les actions, en étudiant les propriétés formelles (consistance, modularité) de théories d’actions et d’événements (en termes de pré-, postconditions, lois du domaine, ...), ainsi que leur évolution.

Sécurité des systèmes d’information et de communication

Dans un environnement dégradé, l’interaction entre agents nécessite d’être protégée. La protection se décline sous la forme de trois propriétés : disponibilité, intégrité, confidentialité. Pour être réputé sûr, un système informatique doit être formellement spécifié et la preuve que la spécification du système vérifie les trois propriétés ci-dessus doit être fournie. La spécification et la vérification apparaissent clairement dans le contrôle d’accès et la vérification des protocoles cryptographiques.

Également, la modélisation - en termes de rôles et de relations entre utilisateurs - de l’organisation dans laquelle s’insère le système informatique permet de prendre en compte d’autres notions : confiance, responsabilité, délégation.

Au niveau du contrôle d’accès, il s’agit d’étendre le modèle de la matrice du contrôle d’accès et de tracer, pour ce qui concerne le problème de la sûreté des modèles étendus, la limite entre décidabilité et indécidabilité.

Au niveau de la vérification de protocoles, il s’agit de définir et de vérifier automatiquement des protocoles qui vont permettre à des agents de garantir la confidentialité ou l’intégrité des informations qu’ils échangent.

Au niveau des organisations, il s’agit de caractériser à la fois les aspects prédicatifs de la notion de rôle et ses aspects déontiques qui font appel aux concepts de permission et d’obligation, à la base également d’autres notions comme celle de confiance.

Langue et communication

Les modèles formels de l’interaction sont ancrés dans des réalités linguistiques ou psychologiques. Nous considérons trois problématiques :

• la modélisation de la structuration du dialogue et des textes en se focalisant notamment sur les aspects spatio-temporels du discours, en liaison avec des travaux de représentation et raisonnement dans les domaines du temps, de l’espace, du mouvement et de l’architecture. Ce travail combine l’étude du lexique associé à chacune de ces composantes à l’étude de la structure du discours dans le cadre de la SDRT, en passant par des études spécifiques en sémantique formelle ou à l’interface sémantique-pragmatique ;
• la formalisation des actes de langage, en donnant à ces actes une sémantique en termes de croyance, de but, d’intention, et d’engagement social, et en modélisant (en interaction avec des psychologues-cognitivistes) sous l’architecture cognitive ACT-R le processus d’attribution d’intention suite à l’accomplissement d’un énoncé ;
• la modélisation des émotions dans le dialogue, en faisant jouer aux émotions un rôle fonctionnel dans le domaine des interactions coopératives entre avatars tant dans la prise de décision langagière que dans les relations sociales entre interlocuteurs.

Modèles de l’interaction

Le but de l’équipe étant d’élaborer un modèle logique général de l’interaction, nous cherchons à intégrer les modèles provenant des axes 1 à 3 en un formalisme unifié, notamment aux travers :

• des logiques BDI et logiques d’action, en construisant des logiques parlant à la fois des croyances, désirs, intentions des agents, ainsi que des actions qu’ils peuvent produire (et en se focalisant sur l’évolution des croyances des agents) ;
• des jeux de dialogue et de l’argumentation, les premiers fournissant un modèle de l’interaction plus riche et flexible que les protocoles de communication, dont la seconde est un cas particulier ;
• des mécanismes sociaux, où la théorie du vote fournit un modèle d’interaction important, en particulier pour les systèmes multi-agents, et où l’utilisation de la logique permet de spécifier et vérifier ces systèmes.

Mécanisation du raisonnement pour les logiques de l’interaction

Les modèles de l’interaction qui précèdent posent des problèmes calculatoires et nécessitent la mise au point d’algorithmes permettant de répondre à des questions de type « telle formule est-elle conséquence de telle théorie logique ? » Nous avons pour cela : substantiellement renouvelé et étendu la méthode dite des tableaux ; obtenu, sur ces bases théoriques, des algorithmes complets pour un grand nombre de logiques basées sur une sémantique de Kripke ; établi un résultat général de terminaison pour des classes de ces algorithmes et, dans certains cas, mis au point des algorithmes optimaux par rapport à la classe de complexité du problème posé. Ce travail est en cours d’implémentation au travers de la plate-forme LoTREC qui offre un langage de programmation de très haut niveau pour la définition rapide de démonstrateurs pour toute logique modale normale.

Nous avons également exploré certains systèmes paraconsistants et proposé une traduction des problèmes posés en termes de formules Booléennes quantifiées.

Enfin, nous avons mis au point des algorithmes spécifiques au traitement des aspects spatio-temporels (cohérence de réseaux de contraintes du formalisme temporel qualitatif INDU ; théories spatio-temporelles qualitatives).