• English
  • français


  • English
  • français

Séminaire

Les lundis, à partir de 14h - UPEC CMC - Salle P2-132

Contact : Luidnel Maignan

Les archives : 2012-13, 2011-12, 2010-11, 2009-10, 2008-09



Séminaires 2013-14

2014-04-07

Benjamin Hellouin (LATP, Université d'Aix-Marseille)

Caractérisation des comportements asymptotiques d'automates cellulaires

Un automate cellulaire est un système complexe défini localement, agissant uniformément et de manière synchrone sur l'espace $\mathcal A^\mathbb Z$, où $\mathcal A$ est un alphabet fini. Des simulations sur des configurations initiales tirées aléatoirement montrent que ces systèmes présentent une grande variété de comportements typiques. Nous cherchons à caractériser les comportements asymptotiques typiques de ces automates.

Formellement, partant d'une mesure de probabilité initiale simple, on considère les mesures et ensembles de mesures atteignables à la limite. Des obstructions en termes de calculabilité apparaissent naturellement sur ces ensembles. Nous montrerons, à l'aide d'une construction explicite, que ces ensembles limites sont atteignables au prix d'une hypothèse supplémentaire, obtenant une caractérisation presque complète. Suivant le temps et l'intérêt exprimés, nous examinerons diverses extensions, limites et conséquences de ce résultat.

2014-03-31

Thomas Seiller (IHES)

Graphes d'Interaction: Logique et Complexité

Je donnerai un aperçu du programme de Géométrie de l'Interaction, et en particulier mon travail sur les graphes d'interaction et son application à la théorie de la complexité. Le programme de Géométrie de l'Interaction trouve ses racines en théorie de la démonstration. Il s'agit d'une reconstruction de la logique autour de la dynamique des programmes, via la correspondance preuves-programmes.

Ce programme de recherche procure des modèles particulièrement intéressants pour l'étude de la complexité algorithmique. J'expliquerai comment ils permettent de caractériser des classes de complexité en temps et en espace, ainsi que les nouvelles méthodes et outils qu'ils procurent.

2014-03-17

Lucie Gournay et Lionel Dufaye (IMAGER - UPEC et Lisaa - UPEM)

La représentation de l'espace dans les langues naturelles : formalisations vs. modélisation linguistiques.

Pour référer à l'espace concret, on dispose selon les langues de différents types de marqueurs, comme les adverbes déictiques (cf. ici), les prépositions (cf. sur), les particules (cf. away en anglais) les verbes a priori de mouvement (cf. lever) etc. Plusieurs linguistes ont tenté de formaliser le sens de ces marqueurs, notamment les prépositions, en listant les propriétés spatiales qu'ils encodaient. Il apparaît que les formalisations se fondant sur des critères géométriques (Tyler & Evans 2001, Talmy 2002,) ou relatifs à une intuition spatiale (Vandeloise 1986, Lakoff 1987) ne sont pas satisfaisantes : soit elles encodent des données non prises en charge dans la langue, soit elles demeurent trop abstraites pour rendre compte de l'usage effectif d'un marqueur. Par exemple l'emploi de la préposition SUR en français dans une phrase comme “il y a une mouche sur le plafond” est un test montrant la défaillance des formalisations proposées, et qui se fondent sur la thèse de la primauté du spatial. Plusieurs linguistes contemporains remettent en question cette thèse de la primauté du spatial et proposent un traitement de la référence sémantique qui minimise les biais de l'interprétation intuitive. Plus particulièrement, c'est une modélisation topologique qui est proposée déduite d'une démarche hypothético-déductive qui s'appuie sur un corpus d'observables multiples. Dans la première partie de la présentation nous ferons un rappel sur la problématique, puis nous prendrons deux cas précis : * celui de la particule away en anglais et on verra que away est à même d'exprimer deux valeurs a priori contradictoires, l'une exprimant la disparition, l'autre l'intensité - ces deux valeurs a priori opposées sont explicables par un rapport entre les propriétés topologiques spatialisables et des propriétés topologiques relatives à la syntaxe propositionnelle. * celui du verbe lever en français et nous montrerons que contre l'intuition on peut rendre compte de ces usages par un ensemble de propriétés saillantes qui ne sont pas liées à la notion relative de “haut”.

2014-03-10

Ines Klimann (LIAFA - Université Paris-Diderot)

Sur la finitude des groupes et semi-groupes d'automates

Un état d'un transducteur lettre-à-lettre (automate avec entrée et sortie) peut, sous certaines conditions, induire une fonction de l'ensemble des mots sur un alphabet dans lui-même. En composant les fonctions ainsi obtenues entre elles, on peut engendrer un semi-groupe, voire un groupe.

Je commencerai par montrer la construction faite par Pierre Gillibert pour montrer que dans le cas général la finitude des semi-groupes d'automate est un problème indécidable.

La question reste ouverte dans le cas des groupes. Je montrerai quelle réponse on peut apporter pour la sous-famille des groupes engendrés par des automates inversibles-réversibles sur 2 lettres.

2014-03-03

Luidnel Maignan (LACL - UPEC)

n-Dimensional Generalized Firing Squad Solutions Using Fields

We present a solution to the Firing Squad Synchronization Problem that works both in Von Neumann and Moore neighborhood and whatever is the dimension of the space. This solution is based on fields that provide a clean modular decomposition of such cellular automata problem.

Since the entire construction is based on the one-dimensional solution, the presentation might be restricted to the one-dimensional case depending on the desire and questions of the audience.

2014-02-10

Martin Potier (LACL - UPEC)

Implémenter des niveaux d'organisation dans un langage de programmation spatiale

Dans le cadre du projet ANR Synbiotic et de la biologie synthétique, on cherche à modéliser une population de bactéries. La programmation de ces myriades d'organismes répartis dans l'espace entre exactement dans le cadre de la programmation spatiale et nous utilisons pour ce faire le langage MGS qui implémente les primitives spatiales dont nous aurons besoin. Alors que les systèmes informatiques peuvent être très compliqués (processeurs, programmes, …), les systèmes biologiques sont complexes et exhibent des propriétés « émergentes » terme certes flou, mais qui a quelques définitions concrètes. Les propriétés observées au niveau de la population sont dépendantes de l'interaction des individus de cette population, elles ne sont cependant pas facilement ou logiquement déductibles. Nous présentons ensuite une méthode constructive pour automatiquement identifier un niveau d'organisation supérieur à l'aide de la notion d'activité spatiale.

2014-02-03

Alex Borello (LACL - UPEC)

Une accélération des automates finis multitêtes oublieux par les automates cellulaires

Les automates cellulaires constituent un modèle de calcul massivement parallèle. On ne sait cependant pas si ce parallélisme lui permet d'être plus rapide, dans le cas général, qu'un modèle séquentiel. En particulier, on ne sait simuler une machine de Turing quelconque qu'avec un automate cellulaire qui, au mieux, effectue son calcul à la même vitesse ; et même avec des modèles séquentiels plus simples, comme les automates finis multitêtes (qui sont des machines de Turing à un ruban en lecture seule et avec plusieurs têtes de lecture), on ne sait pas s'il est toujours possible d'accélérer les calculs avec une simulation par automate cellulaire. Néanmoins, c'est possible si l'on se restreint aux automates finis multitêtes oublieux, c'est-à-dire dont la trajectoire des têtes de lecture sur un mot d'entrée ne dépend que de la taille dudit mot et non des lettres qui le composent. C'est un modèle de reconnaissance de langages simple, mais loin d'être trivial, puisque les langages reconnus constituent la classe NC1. Dans ce travail commun avec Gaétan Richard et Véronique Terrier du GREYC présenté à STACS 2011, on montre qu'un tel automate à k têtes, qui fonctionne en temps O(n^k), peut être simulé par un automate cellulaire fonctionnant en temps O(n^(k - 1)log(n)) et espace O(n^(k - 1)).

2014-01-27

Sergiu Ivanov (LACL - UPEC)

Petits réseaux de Petri universels

Nous examinons le problème de construction de réseaux de Petri de petite taille avec des arcs inhibiteurs. Nous considérons et essayons de minimiser quatre paramètres de complexité descriptive : le nombre de places, de transitions, d'arcs inhibiteurs, ainsi que le degré maximal d'une transition. Nous proposons six constructions avec les tailles suivantes des paramètres correspondants : (30, 34, 13, 3), (14, 31, 51, 8), (11, 31, 79, 11), (21, 25, 13, 5), (67, 64, 8, 3), (58, 55, 8, 5). Ces constructions améliorent les peu nombreux résultats connu par rapport à l'universalité des réseaux de Petri, et en plus nous mettons en évidence certains compromis. À cause des équivalences, notre résultats peuvent être traduits pour la réécriture des multiensembles avec des conditions interdisantes ou bien pour les systèmes P avec des inhibiteurs.

2014-01-20

Cinzia Di Giusto (équipe COSMO, IBISC, Université d'Evry)

Adaptable processes

I will introduce the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behaviour and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems such as workflows or cloud computing scenarios. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.

I will present a core calculus of adaptable processes and propose a framework for verifying and ensuring properties of the designed systems along two directions. First, I will show two specific verification problems and a way of generalising them. The verification properties ensures that the number of consecutive erroneous states that can be traversed during a computation is bound by some given number k, or that a state without errors will be eventually reached. We study the (un)decidability of these two problems and their generalisation in several variants of the calculus. Finally, I will propose a type system for statically ensuring that well typed processes guarantee safe and secure updates: for instance, we guarantee that no active protocol is interrupted by an update.

2014-01-13

Louis Bigo (LACL - UPEC)

Représentations symboliques musicales et calcul spatial

La notion d’espace symbolique est fréquemment utilisée en théorie, analyse et composition musicale. La représentation de séquences dans des espaces de hauteurs, comme le Tonnetz, permet de capturer des propriétés mélodiques et harmoniques qui échappent aux systèmes de représentation traditionnels. Nous généralisons cette approche en reformulant d’un point de vue spatial différents problèmes musicaux (reconnaissance de style, transformations mélodiques et harmoniques, classification des séries tous-intervalles, etc.). Les espaces sont formalisés à l’aide de collections topologiques, une notion correspondant à la décoration d’un complexe cellulaire en topologie algébrique. Un complexe cellulaire permet la représentation discrète d’un espace à travers un ensemble de cellules topologiques liées les unes aux autres par des relations de voisinage spécifiques. Nous représentons des objets musicaux élémentaires (par exemple des hauteurs ou des accords) par des cellules et construisons un complexe en les organisant suivant une relation de voisinage définie par une propriété musicale. Une séquence musicale est représentée dans un complexe par une trajectoire. L’aspect de la trajectoire révèle des informations sur le style de la pièce et les stratégies de composition employées. L’application d’opérations géométriques sur les trajectoires entraîne des transformations sur la pièce musicale initiale. Les espaces et les trajectoires sont construits à l’aide du langage MGS, un langage de programmation expérimental dédié au calcul spatial, qui vise à introduire la notion d’espace dans le calcul. Un outil, HexaChord, a été développé afin de faciliter l’utilisation de ces notions pour un ensemble prédéfinis d’espaces musicaux.

2014-01-06

Arthur Milchior (LACL - UPEC)

FO[<,mod], automates et décidabilité sur les mots

FO[N,+], la logique du premier ordre, sur les entiers naturels, utilisant uniquement la fonction + et l'égalité, est une logique très étudiée, appelée Logique de Presburger. Je m'intéresse à trouver des ressemblances et des différences entre cette logique et FO[N,<,mod], la logique du premier ordre sur les entiers naturels avec la relation d'ordre entre les variables et des prédicats modulaires du style “x=a mod b” si et seulement si a est congru à la variable x mod b.

Je parlerai dans cet exposé des deux principaux sujets sur lesquels j'ai travaillé en deux ans, de stage puis de thèse:

- Il existe plusieurs manières de caractériser les ensembles de vecteurs d'entiers, c'est à dire de sous-ensembles de N^d pour un entier d, définissables dans la logique de Presburger. Il s'agit des ensembles semilinéaires, mais aussi des ensembles rationnels quand on regarde (N^d,+) comme un monoïde. Il s'agit aussi des ensembles qui respectent la caractérisation de Muchnik, et aussi des ensembles E tels que tous les ensembles d'entiers définissables dans FO[N,+,E] soient ultimement périodiques, c'est le théorème de Michaux-Villemaire.

J'expliquerai que la caractérisation de Muchnik peut être modifiée de manière à caractériser les ensembles définissables dans FO[N,<,mod]. Que le théorème de Michaux-Villemaire peut être modifié pourvu qu'on rajoute l'hypothèse que les ensembles considérés soient semilinéaires. Enfin, j'expliquerai que cette propriété permet de prouver que la satisfiabilité de la logique FO[N,<,E] pour n'importe quel prédicat E semilinéaire non définissable dans FO[N,<,mod] est indécidable sur les mots.

- De plus, si un automate fini reconnaît un ensemble de vecteurs d'entiers, il est possible de décider en temps polynomial si cet ensemble est semilinéaire, c'est à dire s'il est dans FO[N,+]. J'expliquerai comment le problème est précisément défini, et qu'un algorithme fort différent permet de caractériser les automates acceptant un ensemble définissable dans FO[N,<,mod] ainsi que dans quelques logiques encore moins expressives.

2013-12-16

Yoann Marquer (LACL - UPEC)

Complétude algorithmique des langages impératifs

Gurevich a caractérisé dans “Sequential Abstract State Machines Capture Sequential Algorithms” les algorithmes symboliques séquentiels par ses ASMs. Philippe Andary, Bruno Patrou et Pierre Valarcher ont montré dans “A theorem of representation for primitive recursive algorithms” qu'un langage impératif simplifié (le Loop de Albert Meyer et Dennis Ritchie enrichi d'une instruction exit) permettait d'implémenter fidèlement (c'est à dire presque pas à pas) une classe restreinte d'ASMs : les APRAs (Arithmetical Primitive Recursive Algorithms). Mais :

  • les seuls symboles dynamiques sont les variables
  • le seul type de données utilisé est celui des entiers unaires
  • la complexité de l'algorithme est supposée primitive récursive.

