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

Lifo > LIFO Research Report for Year 2004

 Site en Français



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



Go to Research Reports of Year : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018

LIFO Research Report for Year 2004


RR-2004-01 Manipulating Tree Tuple Languages by Transforming Logic Programs
Sebastien Limet and Gernot Salzer
Date : 2004-03-08
Abstract Download

RR-2004-02 Can We Load Efficiently Dense datasets ?
Ansaf Salleb and Christel Vrain
Date : 2004-06-14
Abstract Download

RR-2004-03 A Timed Synchronous Algebra for Information Flow Analysis
S. Anantharaman, J. Chen, G. Hains
Date : 2004-03-24
Abstract Download

RR-2004-04 Context-Free Tree languages for Descendants
Pierre Réty, Julie Vuotto
Date : 2004-03-24
Abstract Download

RR-2004-05 Proving Properties of Term Rewrite Systems via Logic Programs
S. Limet and G. Salzer
Date : 2004-11-29
Abstract Download

RR-2004-06 A bulk-synchronous parallel process algebra
Armelle Merlin, Gaétan Hains
Date : 2004-06-14
Abstract Download

RR-2004-07 Interactive rendering of massive terrains on PC cluster
V. Gouranton, S. Madougou, E. Melin, C. Nortet
Date : 2004-12-17
Abstract Download

RR-2004-08 Sampling the evaluation of relational patterns
Agnès Braud, Teddy Turmeaux
Date : 2004-09-09
Abstract Download

RR-2004-09 Exact (exponential) algorithms for treewidth and minimum fill-in
Dieter KRATSCH, Fedor FOMIN, and Ioan TODINCA
Date : 2004-05-14
Abstract Download

RR-2004-10 A Declarative View of CSP Consistencies
Gérard Ferrand and Arnaud Lallouet
Date : 2004-05-14
Abstract Download

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
Abstract Download

RR-2004-12 How Useful are Dag Automata ?
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
Date : 2004-07-23
Abstract Download

RR-2004-13 A Proof System for Weak Congruence in Timed Pi Calculus
Jing Chen
Date : 2004-11-02
Abstract Download

RR-2004-14 Distributed Level of Details for Graphics Clusters
Valérie Gouranton, Sébastien Limet, Souley Madougou, Emmanuel Melin
Date : 2004-12-17
Abstract Download


Abstracts of Research Reports


RR-2004-01 Manipulating Tree Tuple Languages by Transforming Logic Programs
Sebastien Limet and Gernot Salzer
Abstract : We introduce inductive definitions over language expressions as a framework for specifying tree tuple languages. Inductive definitions and their sub-classes correspond naturally to classes of logic programs, and operations on tree tuple languages correspond to the transformation of logic programs. We present an algorithm based on unfolding and definition introduction that is able to deal with several classes of tuple languages in a uniform way. Termination proofs for clause classes translate directly to closure properties of tuple languages, leading to new decidability and computability results for the latter.
Keywords : Tree languages; logic programming; decidability; program transformation

RR-2004-02 Can We Load Efficiently Dense datasets ?
Ansaf Salleb and Christel Vrain
Abstract : 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.
Keywords : 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
Abstract : 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.
Keywords :

RR-2004-04 Context-Free Tree languages for Descendants
Pierre Réty, Julie Vuotto
Abstract : 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.
Keywords : term rewriting, context-free tree language.

RR-2004-05 Proving Properties of Term Rewrite Systems via Logic Programs
S. Limet and G. Salzer
Abstract : We present a general translation of term rewrite systems (TRS) to logic programs such that basic rewriting derivations become logic deductions. Certain TRS result in so-called cs-programs, which were originally studied in the context of constraint systems and tree tuple languages. By applying decidability and computability results of cs-programs we obtain new classes of TRS that have nice properties like decidability of unification, regular sets of descendants or finite representations of $R$-unifiers. Our findings generalize former results in the field of term rewriting.
Keywords : Term rewriting; logic programming, tree languages, decidability

RR-2004-06 A bulk-synchronous parallel process algebra
Armelle Merlin, Gaétan Hains
Abstract : The CCS (Calculus of Communicating System) process algebra is a well-known formal model of synchronization and communication, useful for the analysis of safety and liveness in protocols or distributed programs, and in more recent works their security properties. BSP (Bulk-synchronous parallelism) is an algorithm- and programming model of data-parallel computation. It is useful for the design, analysis and programming of scalable parallel algorithms. Many current evolutions require the integration of distributed- and parallel programming: grid systems for sharing ressources across the internet, secure and reliable global access to parallel computer systems, geographic distribution of confidential data on randomly accessible systems, etc. Such software services much provide guarantees of safety, liveness, security together with scalable and reliable performance. Formal models are therefore needed to combine parallel performance and concurrent behaviour. With this goal in mind, we propose here an integration of BSP with CCS semantics, generalize its cost (performance) model and sketch its application to scheduling problems in meta-computing.
Keywords : Concurrency; cost model; data-parallelism; CCS; BSP

