Séminaires

Séminaire LoCaL

Les logiques stratégiques sont une famille de logiques temporelles à temps branchant utilisées pour raisonner sur les systèmes multi-agents. L’une des plus connues est Alternating-Time Temporal Logic (ATL). La sémantique d’ATL est définie sur des structures de jeux concurrents (Concurrent Game Structures), que l’on peut voir comme des systèmes de transitions étiquetés. Chaque transition est étiquetée par un tuple d’actions et ces tuples représentent les actions choisies simultanément par les différents agents. Une stratégie pour un groupe d’agents associe à chaque état une action pour chacun des agents du groupe. Une formule d’ATL de la forme psi exprime alors le fait qu’il existe une stratégie pour la coalition d’agents A telle que, quelles que soient les stratégies choisies par les agents à l’extérieur de A, la séquence infinie d’états induite sur le système de transitions satisfait la propriété temporelle psi. La sémantique des opérateurs temporels d’ATL peut être caractérisée en termes de plus petits et de plus grands points fixes d’opérateurs décrivant localement l’évolution du système. Au niveau de la théorie de la preuve, cette structure se traduit par le caractère infinitaire des dérivations : les dérivations du calcul des séquents pour ATL sont potentiellement infinies et sont soumises à une condition globale, la progressivité. Cette condition exige que toute branche infinie d’une dérivation soit produite par l’application infiniment répétée d’une règle associée à un plus grand point fixe. Dans cet exposé, nous présenterons un tel calcul des séquents, correct et complet pour ATL. Nous nous intéresserons ensuite à l’élimination de la coupure dans ce cadre. Contrairement au cas des dérivations finies, les réductions des coupures peuvent produire une suite infinie de dérivations sans atteindre une forme normale en un nombre fini d’étapes. Nous montrerons comment définir l’élimination de la coupure comme un passage à la limite des réductions des coupures. La difficulté principale consiste alors à montrer que la dérivation obtenue à la limite satisfait toujours la condition de progressivité et constitue donc une dérivation valide.

Historiquement, l'approche franco-italo-japonais de la logique linéaire accorde beaucoup d'importance à la notion de réseaux de preuve. Celle-ci est, à son tour, basée sur un ensemble d'objets de nature calculatoire (des espèces de programmes non-typés) que l'on peut appeler des "structure de preuve non-typées". Dans l'exposé, je considérerai par parti pris les processus du pi-calcul comme des structures de preuve non-typées et non-déterministes, et je montrerai comment arriver aux réseaux de preuve d'une version de la logique linéaire avec cocontraction (mais sans coaffaiblissement ou codéreliction). S'il y a le temps, je parlerai de comment libéraliser cela pour obtenir un système de types pour le pi-calcul garnatissant l'absence de deadlock tout en permettant des processus "cycliques", habituellement exclus des systèmes de type à base de logique linéaire. Ceci est un travail en collaboration avec Juan Jaramillo et Jorge Perez (Université de Groeningen).

Réunion de plannification