Je m'intéresse à un langage de programmation impératif suffisamment général, de façon à ce que les résultats puissent être pertinents pour des langages réels comme le C ou le Python. Théorème 1 : Un langage impératif peut simuler presque pas à pas tout algorithme symbolique séquentiel. Le pas à pas peut être obtenu en augmentant la puissance du langage. Pour travailler sur la complexité de l'algorithme, c'est à dire la durée d'une exécution en fonction de la taille des entrées, il est nécessaire de pouvoir définir les types de données usuels ainsi que leur taille. Théorème 2 : Les types usuels peuvent être implémentés dans les structures logiques des ASMs. Cela comprend les booléens, les entiers, les mots et les listes. Les tableaux, les matrices, les graphes et les pointeurs feront l'objet d'une discussion. Ainsi, nous étendons bien le résultat sur les APRAs :

  • nous donnons un sens opérationnel à la notion de fonction dynamique
  • les types usuels sont décrits et leur taille bien définie
  • la complexité peut être quelconque en utilisant une instruction while, et de plus si elle est primitive récursive il est possible de n'utiliser que des instructions for à la place.

2013-11-25

Mikaël Cozic (Dep. Philo UPEC, ENS Ulm)

Probabilistic Unawareness

Awareness and unawareness are a major theme in the epistemic logic literature, but it is handled there only in terms of full belief operators. The present paper aims at a treatment in terms of partial belief operators. It draws upon the modal probabilistic logic that was introduced by Aumann (1999) at the semantic level and then axiomatized by Heifetz & Mongin (2001). The paper embodies in this framework those properties of unawareness which have been highlighted in the seminal paper by Modica & Rustichini (1999). This last paper is concerned with full belief, but we argue that the properties in question also apply to partial belief in the chosen probabilistic sense. The main result is a (soundness and) completeness theorem that reunites the two strands, modal and probabilistic, of epistemic logic.