RR-2004-07 Interactive rendering of massive terrains on PC cluster
V. Gouranton, S. Madougou, E. Melin, C. Nortet
Abstract : We describe a parallel framework for interactive smooth rendering of massive terrains. We define a parallelization scheme for level of detail algorithms in cluster-based environments. The scheme relies on modern PC clusters capabilities to address the scalability issue of level of detail algorithms. To achieve this, we propose an efficient tile-based data partitioning method that allows both reducing load imbalance and solving the well-known border problem. At runtime level of detail computations are performed in parallel on cluster nodes. A hierarchical view frustum culling combined to a compression mechanism harnessing the frame-to-frame coherence are used to drastically reduce the inter-tasks communication overhead. We take into account level of detail algorithms visual quality issue by providing geomorphing and texturing supports. We are able to interactively and smoothly render terrains composed of hundreds of millions to billions of polygons on a cluster of 8 PCs.
Keywords : LOD algorithms, parallelism, Real-time rendering, Virtual Reality

RR-2004-08 Sampling the evaluation of relational patterns
Agnès Braud, Teddy Turmeaux
Abstract : Scalability is a critical problem in relational Data Mining. This is mainly due to the evaluation of many patterns. Tractability can be achieved by decreasing either the number of patterns evaluated, or the cost of their evaluation. We investigate the second case, and more precisely the use of data sampling. Each pattern aims to express a piece of knowledge on some entities of interest, that have to be counted to evaluate the pattern. Learning in first order logic often implies a multi-instance setting that induces two levels in the data: entities and instances. We compare different strategies according to the level at which sampling is done. We show the importance of the strategy chosen in order to achieve a better estimate of thecounting and thus to enable the use of sampling in relational DataMining. We also propose a family of estimators for our framework together with some bounds on the accuracy obtained.
Keywords : pattern evaluation; sampling; relational data mining

RR-2004-09 Exact (exponential) algorithms for treewidth and minimum fill-in
Dieter KRATSCH, Fedor FOMIN, and Ioan TODINCA
Abstract : We show that for a graph G on n vertices its treewidth and minimum fill-in can be computed in O(poly(n) x 1.9601^n) time. Our result is based on a combinatorial proof that the number of minimal separators in a graph is O(n x 1.7087^n) and that the number of potential maximal cliques is O(n^4 x 1.9601^n). For the class of AT-free graphs we obtain O(poly(n) x 1.4142^n) time algorithm computing treewidth and minimum fill-in.
Keywords :

RR-2004-10 A Declarative View of CSP Consistencies
Gérard Ferrand and Arnaud Lallouet
Abstract : We provide here a model-theoretic characterization of the approximations computed by a consistency while solving a finite domain CSP. At first, we propose a definite CLP program which allows to characterize the computed approximation by its fixpoints. This framework is general enough to be applied to (hyper)arc-consistency, bound-consistency or any approximation scheme. Moreover, motivated by other approaches of CSP representations by logic programs with stable model semantics, the computed approximation is also represented in a natural way by the stable models of another (normal) CLP program.
Keywords : Constraint Logic Programming; CSP; Consistencies; Stable models

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).
Abstract :
Keywords :

RR-2004-12 How Useful are Dag Automata ?
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
Abstract : 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.
Keywords : Tree automata, Determinism, Complementation, Universality, Decidability, Complexity, E-Unification.

RR-2004-13 A Proof System for Weak Congruence in Timed Pi Calculus
Jing Chen
Abstract : 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.
Keywords : 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
Abstract : Today, large and complex data sets are commonplace. With enhancements in electronic components, even low-end computers are able to process large part of them. But problems arise when one has to visualize such data sets, especially in real time environments. Level of detail (LOD) techniques try to answer these issues, but so far, there is no satisfactory solutions because most of the solutions are designed for shared memory machines. In this paper, we present a method that benefits from cluster computing power and storage capacities to speed up LOD algorithms and to scale data sets that are processed. The method begins by distributing data among some cluster nodes called computation nodes. There, LOD algorithm is executed using locally held data. Results are culled against view frusta, modified data only are determinated and sent for visualization to a subset of nodes called visualization nodes. Here, rendered data are updated using received data. Furthermore, the scheme removes the possible bottleneck on visualization node by permitting the use of a potentially high number of visualization nodes.
Keywords : computer graphics, real-time rendering, level of detail, parallel rendering, parallelism