Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Les séminaires du LIFO

 English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 70 11
Fax: +33 (0)2 38 41 71 37



Les séminaires du LIFO


Accès par année : 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017

Sauf exception, les séminaires se déroulent le lundi de 14h à 15h, Salle de réunion 1, bâtiment IIIA (voir plan du campus).


23/11/2001 : Games for synthesis of controllers with partial observation
André Arnold (Université Bordeaux 1) Résumé

22/10/2001 : Un schéma d'approximation pour la dissémination de données
Nicolas Schabanel (CNRS - ENS Lyon) Résumé

08/10/2001 : Automatising Reasoning in Many-valued Logics, and How to Automatise Automatisation
Gernot Salzer (Technische Universität Wien, Autriche) Résumé

24/09/2001 : Analyse de protocoles de securité par les flots d'information
Stéphane Lafrance (Ecole Polytechnique de Montréal) Résumé

30/06/2001 : Soutenance d'habilitation : Langages synchronises d'arbres et applications
Pierre Réty (LIFO) Résumé

25/06/2001 : Soutenance de thèse: Conception des curcuits programmables par la réécriture conditionnelle et étude des aspects vectoriels des fonctions booléennes
Zahir Maazouzi (LIFO) Résumé

28/05/2001 : Intervalles et contraintes numériques
Laurent Granvilliers (IRIN) Résumé

09/04/2001 : Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis
Thi Bich Hanh DAO (LIM) Résumé

02/04/2001 : CHR and Harrop formulas: entailment, universal constraints, cooperation of solvers
Olivier Ridoux (IRISA, Rennes) Résumé

19/03/2001 : Implementing an Object Oriented Design in Curry
Herbert Kuchen (University of Münster) Résumé

19/02/2001 : Mise en oeuvre automatisée d'analyseurs d'exécutions performants
Erwan Jahier (IRISA Rennes) Résumé

05/02/2001 : Langages synchronises d'arbres et application a la concurrence
Pierre Réty (LIFO) Résumé


Résumés des séminaires


Games for synthesis of controllers with partial observation André Arnold, Université Bordeaux 1

The synthesis of controllers for discrete event systems, as introduced by Ramadge and Wonham, amounts to computing winning strategies in parity games. We show that in this framework it is possible to extend the specifications of the supervised systems as well as the constraints on the controllers by expressing them in the modal $\mu$-calculus. In order to express unobservability constraints, we propose an extension of the modal $\mu$-calculus in which one can specify whether an edge of a graph is a loop. This extended $\mu$-calculus still has the interesting properties of the classical one. In particular it is equivalent to automata with loop testing. The problems such as emptiness testing and elimination of alternation are solvable for such automata. The method proposed in this paper relies on a simple construction of the quotient of automata with loop testing by a deterministic transition system. This is enough to deal with the centralized control problems. The solution of the decentralized control problems uses a more involved construction of the quotient of two automata. This work extends the framework of Ramadge and Wonham in two directions. We consider infinite behaviours and arbitrary regular specifications, while the standard framework deals only with specifications on the set of finite paths of processes. We also allow dynamic changes of the set of ob- servable and controllable events.


Un schéma d'approximation pour la dissémination de données Nicolas Schabanel, CNRS - ENS Lyon

Un schéma d'approximation est un algorithme qui prend en entrée une variable supplémentaire epsilon et donne en sortie une solution approchée d'un problème à epsilon près au bout d'un temps polynomial (qui dépend d'epsilon), quelque soit epsilon > 0. Dans cet exposé, je vous présenterai comment on peut construire un tel algorithme pour le problème de la dissémination de données. La dissémination de données est une protocole proposé pour diminuer la charge des réseaux et serveurs d'information. Souvent, la plupart des clients demande la plupart du temps les mêmes informations. Aussi, afin d'éviter de saturer à la fois le serveur et le réseau avec la diffusion des pages les plus populaires, l'approche de la dissémination propose de réserver un certain nombre de canaux d'émission à la diffusion systématique des informations les plus populaires. Ces canaux (typiquement Hertzien, TV par câble, satellite, ...) sont accessibles en simultané par tous les clients. Le problème est alors d'ordonnancer la diffusion des différentes pages d'information. Un client, intéressé par l'une de ces pages, n'émet pas de requête mais se connecte sur ces canaux réservés et attend que l'information qui l'intéresse soit diffusée. Il s'agit donc de trouver un ordonnancement qui minimise l'attente moyenne des clients. Ce problème, NP-dur en général, est un problème de minimisation quadratique, qui modélise également d'autres problèmes d'ordonnancement tels la planification de maintenances de machines ou le réapprovisionnement de stocks. Il en existe différentes variantes. Nous nous intéresserons dans cet exposé au cas où les pages ont toutes la même taille: dans ce cas nous pouvons construire une solution "presque"-optimale.


Automatising Reasoning in Many-valued Logics, and How to Automatise Automatisation Gernot Salzer, Technische Universität Wien, Autriche

