Home - English version - Publications - Séminaire Thésard - Divers

Programme séminaire thésard

Le séminaire thésard est destiné en priorité aux thésards, les orateurs étant aussi des thésards.

L'objectif est de présenter des introductions aux différents domaines de recherches, a contrario des groupes de travails qui sont souvent pointus dans leur spécialités. L'ensemble des thésards n'étant pas souvent au fait des techniques utilisées par ses voisins de bureaux, ce séminaire a pour but de présenter différentes problèmatiques des laboratoires PPS et LIAFA.

Planning du séminaire thésard

Les séminaires thésard ont lieu sauf cas exceptionnel, dans le sous-marin(salle 6A92) à 11h, les mercredis matins.

Mercredi 1er Mars
Laura Chaubard
Produit en couronne de C-variétés

"Lors de l'épisode précédent, nous avions introduit la toute récente théorie des C-variétés. Ces nouvelles variétés, initiées par Straubing, permettent de généraliser et d'unifier la théorie d'Eilenberg en classifiant les langages selon les propriétés de nouveaux invariants syntactiques. Le principe du produit en couronne est un outil classique sur les monoïdes, caractérisant les langages reconnus par des fonctions séquentielles. Après avoir rappelé les motivations et les premières définitions de la théorie des C-variétés, nous exposerons la généralisation du principe du produit en couronne et ses applications."

Mercredi 1er Février
Samy Abbes
Structure d'événements probabilistes

On introduit une definition formelle de structure d'evenements probabilistes. L'interet est de disposer d'un modele probabiliste de concurrence sous une semantique d'ordres partiels, contrairement aux modeles classiques qui analysent la semantique d'entrelacement. Pour une modelisation de systeme distribue, il est normal d'exiger, informellement, que des processus concurrents soient statistiquement independants. On donne des conditions sous lesquelles on peut satisfaire cette exigence

Mercredi 18 Janvier
Joachim Delataillade
Sémantique des jeux.

