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

Mickaël Randour (LSV - Ens Cachan)

Titre à venir

Résumé à venir

2015-03-23

Victor Allombert (LACL - UPEC)

Multi-BSML, une approche à la ML pour la programmation Multi-BSP

Le modèle Multi-BSP, extension du modèle de parallélisme quasi-synchrone BSP, propose une représentation des machines hiérarchique sous la forme d'un arbre de mémoires et de processeurs. En s'appuyant sur ce modèle, nous proposons le langage Multi-BSML conçu pour programmer des algorithmes adaptés à ces machines hiérarchiques. Le langage Multi-BSML est basé sur BSML (Bulk Synchronous Parallel ML), un langage fonctionnel pour la programmation d'algorithmes BSP. Nous proposons deux approches, la première est un langage très général étendant la syntaxe OCaml et permettant d'écrire de manière efficace et expressive des algorithmes Multi-BSP ; la seconde est un squelette purement fonctionnel autorisant le développement de programmes certifiés grâce à l'assistant de preuve Coq. Nous présenterons les principaux concepts du langage Multi-BSML et comparerons, avec quelques exemples, les différences des deux approches proposées.

2015-03-16

Rodica Bozianu (LACL - UPEC)

Safraless Synthesis for Epistemic Temporal Specifications

We address the synthesis problem for specifications given in linear temporal single agent epistemic logic, KLTL, over single-agent systems having imperfect information of the environment state. R. van der Meyden and M. Vardi have shown that this problem is 2Exptime complete. However, their procedure relies on complex automata constructions that are notoriously resistant to efficient implementations as they use Safra-like determinization.

We propose a ”Safraless” synthesis procedure for a large fragment of KLTL. The construction transforms first the synthesis problem into theproblem of checking emptiness for universal co-Büchi tree automata using an information-set construction. Then we build a safety game that can be solved using an antichain-based symbolic technique exploiting the structure of the underlying automata. The technique is implemented and applied to a couple of case studies.

Further, we try to extend the procedure for the entire KLTL by defining automata accepting sets of words satisfying KLTL formula. We use the J. M. Couvreur’s construction of Büchi automata for LTL formulas and extend it to accept sets of words satisfying KLTL formulas.

2015-03-09

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

Some new definability and complexity results in monadic second-order arithmetic

Let $ A $ be a structure with domain the natural numbers. Consider the following properties:

— for every positive natural number $ n $, the set of $\Pi^1_n$-sentences true in $ A $ is $\Pi^1_n$-complete;

— for every positive natural number $ n $, if a set $ X $ of natural numbers is $\Pi^1_n$-definable in the standard model of arithmetic and closed under automorphisms of $ A $, then it is $\Pi^1_n$-definable in $ A $.

I prove that the natural numbers with the coprimeness relation and all Pascal's triangles modulo a prime have both properties. In effect, the proofs provide a method which can be used in other situations. E.g. the same holds for the natural numbers with the divisibility relation.

2015-02-16

Maxime Senot (LACL - UPEC)

Le monde des signaux, ou comment calculer géométriquement dans le plan

Les machines à signaux constituent un modèle de calcul simple qui permet de calculer géométriquement sur un espace-temps continu, à savoir le plan euclidien. Ce modèle tire son origine dans le monde des automates cellulaires, et les objets de base sont des signaux abstraits unidimensionnels et leurs interactions, modélisées sous forme de collisions entre ces signaux. Nous donnerons un bref aperçu de ce modèle de calcul non-classique, ainsi que certaines de ces principales propriétés calculatoires, comme son pouvoir de calcul et son efficacité en terme de calcul parallèle.

2015-02-09

Farah Ait-Salaht (SAMOVAR, Télécom SudParis) de 13h30 à 14h30

Approche par encadrement pour l’analyse de modèles complexes

Nous remarquons que pour certains problèmes, nous n’avons pas besoin de la valeur exacte de la mesure requise pour prendre une décision. Il suffit de déterminer une borne et la comparer au seuil donné pour conclure. Dans cet exposé, je présenterai premièrement la problématique des chaînes de Markov incomplètement spécifiées et pour laquelle nous avons proposé des algorithmes de bornes sur les distributions stationnaires. Dans un second temps, j’exposerai une approche de bornes stochastiques sur les distributions discrètes qui a pour objectif réduire la taille et ainsi le coût de calcul des modèles. Partant de distributions discrètes définies sur un espace d’état très grand, nous déterminons des distributions bornantes définies sur des supports de tailles réduites qui offrent un encadrement très fin de la distribution initiale (exacte). Le fait de pouvoir ainsi paramétrer la taille des distributions bornantes va permettre de faire un compromis intéressant entre le temps de calcul et la qualité des bornes.

Je montrerai également l’applicabilité de ces approches dans différents domaines : fiabilité, évaluation de performance, vérification probabiliste, etc.

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