Gernot Salzer : Automatising Reasoning in Many-valued Logics, and How to Automatise Automatisation After introducing and motivating many-valued logics we will explain how proof techniques from classical logic (like resolution, tableaux, sequent calculus) can be generalised to cope with arbitrary finitely-valued logics. Given a particular logic specified by the truth tables of its operators and quantifiers, calculi for automated reasoning can in turn be constructed automatically. The talk will conclude with a presentation of MUltlog, a program that generates ready-to-publish scientific papers out of minimal input.


Analyse de protocoles de securité par les flots d'information Stéphane Lafrance, Ecole Polytechnique de Montréal

Le problème de s'assurer que les protocoles de securité que nous utilisons régulièrement sont fiables est loin d'être trivial. Nous présenterons une méthode de validation pour de tels protocoles, tout particulièrement pour des cryptoprotocoles et des protocoles de transactions électroniques, basée sur l'analyse de leurs flots d'informations


Soutenance d'habilitation : Langages synchronises d'arbres et applications Pierre Réty, LIFO

Afin de manipuler des ensembles infinis de termes, et de disposer d'une expressivite plus grande que celle des langages reguliers d'arbres, nous introduisons les langages synchronises d'arbres, et nous presentons des applications a la reecriture et a la concurrence.


Soutenance de thèse: Conception des curcuits programmables par la réécriture conditionnelle et étude des aspects vectoriels des fonctions booléennes Zahir Maazouzi, LIFO

Dans ce travail, nous proposons une méthode de conception originale pour les circuits combinatoires de type FPLA, basée sur des techniques de réécriture conditionnelle. Ce cadre théorique fort nous permet d'obtenir une méthode correcte (les solutions proposées sont exactes) et complète. L'implémentation du système de règles d'inférences, s'est faite dans un premier temps en utilisant un démonstrateur automatique dans les théories de Horn. Pour améliorer les performances nous avons développé des heuristiques et des stratégies, propres à nos objectifs. Puis nous avons élaboré un nouveau logiciel en adaptant les structures de données et ne conservant que les traitements nécessaires à notre problématique. Nous avons ensuite étudié l'aspect vectoriel de l'algèbre de Boole et ainsi dégagé de nouvelles propriétés sur les tables de vérités et la notion de «somme de produits» d'une fonction booléenne. Ceci nous a permis d'optimiser considérablement en mémoire et en temps notre méthode, tout en conservant la correction et la complétude. L'efficacité restant toutefois limitée, nous avons repris les propriétés dégagées et proposé une nouvelle représentation dite «chapeau» des produits booléennes. Cette nouvelle représentation a l'avantage de la représentation dite syntaxique tout en conservant les propriétés établies sur la forme vectorielle. Ceci nous a permis de dépasser le cadre de conception de circuit et de proposer un arbre ternaire ayant pour racine une fonction booléenne et codant sous forme «chapeau» l'ensemble de ses implicants premiers. Cet arbre inclut la nouvelle notion de sémantique d'une fonction booléenne qui optimise notre méthode. Cette approche a aussi été utilisée pour le calcul d'une couverture irredondante d'une fonction. La complexité théorique et la comparaison avec d'autres méthodes existantes sont étudiées et l'amélioration est confirmée en pratique par le développement d'un prototype ayant comme structures de données sous-jacente les BDD.


Intervalles et contraintes numériques Laurent Granvilliers, IRIN

Les intervalles donnent un moyen de calculer avec correction et garantie les solutions de problèmes numériques difficiles. On montrera comment se rejoignent les techniques d'analyse par intervalles, de propagation de contraintes, et de calcul symbolique au coeur des solveurs de contraintes actuels.


Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis Thi Bich Hanh DAO, LIM

Nous nous intéressons à la résolution de contraintes dans la théorie complète $T$ des arbres éventuellement infinis. Ces contraintes se présentent sous forme de formules générales du premier ordre construites à partir d'un ensemble infini de symboles d'opérations et de l'égalité. Par, résoudre une contrainte $p$ dans $T$, nous entendons : transformer $p$ en une contrainte $q$ équivalente dans $T$, qui est la constante logique $vrai$ si $p$ est toujours vraie dans $T$, est la constante $faux$ si $p$ est toujours fausse dans $T$. De plus, si $p$ ou sa négation a une base fini de solutions dans un modèle de $T$, alors ces solutions ou non-solutions doivent être explicites dans $q$. Après avoir introduit l'algèbre des arbres qui constitue un modèle de la théorie $T$, nous montrons que nos contraintes ont un pouvoir d'expression << quasi-universel >> et proposons un algorithme en 11 règles de réécriture de sous-formules pour les résoudre. Nous considérons ensuite la structure obtenue en introduisant dans cette algèbre un prédicat unaire $fini(x)$, exprimant que $x$ est un arbre fini. Nous proposons une extension $T\union FINI$ de la théorie $T$ admettant cette structure comme modèle. Nous donnons un algorithme pour résoudre les contraintes dans $T\union FINI$ en 16 règles de réécriture et concluons ainsi que $T\union FINI$ est une théorie complète. Nous donnons également un système de 12 règles de réécriture qui effectue le même type de résolution de contraintes dans la théorie des arbres finis. Nous terminons par des détails sur l'implantation d'algorithmes de résolution de contraintes, dans la théorie $T$ des arbres éventuellement infinis et dans la théorie des arbres finis. Les exemples qui nous ont servi à montrer le pouvoir d'expression de nos contraintes nous permettent de produire des benchmarks intéressants.


