• 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-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

Résumé à venir

2015-01-26

Laure Daviaud (LIF Marseille)

Titre à venir

Résumé à venir

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 Barnot (ENS Cachan)

Titre à venir

Résumé à venir

2015-01-05

Denis Kuperberg (IRIT/ONERA, Toulouse)

Titre à venir

Résumé à venir

2014-12-15

Membres du LACL () Toute la journée

Seconde Journée Séminaire Local LACL

Résumé à venir

2014-12-08

Membres du LACL () Toute la journée

Première Journée Séminaire Local LACL

Résumé à 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