• English
  • français


  • English
  • français

Séminaire

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

Contact : Luidnel Maignan

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



Séminaires 2014-15

2015-03-30

Mickaël Randour (LSV - Ens Cachan)

Titre à venir

Résumé à venir

2015-03-09

Stanislav Speranski (Laboratory of Logical Systems, Sobolev Institute of Mathematics)

Titre à venir

Résumé à venir

2015-02-16

Maxime Senot (LACL - UPEC)

Titre à venir

Résumé à venir

2015-02-09

Farah Ait-Salaht ()

Titre à venir

Résumé à venir

2015-02-02

Maël Pégny (IHPST - Université de Paris-1)

La théorie de la complexité : problèmes de fondements

'La théorie de la complexité permet de démontrer des bornes ultimes sur la difficulté des problèmes computationnels.' Dans cet exposé philosophique, j'essayerai de montrer les nombreux problèmes que cette caractérisation d'apparence innocente peut dissimuler, et de rendre manifeste que la théorie de la complexité est une science jeune en attente de fondements théoriques propres.

2015-01-26

Laure Daviaud (LIF Marseille)

Max-plus automata and size-change abstraction

Max-plus automata are weighted automata over the semiring (NU{-infinite}, max, +) that compute some functions from words to NU{-infinite}. More precisely, a max-plus automaton is a non deterministic finite automaton with a weight on each transition. The weight of a given run is the sum of the weights of the transitions along the run and the weight of a word w is the maximum of the weights of the runs labelled by w and going from an initial state to a final state.

In this talk, we will study the asymptotic behaviour of a max-plus automaton and more precisely the maximum length of a word of weight at most n. In particular, I will show that this function is of the form Theta(n^alpha) for a computable rational alpha. I will also explain how this analysis can, in combination with the size-change abstraction, be used for inferring the termination time of an algorithm as a function of the size of its input.

This is a joint work with Thomas Colcombet (LIAFA, Université Paris 7, CNRS) and Florian Zuleger (Vienna University).

2015-01-19

Anael Grandjean (LIRMM - Université Montpellier 2)

Comparing 1D and 2D Real Time on Cellular Automata

We study the influence of the dimension of cellular automata (CA) for real time language recognition of one-dimensional languages with parallel input. Specifically, we focus on the question of determining whether every language that can be recognized in real time on a 2-dimensional CA working on the Moore neighborhood can also be recognized in real time by a 1-dimensional CA working on the standard two-way neighborhood. We show that 2-dimensional CA in real time can perform a linear number of simulations of a 1-dimensional real time CA. If the two classes are equal, then the number of simulated instances can be polynomial.

2015-01-12

Benoit Barbot (ENS Cachan)

Accélération pour le Model Checking Statistique

Ces dernières années, l'analyse de systèmes complexes critiques est devenue de plus en plus importante. En particulier, l'analyse quantitative de tels systèmes est nécessaire afin de pouvoir garantir que leur probabilité d'échec est très faible. La difficulté de l'analyse de ces systèmes réside dans le fait que leur espace d’état est très grand et que la probabilité recherchée est extrêmement petite, de l'ordre d'une chance sur un milliard, ce qui rend les méthodes usuelles inopérantes.

Les algorithmes de Model Checking quantitatif sont les algorithmes classiques pour l'analyse de systèmes probabilistes. Ils prennent en entrée le système et son comportement attendu et calculent la probabilité avec laquelle les trajectoires du système correspondent à ce comportement. Ces algorithmes de Model Checking ont été largement étudié depuis leurs créations. Deux familles d'algorithme existent :

  • le Model Checking numérique qui réduit le problème à la résolution d'un système d'équations. Il permet de calculer précisément des petites probabilités mais soufre du problème d'explosion combinatoire;
  • le Model Checking statistique basé sur la méthode de Monte-Carlo qui se prête bien à l'analyse de très gros systèmes mais qui ne permet pas de calculer de petite probabilités.

La contribution principale de cette thèse est le développement d'une méthode combinant les avantages des deux approches et qui renvoie un résultat sous forme d'intervalles de confiance. Cette méthode s'applique à la fois aux systèmes discrets et continus pour des propriétés bornées ou non bornées temporellement. Cette méthode est basée sur une abstraction du modèle qui est analysée à l'aide de méthodes numériques, puis le résultat de cette analyse est utilisé pour guider une simulation du modèle initial. Ce modèle abstrait doit à la fois être suffisamment petit pour être analysé par des méthodes numériques et suffisamment précis pour guider efficacement la simulation. Dans le cas général, cette abstraction doit être construite par le modélisateur. Cependant, une classe de systèmes probabilistes a été identifiée dans laquelle le modèle abstrait peut être calculé automatiquement.

Cette approche a été implémentée dans l'outil Cosmos et des expériences sur des modèles de référence ainsi que sur une étude de cas ont été effectuées, qui montrent l'efficacité de la méthode.

2015-01-05

Denis Kuperberg (IRIT/ONERA, Toulouse)

Good-for-Games automata versus Deterministic automata

Good-For-Games (GFG) automata are non-deterministic automata with a semantic condition that gives them some deterministic features: there must exist a strategy to resolve the non-determinism without future look-ahead, that allows to accept every word of the language. This notion was introduced in different contexts and several questions about its precise link with determinism were left open. The interest of these GFG automata stems from the fact that they can be used instead of deterministic ones in the context of games. For instance unlike general nondeterministic automata, GFG automata can be used in a sound way to evaluate the output of a game. It turns out that this new notion of GFG automata is only interesting over infinite words, since it boils down to determinism on finite words. After presenting examples of such GFG automata on infinite words, I will describe results on the blow-up problem, i.e. can we save states by replacing determinism by GFGness? This is joint work with Michał Skrzypczak.