CHR and Harrop formulas: entailment, universal constraints, cooperation of solvers Olivier Ridoux, IRISA, Rennes

We propose an integration of Constraints Handling Rules (CHR) and Harrop formulas. Implication in goals offers a means for dynamically loading CHR rules, and for augmenting the constraint store. Constraints in goals are checked against the current store, but do not augment the store. Universal quantifier in goals offers a means for introducing new constrained variables. The neat effect of this integration is that the constraint store is more like a LambdaProlog program than like a Prolog goal. In particular, consistency checking (when augmenting the store) and entailment (when checking a constraint against the store) are clearly distinguished. This helps among other things in making different solvers cooperate. A high-level implementation is sketched. It uses in a critical way a feature of the Prolog/Mali implementation of LambdaProlog called substitutable terms.


Implementing an Object Oriented Design in Curry Herbert Kuchen, University of Münster

Declarative programming languages provide a higher level of abstraction and more powerful concepts than typical imperative and object oriented languages. On the other hand, the object oriented paradigm is superseding conventional approaches to software development like SA/SD and modular design. This is, among others, due to the better reusability and simpler maintenance of object oriented components. As a consequence, only languages which enable a simple implementation of object oriented designs will remain interesting for the development of significant software systems. It will be considered how an object oriented design can be implemented in the functional logic language Curry.


Mise en oeuvre automatisée d'analyseurs d'exécutions performants Erwan Jahier, IRISA Rennes

De nombreuses études montrent que la plus grande partie du coût de production d'un logiciel est générée lors de la phase de maintenance. Lors de cette phase, pour corriger des erreurs, pour optimiser des programmes, ou pour ajouter des fonctionnalités, il est essentiel de comprendre les programmes, et en particulier de comprendre leur comportement. Les analyseurs dynamiques d'exécutions tels que les profileurs, les moniteurs, ou les débogueurs, sont alors des outils indispensables. Cependant, ces outils d'analyse dynamique sont extrêmement coûteux à mettre en oeuvre : (1) d'abord, parce qu'il est généralement nécessaire de modifier le système de compilation utilisé, ce qui est fastidieux et pas toujours envisageable ; (2) en outre, les besoins en outils d'analyse de programmes varient d'un utilisateur à l'autre, en fonction de sa compétence, de son expérience du système de programmation utilisé, ainsi que de sa connaissance du code à maintenir ; (3) et enfin, parce que ces outils sont difficilement réutilisables. Il est donc souhaitable que chaque utilisateur puisse spécifier facilement les analyses dynamiques dont il a besoin. C'est pourquoi nous proposons une architecture qui permet de faciliter leur mise en oeuvre. Cette architecture est basée : (1) sur une instrumentation systématique du programme qui produit une image très détaillée de l'exécution, la trace ; (2) sur un ensemble de primitives qui permettent d'analyser cette trace efficacement. Les analyseurs résultants ont des performances du même ordre de grandeur que leurs équivalents implémentés <> par modification du système de compilation. Ils peuvent être mis en oeuvre par des utilisateurs sans connaissance particulière du système de compilation, qu'ils n'ont pas à modifier. Cette architecture leur permet d'implémenter les outils qui leur conviennent, adaptés à leur niveau de compréhension du code qu'ils sont chargés de maintenir. De plus, la structure modulaire de l'architecture proposée devrait permettre de faciliter la réutilisation de ces analyseurs pour d'autres systèmes. Notre propos est illustré dans le cadre du langage de programmation logique et fonctionnelle Mercury.


Langages synchronises d'arbres et application a la concurrence Pierre Réty, LIFO

Nous présentons une formulation nouvelle et plus simple des langages synchronisés de n-uplets d'arbres. Ce nouveau formalisme permet de prouver des propriétés structurelles plus fortes. En conséquence, les langages synchronisés donnent lieu à de nouvelles applications, en particulier a la concurrence. Nous introduisons une extension des algebres de processus PA permettant la communication sous une forme bornee, et nous montrons qu'une restriction de la logique temporelle (logique EF) est decidable sur cette structure infinie. Par consequent, l'absence d'interblocages est decidable. Ce resultat etend celui de Lugiez-Schnoebelen a une algebre de processus avec communication.