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

Laure Daviaud (LIF Marseille)

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)

Titre à venir

Résumé à venir

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