2014-12-15

Membres du LACL () Toute la journée

Seconde Journée Séminaire Local LACL

  • 9h30-10h30: Fabrice Mourlin : “Measurement and improvement of Mobile Cloudlet interaction protocols”
  • 10h30-11h30: Serghei Verlan : “Langages formels, Algèbre et Combinatoire - outils pour l’accélération du calcul parallèle”
  • 11h30-12h00: Elisabeth Pelz, Nathalie Caspard

Pause déjeuner

  • 14h20-14h50: Daniele Varacca : “Sous-typage sémantique pour Java”
  • 14h50-15h30: Frédéric Gava : “TurtleArt, Thymio, Scratch, Snap; Et bour et bour et ratatam”
  • 15h30-14h30: Mathieu Sassolas : Titre à venir

2014-12-08

Membres du LACL () Toute la journée

Première Journée Séminaire Local LACL

  • 9h30-10h30: Anatol Slissenko : “Espace métrique d'événements d'algorithme”
  • 10h30-11h30: Nihal Pekergin : “Différentes applications de la méthode de comparaison stochastique”
  • 11h30-12h30: Alexis Bès : “Logique MSO et relations de cardinalité”

Pause déjeuner

  • 14h30-15h00: Régine Laleau, Pierre Valarcher
  • 15h00-15h30: Antoine Spicher
  • 15h30-16h30: Catalin Dima : Titre à venir

2014-12-01

Nicolas Troquard (LACL - UPEC)

Raisonnement sur les jeux stratégiques

On présente une logique pour raisonner sur les jeux stratégiques. La logique proposée est un formalisme modal avec des modalités pour parler des pouvoirs des agents, et des modalités pour parler des préférences des agents. Si souvent les logiques modales sont interprétés sur des modèles de Kripke, ça n'est pas le cas ici. On représente les jeux stratégiques avec des modèles plus compacts basés sur les modèles de contrôle propositionnel. On montre que de nombreux concepts d'équilibre peuvent être exprimés dans la logique. On présente ensuite quelques applications directe des problèmes de décision de la logique pour résoudre des problèmes de la théorie du choix social.

Cette présentation est basé sur http://www.loa.istc.cnr.it/personal/troquard/PAPERS/TrvdHWo09aamas.pdf

2014-11-17

Amélie David (IBISC, Université d'Evry-Val-d'Essonne)

Méthode de décision de la satisfiabilité basée sur les tableaux pour ATL+

La logique ATL (Alternating-time Temporal Logic) et ses extensions sont des langages naturels pour la spécification de systèmes ouverts, i.e. de systèmes interagissant avec leur environnement. Les composantes du système ainsi que l'environnement sont représentés par un jeu dans lequel les joueurs ou des coalitions de joueurs doivent trouver une stratégie pour atteindre leur objectif. La logique ATL+ correspond à l'extension permettant la description de plusieurs objectifs à l'intérieur d'un même stratégie. Nous souhaitons répondre de manière automatique et constructive au problème de la satisfiabilité: existe-t-il un modèle d'une formule donnée? Nous présentons donc une méthode de décision pour l'extension ATL+ basée sur les tableaux permettant de résoudre le problème de manière optimale en 2EXPTIME.

2014-10-20

Clément Aubert (LACL - UPEC)

La logique linéaire, outil de la théorie de la démonstration pour la complexité implicite.

La logique linéaire est un système d’étude des preuves qui porte son attention sur les règles structurelles (affaiblissement, contraction) et de fait introduit dans les preuves une notion de limitation des ressources. Elle est dotée d’une dynamique de ré-écriture de preuves (l’élimination des coupures) qui est isomorphe à l’évaluation de programmes (formalisé comme la bêta-réduction dans le lambda-calcul), par la correspondance de Curry-Howard. Il est possible de n’étudier que des fragments de cette logique, et ainsi de restreindre les règles et le pouvoir expressif de ce système. Ce faisant, on peut produire des spécifications de langages de programmation à complexité bornée : tout programme rédigé dans telle syntaxe peut résoudre des problèmes d’au moins telle complexité, déterminer le résultat de l’évaluation de tel programme rédigé dans cette syntaxe nécessite au plus tant de ressources.

Ce champ de la complexité implicite fût le terrain principal de mes recherches jusqu’ici, intégrant des outils sémantiques (on interprète les preuves comme des opérateurs dans une algèbre de von Neumann, ou encore avec des termes du premier ordre) qui ont permis d’obtenir des caractérisations « abstraites » de classes de complexité célèbres (co-NL, L, P). Je vous en présenterai les grandes lignes, du cadre général de la théorie de la démonstration à la complexité implicite et même, si le temps le permets, comment les automates se sont avérés être un outil précieux et vivifiant de cette approche.

2014-10-06

Youssouf Oualhadj (LACL - UPEC)

Probabilistic Robust Timed Games

Solving games played on timed automata is well-known and has led to tools and industrial case studies. In these games, the first player Controller chooses delays and actions and the second player Perturbator resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. These notions of robustness guarantee the implementability of synthesized controllers. We provide characterizations of the resulting games for Büchi conditions, and prove the EXPTIME-completeness of the corresponding decision problems.






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 215
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 208
Tél : +33 (0)1 45 17 65 97
Fax : +33 (0)1 45 17 66 01