2013-11-18

Mathieu Sassolas (LACL - UPEC)

Jeux pour la vérification et la synthèse: le cas de l'admissibilité pour des objectifs oméga-réguliers

Les jeux ont pris une place croissante dans le domaine de la vérification formelle de systèmes, en particulier parce qu'ils permettent également la synthèse de contrôleurs pour le système. Plusieurs notions qui avaient tout d'abord été proposées dans le cadre de modélisation de systèmes économiques ont été adaptées au contexte des jeux sur des graphes: dans le cas de jeux multijoueurs, on retient le plus souvent le concept d'équilibre de Nash. Mais d'autres paradigmes ont également été adaptés, en particulier celui d'élimination de stratégies dominées, qui est celui qui retiendra notre attention dans cet exposé.

Après avoir fait un bref tour d'horizon des applications des jeux pour la vérification, je m'intéresserai plus précisément à l'élimination itérative de stratégies dominées dans des jeux multijoueurs (infinis) sur des graphes (finis). Ici, chaque joueur dispose d'un objectif oméga-régulier qui n'est pas nécessairement en opposition avec celui des autres joueurs (jeu dit à somme non nulle). Dans ce cadre nous étudions l'algorithmique de problèmes naturels à propos de l'ensemble des stratégies admissibles – celles survivant toutes les phases d'élimination–, et obtenons leur complexité exacte. De plus, nous obtenons un automate reconnaissant l'ensemble des exécutions possibles lorsque tous les joueurs choisissent une stratégie admissible.

