Alexander Bockmayr et T. Kasper
---------------
Titre: Contraintes symboliques en programmation linéaire sur nombres entiers
Résumé:
Les contraintes symboliques jouent un rôle important dans la programmation par contraintes sur les domaines finis. Nous montrons comment introduire ce concept dans la programmation linéaire sur les nombres entiers pour améliorer l'expressivité et l'efficacité de cette approche.
-----------
Titre: Des flots vers un anamorphisme
Résumé:
L'utilisation des flots (listes infinies) est un modèle expressif et reconnu pour représenter différents phénomènes tels que le temps, les communications entre processus, les entrées/sorties. Leur spécification dans un langage de haut-niveau permet de les définir de facon modulaire,concise et proche de l'intuition. Mais la définition obtenue devient extrèmement complexe tant pour une implantation efficace que pour des raisonnements sur des propriétés globales.
Dans cet exposé, nous introduisons une technique permettant de transformer des définitions mutuellement récursives de flots en anamorphismes de flots. Nous capturons ainsi la récursion par un schéma unique. La formulation obtenue offre différrentes opportunités comme une implantation efficace par un système de transitions, la découverte d'invariants et la simplification de preuves telles que la sûreté (safety) et la vivacité (liveness). Cette technique préserve les avantages du langage de haut niveau en ne posant pas de contrainte sur le type des éléments du flot.
Dans une première partie, nous définissons une primitive MAPITER
i) qui nous permet d'exprimer l'anamorphisme sur les flots,
ii) qui possède de nombreuses propriétés notamment de fusions.
Ensuite nous présentons une stratégie qui permet de transformer les définitions de flots en expressions équivalentes basées sur MAPITER. Cette stratégie bien qu'incomplète s'avère dors et déjà concluante pour plusieurs exemples.
-----------------
Titre: Vérification des propriétés dynamiques des systèmes reactifs dans le cadre d'une spécification par raffinement en utilisant une technique hybride : preuve et Model-Checking.
Résumé:
Nous proposons de spécifier les systèmes réactifs par une méthode de raffinement (à la B). Les proprietes invariantes peuvent être certifiées par des techniques de preuve (l'atelier B par exemple) tandis que les propriétés dynamiques sont exprimées en LTL et vérifiées au niveau le plus abstrait par Model-Checking. Cependant, la validité du raffinement des propriétés dynamiques peut, pour certains schémas de raffinement, être vérifiée grâce à la certification d'un certain nombre d'invariants qui, eux, sont validés par le prouveur. Ceci doit permettre de réduire de facon importante la preuve par Model-Checking et permettre de vérifier des systèmes ayant nombre d'états finis pour qui une vérification complète par model-checking s'avérerait explosive.
---------------------
Titre: Développements récents de CLAIRE en matière de traitement de règles.
Résumé :
xxxxxxxxxxxxxxxx
Jacques Chassin de Kergommeaux
-----------------------
Titre: Programmation en logique OU-parallèle dans le projet APACHE.
Résumé:
Le projet INRIA APACHE développe un environnement appelé Athapascan, dont l'objectif est de faciliter la programmation efficace et portable des architectures parallèles émergentes. Nous supposons que ces architectures seront basées sur les multiprocesseurs symétriques à mémoire partagée, produits en série par la plupart des constructeurs généralistes. Ces multiprocesseurs comportent un nombre modéré de processeurs (quatre au maximum) connectés par un bus et une mémoire commune. Si l'on souhaite augmenter le degré de parallélisme, il est possible de connecter un certain nombre machines à mémoire partagée, en utilisant des réseaux locaux à hautes performances. L'environnement Athapascan développé dans le projet APACHE, vise à faciliter la programmation efficace et portable de telles architectures.
Athapascan se décompose en deux niveaux :
- Un noyau exécutif, Athapascan-0, à base de processus communicants. Athapascan-0 exploite deux niveaux de parallélisme : parallélisme entre noeuds mis en oeuvre par un nombre fixes de processus systèmes et parallélisme interne à chacun des noeuds, exploité par un réseau de fils d'exécution (threads) évoluant dynamiquement.
- Une interface de programmation parallèle, Athapascan-1 basée sur un modèle de parallélisme de tâches avec cohérence de données et permettant une répartition automatique de la charge de calcul.
Athapascan comporte également des outils d'aide à la mise au point de programmes parallèles.
Développé dans le cadre du projet APACHE, le système de programmation en logique OU-parallèle PloSys a pour objectif de résoudre l'ensemble des problèmes que pose la réalisation d'un système Prolog OU-parallèle efficace sur les architectures cibles du projet APACHE et dont l'utilisation soit entièrement transparente pour le programmeur. Ces problèmes sont essentiellement le traitement des effets de bords et de la coupure Prolog ainsi que les problèmes d'ordonnancement et d'allocation de tâches.
PloSys constitue une application importante de test pour les idées mises en oeuvre dans l'environnement Athapascan puisque, contrairement à certaines applications numériques, il est très difficile de prévoir la granularité des tâches qui peuvent être lancées en parallèle. Actuellement PloSys traîte efficacement les «gros» problèmes très combinatoires, mais peut se révéler moins efficace qu'un système de programmation en logique séquentiel pour les problèmes «petits» ou faisant des effets de bord. L'objectif sera d'obtenir dans tous les cas une efficacité au moins équivalente à celle des meilleurs systèmes séquentiels et ce, quelle que soit la granularité exploitable par le système parallèle cible.
-------------------
Titre: Compiling Semiring-based Constraints with clp(FD,S).
Résumé :
Le but de ce travail est d'étendre le paradigme de la Programmation Logique avec Contraintes afin de résoudre des problèmes sur-contraints, des problèmes flous et de faire du raisonnnement hypothétique.
Nous sommes basés sur des travaux théoriques développés à Pise par Stefano Bistarelli, Francesca Rossi et Ugo Montanari. Le cadre qu'ils proposent est celui des contraintes valuées dans des demi-anneaux (les contraintes deviennent donc des fonctions associant à un $n$-uplet un élément d'un demi-anneau).
Nos travaux ont été théoriques:
- étude de la consistance d'arc,
- consistance d'arc approchée,
mais aussi pratiques:
- implémentation du système {\clpFDS} (distribué par {\tt http}), ce langage générique de Programmation Logique avec Contraintes permet la résolution efficace de problèmes où les contraintes sont valuées dans un demi-anneau spécifiable par l'utilisateur,
- résolution de nombreux problèmes (tomographie, démonstration automatique, emplois du temps, ...).
-------
Titre: Parallel Algorithmic Skeletons and the Exploitation of Regularity in Symbolic Programming Résumé:
The skeletal approach to the design of parallel programming systems proposes that an acceptable balance between expressive clarity and effective implementability can be obtained by restricting the mechanisms through which parallelism can be introduced to a small number of architecture independent control constructs, originally known as `algorithmic skeletons'. Each skeleton specification captures the logical behaviour of a commonly occurring pattern of parallel computation (such as ``divide-and-conquer'', ``farm'' or ``scan''), while pre-packaging and hiding the details of its concrete implementation. Recent and ongoing work in the area addresses issues of presentation (eg as imperative block-structured mechanisms or as pure higher order functions), of implementation (particularly when composition is allowed) and of cost modeling (assisted by the restrictive nature of the approach). A further avenue for research addresses the question of whether such frameworks should attempt to be universal or targeted at restricted application domains. This talk will present an overview of the field and consider the scope for its application to the parallelization of activities in the areas of symbolic and constraint programming.
-----------
Titre: Définition récursive de tableaux et de champs de données.
Résumé:
Nous examinons la définition de tableaux par des équations fonctionnelles avec des maps, des concaténations et des coupures.
Notre but initial est de générer un code permettant de résoudre efficacement les contraintes sur les éléments des tableaux solutions. Dans notre cadre, ``efficacement'' veut dire que la résolution se fait par un nid de boucles générés statiquement à partir de la forme syntaxique des expressions qui apparaissent dans les équations.
La concaténation de deux tableaux quelconques n'étant pas nécessairement un tableau, nous reformulons ce problème en nous appuyant sur une structure de donnée plus générale : les champs de données. Nous essayons de caractériser la géométrie d'un champ de données solution d'un système d'équations récursives prenant une forme particulière et proposons une conjoncture. Pour finir, nous esquisserons l'architecture d'un support d'exécution parallèle permettant des calculs arbitraires sur les champs de données sur $Z^n$.
-------------
Titre: Stratégies parallèles de propagation d'intervalles
Résumé:
Les algorithmes de propagation d'intervalles vérifient une propriété de consistance de problèmes de satisfaction de contraintes (CSP) numériques en contractant les domaines des variables représentés par des intervalles. Ils appliquent dans un certain ordre, i.e. la stratégie de propagation, des opérateurs monotones associés aux contraintes, et sont confluents dans le sens où les domaines calculés sont indépendants de la stratégie.
Dans cet exposé, nous décrirons les deux types de stratégies séquentielles existantes, les unes adaptées de AC3 pour les calculs d'intervalles, les autres dediées à la simplification des cycles d'application des opérateurs. Puis les problèmes concernant la parallélisation de ces stratégies seront détaillés. Enfin, un nouveau type de stratégie séquentielle sera proposé, ainsi que différentes implantations parallèles possibles. Les coûts dûs au parallélisme seront quantifiés dans le modèle Bulk-Synchronous-Programming (BSP).
--------
Titre: On the Word, Subsumption, and Complement Problem for Recurrent Term Schematizations.
Résumé:
We investigate the word and the subsumption problem for recurrent term schematizations, which are a special type of constraints based on iteration. By means of unification, we reduce these problems to a fragment of Presburger arithmetic.
Our approach is applicable to all recurrent term schematizations having a finitary unification algorithm. Furthermore, we study a particular form of the complement problem. Given a finite set of terms, we ask whether its complement can be finitely represented by schematizations, using only the equality predicate without negation. The answer is negative as there are ground terms too complex to be represented by schematizations with limited resources.
----------------------
Titre: Programmation par Réécriture et Stratégies pour la Programmation avec Contraintes
Résumé:
Dans cet exposé, nous présentons un point de vue de la programmation avec contraintes, basé sur la notion de réécriture controlée par des stratégies. Ce concept nous permet de décrire d'une façon uniforme le mécanisme de résolution de contraintes et le méta-langage nécessaire pour manipuler les contraintes. Ceci a l'avantage de fournir des descriptions à base de règles pour modéliser des manipulations de contraintes comme l'unification ou la résolution de contraintes numériques. Notre approche est motivée par des exemples de solveurs de contraintes et de leurs combinaisons. Ces exemples sont spécifiés en ELAN, un langage de programmation par réécriture, enrichi par une notion de stratégie pour guider l'application des règles.
--------
Titre: Propagation de contraintes globales en ECLAIR.
Résumé:
Cet exposé présente l'intégration de contraintes globales dans Eclair, une librairie orientée-objet de propagation de contraintes sur les domaines finis. Les contraintes globales sont un outil puissant pour faire de la déduction sous contraintes en optimisation combinatoire pour deux raisons :
- d'une part, elles permettent de modéliser un problème par une formule et évitent ainsi l'éclatement de la modélisation en une foule de contraintes arithmétiques ;
- d'autre part, elles fournissent un cadre pour l'encapsulation d'algorithmes de Recherche Opérationnelle (par exemple, des algorithmes de graphes).
En se basant sur les contraintes globales aujourd'hui disponibles en eclair (permutations, listes croissantes, bijections et couplages de poids minimal), on discutera de l'introduction par l'utilisateur de nouvelles contraintes globales dans un outil de programmation par contraintes.
Deux points techniques spécifiques aux contraintes globales seront abordés :
- L'incrémentalité des algorithmes de propagation envisagés.
- Le mode de propagation envisagé (propagation immédiate ou retardée).
On illustrera cette présentation par deux exemples en optimisation combinatoire, d'une part un problème d'emploi du temps de lycée et le problème de la reconstruction de polyominos à partir de projection.
----------------
Titre: Programmation Génétique avec Contraintes, Application à la fouille de Données.
Résumé:
La Programmation Génétique est une méthode d'optimisation s'inspirant des mécanismes naturels de l'évolution. Elle se base sur l'évolution synchrone d'un grand nombre de solutions potentielles (appelées individus et codifiées sous forme d'arbres) regroupées en population. Des opérateurs comme la reproduction, le croisement ou la mutation sont appliqués aux individus d'une population pour obtenir la génération suivante.
Un problème important en programmation génétique est de garantir, lors de l'application des opérateurs, la validité des individus ainsi obtenus. En effet, l'échange aléatoire de sous-arbres entre individus conduit généralement, entre autre pour des problèmes de typage, à des expressions syntaxiquement et/ou sémantiquement incorrectes. Pour résoudre ce problème, nous avons proposé un nouveau cadre pour la programmation génétique s'appuyant sur une modélisation par contraintes : l'application des opérateurs est paramétrée par un ensemble de contraintes sur les domaines finis. Ce modèle peut être étendu pour permettre la définition d'espaces de recherche, les contraintes sont alors utilisées pour définir des biais sur ces espaces.
L'approche développée a été appliquée à la fouille de données, les individus sont alors modélisés par des expressions en algèbre relationnelle.
F. Saubion, S. Limet et P. Réty
-------------------------
Titre: E-Unification et langages d'arbres
Résumé:
Résoudre des équations modulo une théorie équationnelle E est une technique apparaissant comme essentielle pour la déduction automatique et la résolution de contraintes symboliques. Pourtant, en général, la E-unification est un problème indécidable. Nous proposons une méthode générale basée sur une utilisation de langages d'abres et permettant de décomposer et de traiter l'unification de deux termes en fonction des théories considérées. Comme application de ce shéma, nous montrerons quelques résultats de décidabilité pour la R-unification.
J.-M. Talbot, S. Tison, Ph. Devienne
---------------------------
Titre: Contraintes Ensemblistes et Analyse de Programmes Logiques.
Résumé:
Les contraintes ensemblistes usuelles expriment des inclusions ou non-inclusions entre des expressions ensemblistes définies à partir de symboles de fonction, d'opérateurs booléens et de projection. Elles ont été définies et sont utilisées pour l'analyse de programmes.
Nous avons généralisé ces contraintes, en ajoutant un opérateur de description intentionnnelle de la forme $\{x / \Phi(x)\}$, où $\Phi(x)$ est une formule monadique positive. Nous étudions alors deux sous-classes de contraintes généralisées positives, les définies et les co-définies; nous prouvons leur dualité et donnons un algorithme simple pour tester la satisfiabilité et calculer -sous forme d'automate d'arbres- la plus petite solution (resp. la plus grande) d'un système défini (resp. co-défini) généralisé si le système est satisfiable. Notre algorithme est basé sur les automates d'arbres et la robustesse de notre algorithme nous permet de traiter aussi bien le cas des arbres finis que celui des arbres finis et infinis.
------------
Titre: Contraintes ensemblistes et Spécifications Formelles.
Résumé:
De nombreuses methodes de specification formelles sont basees sur l'ecriture de machines abstraites qui decrivent l'etat d'un module et son evolution. Seules des proprietes statiques, concernant l'etat du systeme a un moment donne, peuvent generalement etre specifiees et verifiees. Nous proposons d'exprimer et de verifier des proprietes dynamiques de machines abstraites, par l'ecriture d'un systeme de contraintes sur des ensembles d'etats "atteignables" par les executions. Tous nos ensembles sont decrits intentionnellement, et nous utilisons la programmation logique pour leur donner une semantique. La verification de la machine abstraite, par rapport a ces proprietes, se fait par la construction d'un programme logique vu comme la synthese du comportement de ses operations, et permettant d'etudier l'ensemble des etats atteignables. Nous nous placons plus precisement dans le cadre de la methode de specification formelle B.