- Renseignements pratiques
- Enseignement
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 99 29
Fax: +33 (0)2 38 41 71 37
Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018
RR-2004-01 Manipulating Tree Tuple Languages by Transforming Logic Programs
Sebastien Limet and Gernot Salzer
Résumé : Nous introduisons la notion de définitions inductives sur des expression de langage comme cadre pour spécifier des langages de n-uplets d'arbres. Les définitions inductives et leurs sous-classes ont une correspondance naturelle avec des classes de programmes logiques et les opération su les langages de n-uplets d'arbres correspondent à la transformation de programmes logiques. Nous présentons un algorithme basé sur la notion de dépliage qui est capable de traiter plusieurs classes de languages de n-uplets de manière uniforme. Les preuves de terminaison de cet algorithme pour certaines classes de clauses se traduisent directement en propriétés de clôture de certaines opérations sur les languages de n-uplets ce qui permet d'obtenir de nouveaux resultats de décidabilité et de calculabilité.
Mot(s) Clé(s) : Langages d'arbres; programmation logique; décidabilité; transformation de programmes
RR-2004-02 Can We Load Efficiently Dense datasets ?
Ansaf Salleb and Christel Vrain
Résumé : We address the problem of representing and loading transactional datasets relying on a compressed representation of all the transactions of that dataset. We present an algorithm, named BoolLoader, to load transactional datasets and we give an experimental evaluation on both sparse and dense datasets. It shows that BoolLoader is efficient for loading dense datasets and gives a useful tool to evaluate the density of a dataset.
Mot(s) Clé(s) : Transactional datasets, boolean functions, decision diagrams, dense datasets, frequent itemsets.
RR-2004-03 A Timed Synchronous Algebra for Information Flow Analysis
S. Anantharaman, J. Chen, G. Hains
Résumé : The formalism of value-passing processes is well-suited for modeling and analyzing protocols. Timed processes account for the time consumed by the actions of the agents. In this paper we define process algebras with a view to cover both these aspects. Synchronous composition will be the central notion in our definition, since the the role played by the synchronous branches is crucial in the analysis of information flow on value-passing processes. Algebraically, parallel synchronous composition will be distributive over the choice operator, and by adding the action prefixes we get a PACUID-signature on which we define our process algebras. With such a vision, we propose an approach based on natural observation criteria and associated notions of non-interference, and show that they are well adapted for the confidentiality and authentication analysis of cryptographic protocols. Our algebra can also be extended naturally into a timed process algebra with a simple algebraic and operational semantics.
Mot(s) Clé(s) :
RR-2004-04 Context-Free Tree languages for Descendants
Pierre Réty, Julie Vuotto
Résumé : The preservation of regular tree languages through rewriting, has already been studied. In this paper, we study the preservation of context-free tree languages through rewriting, for constructor-based term rewrite systems. We give positive and negative results. Positive results are effective since we give algorithms to build context-free grammars.
Mot(s) Clé(s) : term rewriting, context-free tree language.
RR-2004-05 Proving Properties of Term Rewrite Systems via Logic Programs
S. Limet and G. Salzer
Résumé : Nous présentons une transfomation générale d'un système de réécriture (TRS) en un programme logique dont les déductions logiques correspondent à la réécriture basique. Certains TRS sont transfomé en cs-programmes, une classe de programmes logiques étudiée dans le cadre des langages de n-uplets d'arbres. En appliquant des resultats de décidabilité sur les cs-programmes on obtient de nouvelles classes de TRS qui ont des propriétés intéressantes comme la décidabilité de l'unification, des ensembles de descendants reguliers ou une représentation finies des ensembles de $R$-unificateurs. Nos résultats généralisent certains résultats connus dans le domaine de la réécriture.
Mot(s) Clé(s) : réécriture; programmation logique; langages d'arbres; décidabilité
RR-2004-06 A bulk-synchronous parallel process algebra
Armelle Merlin, Gaétan Hains
Résumé : L'algèbre de processus CCS (Calculus of Communicating System) est un modèle formel connu de synchronisation et communication utilisé pour l'analyse de sûreté et terminaison des protocoles ou programmes distribués, et plus récemment utilisé pour l'analyse de propriétés de sécurité. BSP (Bulk-synchronous parallelism) est un modèle de programmation de calcul data-parallèle. Il est utilisé pour concevoir, analyser et programmer des algorithmes massivement parallèles. Actuellement, de nombreuses applications nécessitent l'intégration de systèmes grid (distribués et parallèles) pour partager leurs resources à travers internet, avoir un accès global à des systèmes d'ordinateurs parallèles sécurisé, avoir des données confidentielles géographiquement réparties sur des systèmes aléatoirement accessibles... De tels services doivent garantir la sûreté, la terminaison et la sécurité tout en procurant des performances fiables et évolutives. Nous proposons donc un modèle formel pour combiner la performance parallèle et la concurrence en intégrant BSP dans la sémantique CCS. Nous généralisons son coût et présentons son application à des problèmes d'ordonnancement du meta-computing.
Mot(s) Clé(s) : Concurrence; Modèle de coût; Data-parallèlisme; BSP; CCS
RR-2004-07 Interactive rendering of massive terrains on PC cluster
V. Gouranton, S. Madougou, E. Melin, C. Nortet
Résumé : Nous décrivons un environnement parallèle pour le rendu interactif et continu de terrains très étendus. Nous définissons un schéma de parallélisation des algorithmes de gestion de niveau de détail pour les environnements à base de grappe de PC. Ce schéma se base sur la performance des grappes de PC récentes pour proposer une solution au problème de passage à l'échelle des algorithmes de gestion de niveau de détail. Pour accomplir ceci, nous proposons une méthode efficace de partitionnement de données à base de morceaux de terrain qui permet de réduire le déséquilbrage des charges et de résoudre le problème bien connu de simplification des frontières. Pendant l'exécution, les calculs de niveau de détail sont effectués en parallèle sur les noeuds de la grappe. Un culling hiérarchique combiné à un mécanisme de compression exploitant la cohérence temporelle est utilisé pour réduire, de manière drastique, le surcoût des communications inter-processus. Nous tenons en compte la qualité visuelle des algorithmes de gestion de niveau de détail en proposant un support pour le geomorphing et les textures. Nous sommes capables de rendre de manière interactive et sans à-coups des terrains composés de millions voire de milliards de polygones sur une grappe de 8 PC.
Mot(s) Clé(s) : algorithmes de gestion de niveau de détail, parallélisme, Rendu temps réel, Réalité Virtuelle
RR-2004-08 Sampling the evaluation of relational patterns
Agnès Braud, Teddy Turmeaux
Résumé : Le passage à l'échelle est un problème critique en fouille de données relationnelle. Ceci est principalement dû à l'évaluation de nombreux motifs. Le passage à l'échelle peut être facilité en diminuant soit le nombre de motifs évalués, soit le coût de leur évaluation. Nous étudions le second cas, et plus particulièrement l'utilisation de l'échantillonnage des données. Chaque motif vise à exprimer une connaissance sur des entités d'intérêt, qui doivent être comptées pour évaluer le motif. L'apprentissage en logique du premier ordre implique souvent un cadre multi-instances qui induit deux niveaux dans les données : entités et instances. Nous comparons différentes stratégies en fonction du niveau auquel l'échantillonnage est réalisé. Nous montrons l'importance de la stratégie choisie pour obtenir une meilleure estimation du comptage et ainsi permettre l'utilisation de l'échantillonnage en fouille de données relationnelle. Nous proposons également une famille d'estimateurs pour notre cadre de travail avec des bornes sur la précision obtenue.
Mot(s) Clé(s) : évaluation de motifs ; échantillonnage ; fouille de données relationnelle
RR-2004-09 Exact (exponential) algorithms for treewidth and minimum fill-in
Dieter KRATSCH, Fedor FOMIN, and Ioan TODINCA
Résumé : Nous montrons que pour les graphes à n sommets, la largeur arborescente et le remplissage minimum peuvent être calculés en temps O(poly(n) x .9601^n). Le resultat est basé sur une preuve combinatoire du fait que le nombre de séparateurs minimaux d'un graphe est O(n x 1.7087^n) et que le nombre de cliques maximales potentielles est O(n^4 x 1.9601^n). Pour la classe des graphes sans triplet astéroïde nous obtenons un algorithme de calcul de la largeur arborescente et du remplissage minimum avec une complexité de O(poly(n) x 1.4142^n).
Mot(s) Clé(s) :
RR-2004-10 A Declarative View of CSP Consistencies
Gérard Ferrand and Arnaud Lallouet
Résumé : Nous proposons une caractérisation en termes de modèles des approximations calculées par une consistance pendant la résolution d'un CSP sur les domaines finis. Nous proposons d'abord un premier programme CLP défini dont le plus grand point-fixe représente un état consistant. Ce cadre est suffisamment général pour être appliqué à l'arc-consistance, à la consistance de bornes ou à n'importe quel autre schéma d'approximation. De plus, motivé par d'autres approches visant à représenter les solutions d'un CSP par les modèles stables de programmes logiques, nous proposons un programme normal dont les modèles stables sont les états consistants du CSP.
Mot(s) Clé(s) : Programmation en Logique par Contraintes, CSP, Modèles stables
RR-2004-11 Proceedings of SASYFT 2004 (International Workshop on Security Analysis of Systems: Formalism and Tools). Paper version only.
S. Anantharaman (LIFO, Orléans), P. Gastin (LIAFA, Paris), G. Hains (LIFO, Orléans), J. Mullins (Ecole Polytechnique, Montréal), M. Rusinowitch (LORIA, Nancy).
Résumé :
Mot(s) Clé(s) :
RR-2004-12 How Useful are Dag Automata ?
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
Résumé : Tree automata are widely used in various contexts; and their emptiness problem is known to be decidable in polynomial time. Dag automata -- with or without labels -- are natural extensions of tree automata, which can also be used for solving problems. Our purpose in this paper is to show that algebraically they behave quite differently: the class of dag automata is not closed under complementation, dag automata are not determinizable, their membership problem turns out to be NP-complete, and universality is undecidable; and proving emptiness is NP-complete (even) for deterministic labeled dag automata.
Mot(s) Clé(s) : Tree automata, Determinism, Complementation, Universality, Decidability, Complexity, E-Unification.
RR-2004-13 A Proof System for Weak Congruence in Timed Pi Calculus
Jing Chen
Résumé : A complete axiomatization for weak congruence in the recursion-free fragment of timed Pi calculus is presented, with its soundness and completeness shown. The system consists of some basic algebraic axioms together with several inference rules. The system is first designed for late bisimulation, and can be modified for early bisimulation via simply replacing the rule concerning input action. The proof of the completeness result relies on the theory of Symbolic Bisimulation.
Mot(s) Clé(s) : Process Algebra, Mobile, Real-time, Bisimulation, Axiomatization, Symbolic Bisimulation
RR-2004-14 Distributed Level of Details for Graphics Clusters
Valérie Gouranton, Sébastien Limet, Souley Madougou, Emmanuel Melin
Résumé : Aujourd'hui, il existe de plus en plus de données volumineuses et complexes. Avec les avancées technologiques récentes, même des machines peuvent triater ces données. Les problèmes se posent lorsqu'il faut les visualiser, particulièrement dans les environnements temps-réel. les techniques de gestion de niveaux de détail (LOD) tentent d'apporter des solutions à ces problèmes mais jusqu'ici aucune solution satisfaisante n'a été proposée parce que toutes les solutions proposées se basent sur des architectures à mémoire partagée. Dans cet article, nous présentons une méthode qui tire profit des capacités de calcul et de stockage des grappes de PC pour permettre l'accélération des algorithmes de LOD et le passage à l'échelle des données pouvant être visualisées. La méthode commence par distribuer les données parmi un sous-ensemble de noeuds de la grappe appelés neouds de calcul. L'algorithme de LOD est exécutée en séquentiel sur les données locales au noeud. Les données résultats subissent alors un calcul d'intersection avec les cônes de vision. Ensuite, les données ayant changé dépuis les dernier frame sont déterminées et envoyées pour rendu à un sous-ensemble de noeuds appelés noeuds de visualisation. Sur ces noeuds, les données à rendre sont mises à jour grâce aux données reçues. De plus, le cadre enlève toute possibilité de goulot d'étranglement au noeud de visualisation en permettant l'utilisation d'un grand nombre de noeuds de visualisation.
Mot(s) Clé(s) : graphisme, rendu temps réel, gestion de niveaux de détail, rendu parallèle, parallélisme
Les rapports de recherche du LIFO en 2004
RR-2004-01
Manipulating Tree Tuple Languages by Transforming Logic Programs
Sebastien Limet and Gernot Salzer
Date : 2004-03-08
Résumé Télécharger
RR-2004-02
Can We Load Efficiently Dense datasets ?
Ansaf Salleb and Christel Vrain
Date : 2004-06-14
Résumé Télécharger
RR-2004-03
A Timed Synchronous Algebra for Information Flow Analysis
S. Anantharaman, J. Chen, G. Hains
Date : 2004-03-24
Résumé Télécharger
RR-2004-04
Context-Free Tree languages for Descendants
Pierre Réty, Julie Vuotto
Date : 2004-03-24
Résumé Télécharger
RR-2004-05
Proving Properties of Term Rewrite Systems via Logic Programs
S. Limet and G. Salzer
Date : 2004-11-29
Résumé Télécharger
RR-2004-06
A bulk-synchronous parallel process algebra
Armelle Merlin, Gaétan Hains
Date : 2004-06-14
Résumé Télécharger
RR-2004-07
Interactive rendering of massive terrains on PC cluster
V. Gouranton, S. Madougou, E. Melin, C. Nortet
Date : 2004-12-17
Résumé Télécharger
RR-2004-08
Sampling the evaluation of relational patterns
Agnès Braud, Teddy Turmeaux
Date : 2004-09-09
Résumé Télécharger
RR-2004-09
Exact (exponential) algorithms for treewidth and minimum fill-in
Dieter KRATSCH, Fedor FOMIN, and Ioan TODINCA
Date : 2004-05-14
Résumé Télécharger
RR-2004-10
A Declarative View of CSP Consistencies
Gérard Ferrand and Arnaud Lallouet
Date : 2004-05-14
Résumé Télécharger
RR-2004-11
Proceedings of SASYFT 2004
(International Workshop on Security Analysis of Systems: Formalism and Tools).
Paper version only.
S. Anantharaman (LIFO, Orléans), P. Gastin (LIAFA, Paris), G. Hains (LIFO, Orléans), J. Mullins (Ecole Polytechnique, Montréal), M. Rusinowitch (LORIA, Nancy).
Date : 2004-06-22
Résumé Télécharger
RR-2004-12
How Useful are Dag Automata ?
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
Date : 2004-07-23
Résumé Télécharger
RR-2004-13
A Proof System for Weak Congruence in Timed Pi Calculus
Jing Chen
Date : 2004-11-02
Résumé Télécharger
RR-2004-14
Distributed Level of Details for Graphics Clusters
Valérie Gouranton, Sébastien Limet, Souley Madougou, Emmanuel Melin
Date : 2004-12-17
Résumé Télécharger
Résumés des rapports de recherche
RR-2004-01 Manipulating Tree Tuple Languages by Transforming Logic Programs
Sebastien Limet and Gernot Salzer
Résumé : Nous introduisons la notion de définitions inductives sur des expression de langage comme cadre pour spécifier des langages de n-uplets d'arbres. Les définitions inductives et leurs sous-classes ont une correspondance naturelle avec des classes de programmes logiques et les opération su les langages de n-uplets d'arbres correspondent à la transformation de programmes logiques. Nous présentons un algorithme basé sur la notion de dépliage qui est capable de traiter plusieurs classes de languages de n-uplets de manière uniforme. Les preuves de terminaison de cet algorithme pour certaines classes de clauses se traduisent directement en propriétés de clôture de certaines opérations sur les languages de n-uplets ce qui permet d'obtenir de nouveaux resultats de décidabilité et de calculabilité.
Mot(s) Clé(s) : Langages d'arbres; programmation logique; décidabilité; transformation de programmes
RR-2004-02 Can We Load Efficiently Dense datasets ?
Ansaf Salleb and Christel Vrain
Résumé : We address the problem of representing and loading transactional datasets relying on a compressed representation of all the transactions of that dataset. We present an algorithm, named BoolLoader, to load transactional datasets and we give an experimental evaluation on both sparse and dense datasets. It shows that BoolLoader is efficient for loading dense datasets and gives a useful tool to evaluate the density of a dataset.
Mot(s) Clé(s) : Transactional datasets, boolean functions, decision diagrams, dense datasets, frequent itemsets.
RR-2004-03 A Timed Synchronous Algebra for Information Flow Analysis
S. Anantharaman, J. Chen, G. Hains
Résumé : The formalism of value-passing processes is well-suited for modeling and analyzing protocols. Timed processes account for the time consumed by the actions of the agents. In this paper we define process algebras with a view to cover both these aspects. Synchronous composition will be the central notion in our definition, since the the role played by the synchronous branches is crucial in the analysis of information flow on value-passing processes. Algebraically, parallel synchronous composition will be distributive over the choice operator, and by adding the action prefixes we get a PACUID-signature on which we define our process algebras. With such a vision, we propose an approach based on natural observation criteria and associated notions of non-interference, and show that they are well adapted for the confidentiality and authentication analysis of cryptographic protocols. Our algebra can also be extended naturally into a timed process algebra with a simple algebraic and operational semantics.
Mot(s) Clé(s) :
RR-2004-04 Context-Free Tree languages for Descendants
Pierre Réty, Julie Vuotto
Résumé : The preservation of regular tree languages through rewriting, has already been studied. In this paper, we study the preservation of context-free tree languages through rewriting, for constructor-based term rewrite systems. We give positive and negative results. Positive results are effective since we give algorithms to build context-free grammars.
Mot(s) Clé(s) : term rewriting, context-free tree language.
RR-2004-05 Proving Properties of Term Rewrite Systems via Logic Programs
S. Limet and G. Salzer
Résumé : Nous présentons une transfomation générale d'un système de réécriture (TRS) en un programme logique dont les déductions logiques correspondent à la réécriture basique. Certains TRS sont transfomé en cs-programmes, une classe de programmes logiques étudiée dans le cadre des langages de n-uplets d'arbres. En appliquant des resultats de décidabilité sur les cs-programmes on obtient de nouvelles classes de TRS qui ont des propriétés intéressantes comme la décidabilité de l'unification, des ensembles de descendants reguliers ou une représentation finies des ensembles de $R$-unificateurs. Nos résultats généralisent certains résultats connus dans le domaine de la réécriture.
Mot(s) Clé(s) : réécriture; programmation logique; langages d'arbres; décidabilité
RR-2004-06 A bulk-synchronous parallel process algebra
Armelle Merlin, Gaétan Hains
Résumé : L'algèbre de processus CCS (Calculus of Communicating System) est un modèle formel connu de synchronisation et communication utilisé pour l'analyse de sûreté et terminaison des protocoles ou programmes distribués, et plus récemment utilisé pour l'analyse de propriétés de sécurité. BSP (Bulk-synchronous parallelism) est un modèle de programmation de calcul data-parallèle. Il est utilisé pour concevoir, analyser et programmer des algorithmes massivement parallèles. Actuellement, de nombreuses applications nécessitent l'intégration de systèmes grid (distribués et parallèles) pour partager leurs resources à travers internet, avoir un accès global à des systèmes d'ordinateurs parallèles sécurisé, avoir des données confidentielles géographiquement réparties sur des systèmes aléatoirement accessibles... De tels services doivent garantir la sûreté, la terminaison et la sécurité tout en procurant des performances fiables et évolutives. Nous proposons donc un modèle formel pour combiner la performance parallèle et la concurrence en intégrant BSP dans la sémantique CCS. Nous généralisons son coût et présentons son application à des problèmes d'ordonnancement du meta-computing.
Mot(s) Clé(s) : Concurrence; Modèle de coût; Data-parallèlisme; BSP; CCS
RR-2004-07 Interactive rendering of massive terrains on PC cluster
V. Gouranton, S. Madougou, E. Melin, C. Nortet
Résumé : Nous décrivons un environnement parallèle pour le rendu interactif et continu de terrains très étendus. Nous définissons un schéma de parallélisation des algorithmes de gestion de niveau de détail pour les environnements à base de grappe de PC. Ce schéma se base sur la performance des grappes de PC récentes pour proposer une solution au problème de passage à l'échelle des algorithmes de gestion de niveau de détail. Pour accomplir ceci, nous proposons une méthode efficace de partitionnement de données à base de morceaux de terrain qui permet de réduire le déséquilbrage des charges et de résoudre le problème bien connu de simplification des frontières. Pendant l'exécution, les calculs de niveau de détail sont effectués en parallèle sur les noeuds de la grappe. Un culling hiérarchique combiné à un mécanisme de compression exploitant la cohérence temporelle est utilisé pour réduire, de manière drastique, le surcoût des communications inter-processus. Nous tenons en compte la qualité visuelle des algorithmes de gestion de niveau de détail en proposant un support pour le geomorphing et les textures. Nous sommes capables de rendre de manière interactive et sans à-coups des terrains composés de millions voire de milliards de polygones sur une grappe de 8 PC.
Mot(s) Clé(s) : algorithmes de gestion de niveau de détail, parallélisme, Rendu temps réel, Réalité Virtuelle
RR-2004-08 Sampling the evaluation of relational patterns
Agnès Braud, Teddy Turmeaux
Résumé : Le passage à l'échelle est un problème critique en fouille de données relationnelle. Ceci est principalement dû à l'évaluation de nombreux motifs. Le passage à l'échelle peut être facilité en diminuant soit le nombre de motifs évalués, soit le coût de leur évaluation. Nous étudions le second cas, et plus particulièrement l'utilisation de l'échantillonnage des données. Chaque motif vise à exprimer une connaissance sur des entités d'intérêt, qui doivent être comptées pour évaluer le motif. L'apprentissage en logique du premier ordre implique souvent un cadre multi-instances qui induit deux niveaux dans les données : entités et instances. Nous comparons différentes stratégies en fonction du niveau auquel l'échantillonnage est réalisé. Nous montrons l'importance de la stratégie choisie pour obtenir une meilleure estimation du comptage et ainsi permettre l'utilisation de l'échantillonnage en fouille de données relationnelle. Nous proposons également une famille d'estimateurs pour notre cadre de travail avec des bornes sur la précision obtenue.
Mot(s) Clé(s) : évaluation de motifs ; échantillonnage ; fouille de données relationnelle
RR-2004-09 Exact (exponential) algorithms for treewidth and minimum fill-in
Dieter KRATSCH, Fedor FOMIN, and Ioan TODINCA
Résumé : Nous montrons que pour les graphes à n sommets, la largeur arborescente et le remplissage minimum peuvent être calculés en temps O(poly(n) x .9601^n). Le resultat est basé sur une preuve combinatoire du fait que le nombre de séparateurs minimaux d'un graphe est O(n x 1.7087^n) et que le nombre de cliques maximales potentielles est O(n^4 x 1.9601^n). Pour la classe des graphes sans triplet astéroïde nous obtenons un algorithme de calcul de la largeur arborescente et du remplissage minimum avec une complexité de O(poly(n) x 1.4142^n).
Mot(s) Clé(s) :
RR-2004-10 A Declarative View of CSP Consistencies
Gérard Ferrand and Arnaud Lallouet
Résumé : Nous proposons une caractérisation en termes de modèles des approximations calculées par une consistance pendant la résolution d'un CSP sur les domaines finis. Nous proposons d'abord un premier programme CLP défini dont le plus grand point-fixe représente un état consistant. Ce cadre est suffisamment général pour être appliqué à l'arc-consistance, à la consistance de bornes ou à n'importe quel autre schéma d'approximation. De plus, motivé par d'autres approches visant à représenter les solutions d'un CSP par les modèles stables de programmes logiques, nous proposons un programme normal dont les modèles stables sont les états consistants du CSP.
Mot(s) Clé(s) : Programmation en Logique par Contraintes, CSP, Modèles stables
RR-2004-11 Proceedings of SASYFT 2004 (International Workshop on Security Analysis of Systems: Formalism and Tools). Paper version only.
S. Anantharaman (LIFO, Orléans), P. Gastin (LIAFA, Paris), G. Hains (LIFO, Orléans), J. Mullins (Ecole Polytechnique, Montréal), M. Rusinowitch (LORIA, Nancy).
Résumé :
Mot(s) Clé(s) :
RR-2004-12 How Useful are Dag Automata ?
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
Résumé : Tree automata are widely used in various contexts; and their emptiness problem is known to be decidable in polynomial time. Dag automata -- with or without labels -- are natural extensions of tree automata, which can also be used for solving problems. Our purpose in this paper is to show that algebraically they behave quite differently: the class of dag automata is not closed under complementation, dag automata are not determinizable, their membership problem turns out to be NP-complete, and universality is undecidable; and proving emptiness is NP-complete (even) for deterministic labeled dag automata.
Mot(s) Clé(s) : Tree automata, Determinism, Complementation, Universality, Decidability, Complexity, E-Unification.
RR-2004-13 A Proof System for Weak Congruence in Timed Pi Calculus
Jing Chen
Résumé : A complete axiomatization for weak congruence in the recursion-free fragment of timed Pi calculus is presented, with its soundness and completeness shown. The system consists of some basic algebraic axioms together with several inference rules. The system is first designed for late bisimulation, and can be modified for early bisimulation via simply replacing the rule concerning input action. The proof of the completeness result relies on the theory of Symbolic Bisimulation.
Mot(s) Clé(s) : Process Algebra, Mobile, Real-time, Bisimulation, Axiomatization, Symbolic Bisimulation
RR-2004-14 Distributed Level of Details for Graphics Clusters
Valérie Gouranton, Sébastien Limet, Souley Madougou, Emmanuel Melin
Résumé : Aujourd'hui, il existe de plus en plus de données volumineuses et complexes. Avec les avancées technologiques récentes, même des machines peuvent triater ces données. Les problèmes se posent lorsqu'il faut les visualiser, particulièrement dans les environnements temps-réel. les techniques de gestion de niveaux de détail (LOD) tentent d'apporter des solutions à ces problèmes mais jusqu'ici aucune solution satisfaisante n'a été proposée parce que toutes les solutions proposées se basent sur des architectures à mémoire partagée. Dans cet article, nous présentons une méthode qui tire profit des capacités de calcul et de stockage des grappes de PC pour permettre l'accélération des algorithmes de LOD et le passage à l'échelle des données pouvant être visualisées. La méthode commence par distribuer les données parmi un sous-ensemble de noeuds de la grappe appelés neouds de calcul. L'algorithme de LOD est exécutée en séquentiel sur les données locales au noeud. Les données résultats subissent alors un calcul d'intersection avec les cônes de vision. Ensuite, les données ayant changé dépuis les dernier frame sont déterminées et envoyées pour rendu à un sous-ensemble de noeuds appelés noeuds de visualisation. Sur ces noeuds, les données à rendre sont mises à jour grâce aux données reçues. De plus, le cadre enlève toute possibilité de goulot d'étranglement au noeud de visualisation en permettant l'utilisation d'un grand nombre de noeuds de visualisation.
Mot(s) Clé(s) : graphisme, rendu temps réel, gestion de niveaux de détail, rendu parallèle, parallélisme
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 