Les résultats présentés sont issu d'un travail conjoint avec Romain Brenguier et Jean-François Raskin.

2013-10-14

Cristian S. Calude (University of Auckland, New Zealand)

Quantum Randomness

We will present a strong form of the Kochen-Specker theorem which can be used to certifying a quantum random generator producing highly incompressible sequences.

2013-10-07

Pascal Vanier (LACL - UPEC)

Sous-shifts, conjugaison et calculabilité

Les sous-shifts de type fini (SFTs) sont des ensembles de coloriages du plan vérifiant des contraintes locales en nombre fini. Nous allons ici nous intéresser à la conjugaison, la notion d'isomorphisme adaptée aux sous-shifts, et plus particulièrement aux invariants de conjugaison. Alors qu'en dimension 1, l'étude des SFTs est plutôt algébrique, en dimension 2 et plus, elle est liée au calcul. Ceci est dû à la possibilité d'y encoder des diagrammes espace/temps de machines de Turing. Nous allons nous intéresser à la complexité algorithmique de la conjugaison et nous intéresser à deux invariants : l'un classique, le nombre de points périodiques, et l'autre nouveau, l'ensemble de degrés Turing.






Adresse :

LACL, Département d'Informatique
Faculté des Sciences et Technologie
61 avenue du Général de Gaulle
94010 Créteil Cedex

Secrétariat :

Flore Tsila
Bâtiment P2 - 2ème étage - bureau 223
Tél : +33 (0)1 45 17 16 47
Fax : +33 (0)1 45 17 66 01

Direction :

Régine Laleau
Bâtiment P2 - 2ème étage - bureau 243
Tél : +33 (0)1 45 17 65 97
Fax : +33 (0)1 45 17 66 01