La sémantique des jeux, c'est comme Nicolas Sarkozy : on n'entend parler que de ça, et pourtant on a l'impression que ça ne sert à rien à part à dire des conneries. Eh bien c'est faux (dans le cas de la sémantique des jeux tout du moins) ! Mon exposé, après vous avoir présenté les bases de la sémantique des jeux, vous montrera comment elle interprète de façon simple et précise le lambda-calcul (ainsi que le lambda-mul-calcul, et pas mal d'autres mets-ta-photo-ici-calculs), comment elle permet d'introduire des idées nouvelles en logique, et enfin comment elle permet de s'attaquer sans vergogne à des questions purement syntaxiques, comme par exemple le problème (crucial ?) des isomorphismes de types. Je parlerai aussi du second ordre (système F), histoire de rire un peu.

Mercredi 4 janvier 2006
Pierre Moro
Compteurs, automates, et abstraction

Apres avoir presente le principe d'abstraction-verification-raffinement utilise en regular model checking, je presenterais comment l'arithmetique de presburger peut etre representee via des automates. A partir de ces 2 principes, je presenterais des fonctions d'abstractions sur des automates representant des formules de presburger, et comment tous ces elements reunis ensemble permettent de verifier des programmes a compteurs. Je parlerais ensuite des problemes majeurs de cette approche (comparee aux autres) et quelles sont les possibles solutions a ces problemes.

Vendredi 2 Décembre
Emmanuel Beffara
Logique, réalisabilité et concurrence

Cette thèse se consacre à l'application de techniques de réalisabilité dans le cadre de l'étude du sens calculatoire de la logique. Dans une première partie, nous rappelons le formalisme de la réalisabilité classique de Krivine, dans lequel nous menons ensuite une étude du contenu opérationnel de tautologies purement classiques. Cette exploration du sens calculatoire de la disjonction classique révèle des comportements riches, avec une forte intuition interactive, qui s'interprètent avantageusement comme des structures de contrôle typées. Afin de mieux comprendre la nature de ces mécanismes, nous définissons ensuite une technique de réalisabilité à la Krivine pour un modèle de calcul concurrent, dans le but d'obtenir une notion de constructivité qui ne soit plus fondée sur l'idée de fonction, mais sur celle de processus interactif (si vous comprenez qque chose jusqu'ici c'est que vous travaillez a pps). Le cadre ainsi obtenu donne une interprétation réellement concurrente de la logique linéaire dans un calcul de processus dérivé du pi-calcul, permettant d'appliquer au cas concurrent la méthode de spécification précédemment étudiée dans le cas séquentiel. Par la suite, l'étude des traductions de la logique classique vers la logique linéaire mène à reconstruire systématiquement des décompositions interactives du calcul fonctionnel, permettant ainsi de faire le lien au niveau logique entre les réalisabilités classique et concurrente. Dans une dernière partie, nous étudions plus en détail le mode de calcul issu des algèbres de processus, afin de comprendre son système d'ordonnancement. Cette étude mène à la définition d'un modèle de calcul plus géométrique qui permet une exploration formelle de la notion de causalité dans les calculs concurrents.

Mercredi 16 novembre
Emmanuel Beffara
Logique, réalisabilité et concurrence

Cette thèse se consacre à l'application de techniques de réalisabilité dans le cadre de l'étude du sens calculatoire de la logique. Dans une première partie, nous rappelons le formalisme de la réalisabilité classique de Krivine, dans lequel nous menons ensuite une étude du contenu opérationnel de tautologies purement classiques. Cette exploration du sens calculatoire de la disjonction classique révèle des comportements riches, avec une forte intuition interactive, qui s'interprètent avantageusement comme des structures de contrôle typées. Afin de mieux comprendre la nature de ces mécanismes, nous définissons ensuite une technique de réalisabilité à la Krivine pour un modèle de calcul concurrent, dans le but d'obtenir une notion de constructivité qui ne soit plus fondée sur l'idée de fonction, mais sur celle de processus interactif (si vous comprenez qque chose jusqu'ici c'est que vous travaillez a pps). Le cadre ainsi obtenu donne une interprétation réellement concurrente de la logique linéaire dans un calcul de processus dérivé du pi-calcul, permettant d'appliquer au cas concurrent la méthode de spécification précédemment étudiée dans le cas séquentiel. Par la suite, l'étude des traductions de la logique classique vers la logique linéaire mène à reconstruire systématiquement des décompositions interactives du calcul fonctionnel, permettant ainsi de faire le lien au niveau logique entre les réalisabilités classique et concurrente. Dans une dernière partie, nous étudions plus en détail le mode de calcul issu des algèbres de processus, afin de comprendre son système d'ordonnancement. Cette étude mène à la définition d'un modèle de calcul plus géométrique qui permet une exploration formelle de la notion de causalité dans les calculs concurrents.

Abstract des anciens orateurs, Transparents

Mercredi 16 novembre
Anne Gwenn Bosser
"Réplications Distribuées pour la Définition des Interactions de Jeux Massivement Multi-Joueurs"

Les Jeux Massivement Multi-Joueurs sont des applications distribuées sur Internet dans lesquels on retrouve des problématiques de persistance, de sécurité, de temps-réel, de passage à l'échelle, et d'utilisation critique des ressources des machines et du réseau. Nous proposons un cadre pour la réalisation de telles applications afin de favoriser la réalisation de game-play innovants en permettant une mise au point très fine des interactions. Nous décrivons les techniques actuelles et démontrons comment chaque solution pour la réalisation d'une interaction donnée est fortement liée à la description fonctionnelle de cette interaction dans le cadre du game-play considéré. Notre proposition consiste en un outil de prototypage basé sur un framework doté d'une sémantique simple pour faciliter le développement, mais permettant de gérer très finement les ressources bas-niveau afin de ne pas manquer de généricité. L'outil est destiné à être utilisé dans un cadre réaliste de méthodologie de développement basée sur le raffinement successif de prototypes permettant de valider au plus tôt les choix techniques. Nous présentons le framework que nous avons développé, qui définit un modèle de réplication des données représentant le monde virtuel le long de l'application distribuée. La sémantique utilisée repose sur un modèle d'exécution coopératif et reproductible, dont nous donnons la formalisation des principaux traits sous une forme opérationnelle. Nous décrivons l'organisation du code produit, ainsi que la manière dont le framework s'inscrit dans notre proposition finale et détaillons un exemple complet pour illustrer son utilisation.

Mercredi 2 novembre
Caroline Priou
Séparabilité dans un lambda calcul non-déterministe

Nous rajoutons au lambda calcul standard un opérateur de choix + et une réduction non-déterministe associée, afin d'obtenir un lambda calcul non-déterministe, d'après le travail de U. de'Liguoro et A. Piperno. Nous explorerons ensuite la sémantique opérationnelle de ce calcul, en étendant la notion d'arbre de Bohm et d'approximant, et en étudiant la convergence de type "must" des termes. Quelques techniques de séparabilité classiques adaptées à nos nouveau termes puis le résultat de semi-séparabilité seront présentés.

Mercredi 19 Octobre
Mathias Samuelides
Tree Walking automates utilisant des jetons.

Un Tree-Walking-Automate (TWA) se déplace sur un arbre donné en choisissant chaque mouvement en fonction de l'état courant et du noeud de l'arbre où il se trouve. Nous étudions des TWA utilisant des jetons numerotés de 1 a k qui leur servent de repères dans l'arbre. Un tel automate ne peut poser un jeton i que si les jetons ji ne sont pas posés dans l arbre. Nous considérons deux modèles de TWA avec jetons. Dans le modèle fort l'automate peut retirer le dernier jeton quelle que soit la position de sa tête de lecture. Dans le modele faible l'automate peut retirer le dernier jeton seulement si sa tête de lecture est sur le noeud ou le jeton est posé. Je vais montrer que ces deux modèles sont équivalents dans le cas non-déterministe puis dans le cas déterministe. Pierre

Mercredi 5 Octobre
Samuel Hym
Le vrai lettregrecque-calcul, version répartie

Depuis la nuit des temps (le 1er janvier 1970), l'homme aimerait pouvoir modéliser les programmes écrits par des informaticiens bourrés de bière et de pizza pour éviter le crash de son avion. On présentera dans ce cadre le π-calcul introduit au début des années 90 par Milner, Parrow et Walker, devenu depuis la référence en matière de calcul de processus. Ce calcul a introduit une notion de mobilité. On exposera une extension répartie, appelée Dπ, idéale pour la modélisation des « applications nomades ». Nous montrerons enfin pourquoi et comment le typage sauvera le monde. Si si.

Mercredi 22juin
Sylvain Lebresne
Polynomes chromatiques

De tout temps, l'homme a cherché à calculer des polynômes chromatiques de graphe. En effet, pour un graphe donné G, un tel polynôme (P_G(x)) nous donne le nombre de façons de x-colorier ce graphe, ce qui est bien. Devant l'engouement succité par ce polynôme dans la communauté scientifique, nous nous sommes intéressés à son calcul, problème d'autant plus intéressant que dur (déterminer les coefficients de ce polynôme pour un graphe quelconque a récemment été montré #P-hard; je ne sais pas exactement ce que ca veut dire, mais ça fait peur). Dans cette présentation, nous tenterons d'expliquer, à grand renfort de jolis dessins, l'algorithme que nous avons developpé pour ce calcul et expliquerons les notions sur lesquelles celui-ci s'appuie (graphes triangulés, arbre de cliques, théorie de la relativité ...).

Mercredi 8juin
Julien Dorso
Analyse d'automates hybrides
L'informatique embarquee est omnipresente de nos jours. A mesure que les systemes deviennent plus complexes, les concepteurs, et les utilisateurs, rencontrent des problemes et des erreurs de plus en plus difficiles a cerner et corriger. La verification a pour but de rendre possible l'analyse d'un programme ou systeme, par rapport a sa specification, et soit de trouver les erreurs du systeme, soit de prouver qu'il est correct. La technique dite du "Model Checking" cherche a rendre la verification automatique, par le biais d'algorithmes. Dans cet expose, j'introduirai la notion de systeme hybride, ainsi que la notion d'automate hybride, le formalisme utilise pour modeliser ces systemes. Je decrirai des problemes interessants pour ces systemes. Finalement, je parlerai de RVA's, une representation d'ensembles de reels basee sur les omega-automates.

Mercredi 25 Mai
Stephane Lengrand

Adam Rogalewicz:
Abstract regular tree model checking
Abstract regular tree model checking (ARTMC) is a generalization of abstract regular model checking proposed. This method allow us to verify programs with tree-like structure of states. Program configuration is encoded as a tree, set of such configurations as a tree automaton, and a program behaviour as a tree transducer. ARTMC allow us to compute an overapproximation of set of all reachable configurations. We are interested in use of this method for verification of programs with pointers.

Mercredi 11 Mai
Laura Chaubard
Théorie des C-variétés
transparents
Devant le nombre grandissant d'applications relevant de la théorie des variétés d'Eilenberg, ce cadre s'est révélé parfois mal adapté. Les C-variétés, introduites récemment par Straubing, permettent une généralisation et une unification de la théorie d'Eilenberg (cadre algébrique permettant de considérer les classes de languages fermées par opérations boolèennes, résiduels et morphismes inverses). Cette nouvelle théorie trouve de nombreuses applications dans divers domaines tel que la complexite des circuits, la logique temporelle, la dynamique symbolique... Le but de cet exposé sera avant tout de motiver l'introduction des C-variétés par des exemples de problèmes et de classes de langages pour lesquels la théorie d'Eilenberg ne peut être utilisée. Nous introduirons pour cela la théorie des variétés, puis exposerons la généralisation que représentent les C-variétés. Enfin, nous présenterons les derniers resultats de cette nouvelle théorie.

Mercredi 27 Avril
Benjamin Leperchey
Programmes et contextes: exhibitionnistes et voyeurs
Un programme n'a de sens que dans un contexte global: il peut faire appel a des fonctions de bibliotheques externes, ou utiliser des entrees/sorties. Chaque contexte correspond a une facon d'utiliser le programme, et en cela un contexte est une observation. On peut alors se demander ce qu'on peut ou ne peut pas observer, et donc dans quel mesure deux termes sont interchangeables. L'approche operationnelle est souvent assez peu pratique. La semantique denotationnelle est plus simple, mais moins precise: les modeles contiennent des observations qui ne sont pas permises. On essaiera de montrer en quelques exemples la difference entre les notions d'observations syntaxique et denotationnelle.

Mercredi 13 Avril
Claire David
Logique et données infinies
transparents
On étudie depuis longtemps les langages de mots (écrit sur un alphabet fini de lettres). On sait décrire des languages de mots de plusieurs manières (automates, logique classique, logique temporelle, semi-groupes, grammaires ...). Ici, je m'intéresse à un autre type de mots: des mots avec données. Un mot avec données est un mot où chaque position contient en plus de la lettre provenant d'un alphabet fini et une donnée provenant d'une structure infinie dans laquelle, on ne sait tester que l'égalité. Pourquoi ce type de mots? La motivation vient du langage XML qui manipule des données non-bornées. On peut aussi voir des applications dans la modélisation de systèmes distribués qui peuvent contenir un nombre arbitraire de processus . (Les données pourraient servir à identifier les processus.) On cherche à obtenir des caractérisations intéressantes de tels langages de mots (le but étant ensuite de passer aux langages d'arbres avec données). Pour tenir compte des données, on augmente la logique classique du premier ordre avec un test d'égalité sur les données. Le but de mon exposé est de vous donner des idées de ce que l'on peut faire avec cette logique. Quelles propriétés peut-on exprimer ? Comment la restreindre pour avoir des fragments décidable? Enfin, je parlerai un peu d'automates.

Mercredi 30 Mars
Anne-Gwenn Bosser
Un cadre pour la mise au point des interactions dans les jeux persistants massivement multi-joueurs
Les jeux massivement multi-joueurs sur internet sont une tendance lourde de l'industrie du jeu vidéo. Cependant, ce sont aussi les applications qui ont mené au plus grand nombre de banqueroutes: sécurité, temps réel, bande passante, CPU, tous ces aspects sont critiques pour la réalisation de tels jeux. En particulier, la qualité des interactions entre les joueurs et le monde virtuel est très difficile à mettre au point avant la phase trop tardive du beta-test. On présentera les problématiques techniques ainsi que les domaines de recherche actuels pour aider à la réalisation de telles applications. On montrera qu'aucune des approches software actuelles ne résout ces problèmes de manière satisfaisante. Ensuite, on développera notre proposition d'environnement de développement dédié, en justifiant de son adéquation avec les processus de développement modernes que sont les méthodes agiles. On presentera finalement le Fill-In-The-Gap framework, sur lequel un futur environnement de développement se basera. Ce framework est de la famille des framework ouverts, et vise à mettre en avant les points critiques et à faciliter leur résolution plutôt que de faire des choix techniques génériques limitant le choix des qualités des interactions et donc les game-designs possibles.

Mercredi 23 Mars, Attention séance exceptionnelle, 2 exposés, début de la séance à 10h, café et jus d'orange prévus !
Antoine Meyer
Graphes rationnels

The general context of this talk is the study of families of infinite graphs with a finite description, their links to language theory and their structural properties. This particular work presents a link between rational graphs and context-sensitive languages. Rational graphs are infinite graphs whose vertices are words, and whose edge relations are defined using transducers. Context-sensitive languages are a family of formal languages accepted by Turing machines working in linear space. We will try to show as simply and intuitively as possible that context-sensitive languages coincide with the languages of rational graphs (i.e. the set of path labels between given sets of initial and final vertices, "automata-style"). This is joint work with Arnaud Carayol from Rennes. Suivi de Vince Barany (Aachen University of Technology)
Automatic Structures
abstract

Mercredi 9 Mars
Alexandre Miquel
Réalisabilité et extraction de programmes
Vous savez prouver qu'il existe un entier x satisfaisant une propriété P(x), mais vous ne savez pas explicitement lequel ? Vous savez prouver que tout entier x est en relation avec un entier y (pour une relation R(x, y) donnée), mais vous ne savez pas calculer explicitement y en fonction de x ? Dans cet exposé, je me propose de dévoiler un bout du mystère de la « déraisonnable efficacité des mathématiques » (E. Wigner) en vous montrant comment les techniques dites de réalisabilité permettent d'extraire un *programme* calculant un entier ou une fonction des entiers dans les entiers à partir d'une *preuve* de son existence. Après avoir rappelé le cadre - la correspondance de Curry-Howard - et les origines tourmentées - l'intuitionnisme Brouwérien -, j'essaierai d'expliquer les idées de base de la réalisabilité et de l'extraction de programmes à la lumière de quelques exemples, tout en soulignant les limites que rencontre inévitablement un tel exercice.

Mercredi 23 Février
Hugo Gimbert
Jeux Positionnels
La notion de jeux est utilisée pour modéliser des situations où plusieurs agents interagissent via un système, en tentant de maximiser leur intérêt propre. Dans cet exposé, on s'intéressera aux jeux à information parfaite, qui correspondent aux cas où les joueurs jouent à tour de rôle et connaissent à tout instant l'état exact du système. Pour jouer, les joueurs utilisent des stratégies, qui leur indiquent quel coup jouer en fonction des coups déjà joué depuis le début de la partie. Les stratégies positionnelles sont des stratégies particulièrement simples où le coup conseillé ne dépend que de l'état courant du système. Les jeux les plus classiques en informatique théorique sont des jeux à deux joueurs dont les intérêts sont totalement opposés. Une stratégie qui maximise le revenu d'un joueur est dite optimale. On caractérisera les cas où les deux joueurs possèdent des stratégies optimales positionnelles, et on donnera des exemples. Les jeux à plus de deux joueurs suscitent actuellement un regain d'intérêt dans la communauté. Dans ce cadre, les intérêts des joueurs ne sont plus nécessairement opposés, et l'existence de stratégies optimales n'est plus assurée. On s'intéresse alors aux situations où aucun joueur n'a intérêt à modifier unilatéralement sa stratégie. Ces situations sont appelées équilibres de Nash. On présentera quelques résultats d'existence d'équilibres de Nash positionnels.

Mercredi 9 Février
Vincent Balat
Implémentation de l'évaluation partielle dirigée par les types.

Mon exposé sera une introduction à la technique d'évaluation partielle dirigée par les types (TDPE). Je décrirai notamment une implémentation de cette technique pour le langage Objective Caml. L'évaluation partielle désigne une transformation de programmes visant à en construire des versions spécialisées pour certains paramètres. D'un point de vue théorique, cette réduction de programme correspond à la notion de réduction forte (normalisation). La normalisation par évaluation est un algorithme particulièrement ingénieux pour réaliser cette tâche, qui a été utilisé dans plusieurs domaines (théorie des types, catégories, logique...) Un algorithme d'évaluation partielle reprenant les mêmes idées, appelé TDPE (Type Directed Partial Evaluation), a été présenté par Olivier Danvy. Cependant l'implémentation concrète de TDPE pose de nombreux problèmes, dont beaucoup ne sont pas encore résolus aujourd'hui. J'essaierai de vous montrer les différents aspects de ce problème en me basant sur mon expérience d'implémentation de TDPE pour le langage Objective Caml.

Mercredi 26 Janvier
Pierre Moro
Transparents
«Abstract Regular Model-Checking»
Après avoir présenté le principe du modèle checking, nous allons parler des solutions qui ont été apportées pour les problèmes manipulant des programmes où le nombre de configurations possible est trop grand pour être calculable (on parle de model checking infini). Nous allons d'abord présenter le regular model checking, représentation par des automates de problème du model checking infini. Ensuite nous allons présenter une technique d'accélération : abstract regular model-checking, permettant d'éviter les erreurs inhérentes aux accélérations en général. Nous allons enfin présenter un exemple d'application de cette dernière méthode. Nous nous intéresserons aux programmes manipulant des listes chaînées, à son encodage dans le cadre du regular model checking, ainsi qu'à des méthodes d'abstraction générales, et leur application dans ce cadre.

Mercredi 19 Janvier
Florian Horn
«Jeux de Streett.» Transparents

Les jeux de Streett sont un modéle efficace pour la gestion de ressources non-vitales. De nombreux algorithmes permettent la détermination des stratégies et des régions gagnantes pour de tels jeux. Dans un premier temps, nous allons présenter les définitions et les algorithmes classiques permettant de résoudre le problème de la détermination de ces stratégies. Nous allons ensuite présenter d'autres algorithmes déjà existant dans la littérature, mais sous une forme simplifiée et compréhensible. Nous montrerons une borne inférieure de mémoire du problème, qui complète la preuve d'optimalité des algorithmes précédents.

Mercredi 8 Décembre
Michel Hirschowitz
Transparents
«Les jeux zolympiques»

Le but de cette thèse est de mettre en évidence une nouvelle notion de jeux qu'on appellera jeux d'équipe, en extrayant l'essence de la notion de jeux conçue par Hyland et Ong. La sémantique des jeux est apparue dans les années 90 et a permis de modéliser de nombreux traits non fonctionnels de langages de programmation. La sémantique des jeux est une sémantique satisfaisante à la fois d'un point de vue opérationnel, puisqu'elle décrit les transitions entre états de l'environnement d'un programme, et d'un point de vue dénotationnel puisqu'elle traduit la signification du programme et qu'elle présente cet aspect compositionnel qui permet notamment de comprendre un programme en analysant ses sous-programmes mais aussi de prouver des équivalences. Cependant certains rouages de la sémantique de jeux ne sont pas totalement satisfaisants d'un point de vue mathématique. Notamment la composition des stratégies met en jeu une combinatoire rébarbative qui laisse à penser qu'on peut en donner une définition plus structurelle. Tout le monde pense aussi que les pointeurs des jeux HO n'ont pas un statut très clair par rapport à la composition. Un jeu d'équipe généralise les notions usuelles de positions, coups, parties et stratégies en leur donnant une interprétation géométrique. Parmi les positions on distinguera les positions perdantes des positions gagnantes alors que parmi les stratégies on distinguera les stratégies gagnantes et les stratégies déterministes. La composition, qui permet à deux joueurs de combiner leurs stratégies respectives pour se partager un but en deux objectifs complémentaires, constitue l'attrait principal d'un jeu d'équipe. Notre composition de stratégies a un élément neutre et vérifie la condition habituelle d'associativité. De plus les propriétés du type gagnant ou déterministe sont préservées à travers cette composition. Pour rendre ce travail cohérent je me devais de donner un jeu d'équipe pour les jeux HO totaux, dans lequel les objets sont les parties dans une arène donnée. Les travaux futurs consistent à donner une définition de la logique sous cette nouvelle forme de jeu qui met mieux en relief ses symétries. Le théorème de composition des stratégies gagnantes donne dans ce cadre une nouvelle forme de l'élimination des coupures.

Mercredi 24 Novembre
Thu Ha Dao Thi
Transparents
«Files 0-automatiques et réseaux»

Files d'attente et reseaux à forme de produit ont bcp d'applications dans le domain des réseaux de télécommunication. Un G-network est un réseau qui contient des clients négatifs et à la forme produit. Dans mon exposé, je vais vous presenter les définitions des files d'attente, réseau de Jackson et G-network. Dans la suite, un réseau associé à une paire 0-automatique, soit une autre facon d'incorporer les clients negatifs, va être presentée. Mon but est d'étudier la condition de stabilité, si le réseau à la forme produit. Le nouveau réseau a la forme produit sous certaines conditions, mais les resultats obtenus ont encore besoin d'être ameliorés.

Mercredi 10 Novembre
transparents
Fabien Tarissan
Étude des modèles concurrents appliqués aux systèmes biologiques
Les avancées technologiques qui ont accompagné l'évolution de la biologie à la fin du siècle dernier ont amené la communauté des biologistes à faire face à l'utilisation systématique de l'informatique pour traiter la masse de données obtenues. Parmi les problèmes liés à cette confrontation, celui du choix des langages de modélisation ne fait toujours pas l'unanimité. Je commencerai par passer rapidement en revue les différents formalismes qui sont utilisés dans l'étude des réseaux de régulations pour en arriver à ceux provenant de la théorie de la Concurrence (dont le pi-calcul est le principal représentant). L'intérêt de cette famille de langage est que la description syntaxique des objets donne en même temps leurs capacités d'interaction. L'inconvénient étant que dans une approche un peu brutale, l'emploi de ces formalismes reste relativement non-intuitif pour les biologistes. L'effort consiste donc à trouver un compromis entre une idéalisation suffisamment souple pour une représentation aisée des systèmes biologiques et un niveau de description assez bas-niveau pour être proche du détail moléculaire. Je terminerai la présentation par un exemple d'utilisation de l'un de ces formalismes afin de montrer précisément quel genre de phénomènes on réussit à capturer.

Vendredi 29 Octobre
Mathias Samuelides
«Complémenter un Tree-Walking-Automate deterministe »

Les Tree-Walking-Automates décrivent des ensembles d'arbres finis qui forment une sous-classe des langages d'arbres réguliers. Un Tree-Walking-Automate se déplace sur un arbre donné en choisissant chaque mouvement en fonction de l'état courant et du noeud de l'arbre où il se trouve. Un run de l'automate sur un arbre est acceptant si il termine a la racine dans un état final. Je montrerai comment a partir d'un Tree-Walking-Automate déterministe donné qui reconnait un ensemble d'arbres finis de rang borné on peut construire un Tree-Walking-Automate déterministe qui reconnait le meme ensemble d'arbres et dont tous les runs sont finis. Un Tree-Walking-Automate déterministe dont tous les runs sont finis se complémente ensuite en remplaçant les états finaux par les états non-finaux. J'expliquerai enfin comment utiliser cette méthode pour les Tree-Walking-Automates sur des arbres de rang non borné déterministes et sur des k-Pebbles-Tree-Walking-Automates déterministes (Tree-Walking-Automates déterministes utilsant k jetons).

Jeudi 14 Octobre
transparents
Emmanuel Beffara
« Logique de la programmation concurrente. »
Une bonne part de l'approche actuelle de la sémantique de la programmation se fonde sur l'isomorphisme de Curry-Howard, qui établit une correspondance très forte entre logique (formules, démonstrations, élimination des coupures) et programmation (respectivement: types, programmes, évaluation). Après avoir rappelé un peu plus formellement l'idée de cette correspondance, dans le cadre initial de la logique intuitionniste et de la programmation fonctionnelle (i.e. le lambda-calcul, pour les amateurs de lettres grecques), je tâcherai d'expliquer comment elle peut s'étendre à une correspondance entre le calcul concurrent (avec l'exemple du pi-calcul, pour rester héllénique) et diverses logiques, notament la logique linéaire et éventuellement des logiques spatiales. On peut espérer tirer de cette extension des choses intéressantes sur les rapports entre programmation séquentielle et concurrente, ou encore de nouvelles forme de typage et de spécification pour les processus concurrents.

Pierre Moro
Last modified: Fri Mar 3 14:31:09 CET 2006