Évènements

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).

Interval graphs arise as intersection graphs of intervals on the real line and form a natural meeting point between discrete geometry and graph theory. Their rich structure yields efficient algorithms and applications in scheduling and resource allocation. Representing graphs as intersection graphs of axis-aligned boxes in R^d extends this idea to higher dimensions; the minimum dimension required is the boxicity of the graph, introduced by Roberts in 1969. Boxicity models competition for shared resources in ecology and operations research. It also matters algorithmically: graphs of bounded boxicity inherit some of the tractability of interval graphs (for example, Maximum Clique remains polynomial-time solvable). Exploiting this, however, typically requires a box representation, and finding one is NP-hard in general. Only a few graph classes are known for which boxicity can be computed in polynomial time. To extend this list and to develop new techniques for the problem, we follow the approach of Cozzens and Roberts (1983) and study the boxicity of a graph's complement, which we call its co-boxicity. This change of perspective trades d-dimensional boxes for one-dimensional objects: the co-boxicity of a graph is the minimum number of co-interval subgraphs needed to cover its edges. We show that co-boxicity can be computed block by block from a small amount of local information. As corollaries, we obtain a fixed-parameter tractable algorithm parameterized by the size of the largest block, and polynomial-time algorithms for block graphs and cactus graphs. This talk presents joint work with Will Evans and Tao Gaede.

Réunion de plannification