- Contacts/Reaching LIFO
- Teaching
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
RR-2010-01 Systematic Development of Functional Bulk Synchronous Parallel Programs
Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue, Louis Gesbert
Abstract : With the current generalization of parallel architectures arises the concern of applying formal methods to parallelism, which allows specifications of parallel programs to be precisely stated and the correctness of an implementation to be verified. However, the complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. This calls for a strongly structured form of parallelism, which should not only ease programming by providing abstractions that conceal much of the complexity of parallel computation, but also provide a systematic way of developing practical programs from specification. Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of a proof assistant. The main technical contributions of this paper are as follows: We define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs~; We develop a set of useful theories in Coq for systematic and formal derivation of programs in BH from specification, and we provide a certified parallel implementation of BH in the parallel functional language Bulk Synchronous Parallel ML so that a certified BSP parallel program can be automatically extracted from the proof; We demonstrate with an example that our new framework can be very useful in practice to develop certified BSP parallel programs.
Keywords :
RR-2010-02 Functional Term Rewriting Systems
Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen
Abstract : This reseach report proposes the theoretical foundations of a new formal tool for symbolic verification of finite systems. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs). In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs). First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures. Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round Robin Mutex protocols,...) our tool is not only better than other rewriting tools such as Timbuk or Maude, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).
Keywords :
RR-2010-03 Discriminative Markov Logic Network Structure Learning based on Propositionalization and chi2-test
Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN
Abstract : In this paper we present a bottom-up discriminative algorithm to automatically learn Markov Logic Network structures. Our approach relies on a new propositionalization method that transforms the learning dataset into an approximative representation in the form of a boolean table. Using this table, the algorithm constructs a set of candidate clauses according to a chi2 independence test. To compute and choose clauses, we successively use two different optimization criteria, namely log-likelihood (LL) and conditional log-likelihood (CLL), in order to combine the efficiency of LL optimization algorithms together with the accuracy of CLL ones. First experiments show that our approach outperforms existing discriminative MLN structure learning algorithms.
Keywords : Markov Logic Network, Structure Learning, Relational Learning, Propositionalization, Inductive Logic Programming
RR-2010-04 Interactive and progressive constraint definition for dimensionality reduction and visualization
Lionel Martin, Matthieu Exbrayat, Guillaume Cleuziou, Frédéric Moal
Abstract : In this paper we focus on semi-supervised dimensionality reduction. Projecting and visualizing objects in a low dimension space is a current data analysis task. From another point of view, several works have been conducted recently, that constrain the projection space in order to optimize a given criteria (e.g. classification according to nearest neighbors). Nevertheless, none of those offers a satisfying interaction level. We thus propose an approach that offers to the user the ability to interactively add knowledge in the form of (di)similarity constraints among objects, when those appear either to close or to far in the current observation space. Such constraints can be added iteratively, the projection being modified after each new constraint. We propose several kinds of constraints and present a resolution method that derives from PCA. Experiments have been performed with both synthetic and usual datasets. They show that a satisfying representation (w.r.t a given quality criterion) can be obtained with a small set of constraints.
Keywords : semi supervised learning, dimensionality reduction.
RR-2010-05 Heuristic Method for Discriminative Structure Learning of Markov Logic Networks
Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN
Abstract : Markov Logic Networks (MLNs) combine Markov Networks and first-order logic by attaching weights to firstorder formulas and viewing them as templates for features of Markov Networks. Learning a MLN can be decomposed into structure learning and weights learning. In this paper, we present a heuristic-based algorithm to learn discriminative MLN structures automatically, directly from a training dataset. The algorithm heuristically transforms the relational dataset into boolean tables from which to build candidate clauses for learning the final MLN. Comparisons to the state-of-the-art structure learning algorithms for MLNs in the three real-world domains show that the proposed algorithm outperforms them in terms of the conditional log likelihood (CLL), and the area under the precision-recall curve (AUC).
Keywords : Markov Logic Network, Structure Learning, Discriminative learning, Relational Learning.
RR-2010-06 Security and Virtualization: a Survey
Patrice Clemente, Jonathan Rouzaud-Cornabas
Abstract : In this report, we investigate the security aspects and challenges about computer virtualization. In a few words, virtualization is what allows the execution of multiple operating systems on a single machine at the same time. A virtualization component can be viewed as a layer or a container making some kind of emulation, allowing to execute programs or operating systems on the virtualized layer, for example executing Microsoft Windows and Linux on one single machine at the same time. On one hand, as virtualization can provide a kind of isolation between users/applications/operating systems, it can address some security containment problems. But on the other hand, there exist today many security flaws and attacks focused on such systems, as the virtualization layer controls and monitors all virtualized applications/operating systems. The outline of this report is the following. We first review precisely all the various forms the virtualization layer and related components can take. And what technical aspects it involves. Then we survey more precisely all the vulnerabilities and exploits that currently exist or may appear in the near future. And then we study what are the proposed security protection by actual virtualization technologies. We conclude the report with what is remaining to be done and what are the forthcoming security challenges.
Keywords :
RR-2010-08 Fractal Parallelism: Solving SAT in bounded space and time.
Denys Duchier, Jérôme Durand-Lose, Maxime Senot.
Abstract : Abstract geometrical computation can solve NP-complete problems efficiently: any boolean constraint satisfaction problem, instance of SAT, can be solved in bounded space and time with simple geometrical constructions involving only drawing parallel lines on a Euclidean space-time plane. Complexity as the maximal length of a sequence of consecutive segments is quadratic. The geometrical algorithm achieves massive parallelism: an exponential number of cases are explored simultaneously. The construction relies on a fractal pattern and requires the same amount of space and time independently of the SAT formula.
Keywords : Abstract geometrical computation; Signal machine; Fractal; SAT; Massive parallelism; Model of computation.
RR-2010-09 ON REMOVABLE EDGES IN 3−CONNECTED CUBIC GRAPHS
Jean-Luc FOUQUET, Henri THUILLIER
Abstract : A removable edge in a 3−connected cubic graph G is an edge e = uv such that the cubic graph obtained from G \ {u, v} by adding an edge between the two neighbours of u distinct from v and an edge between the two neighbours of v disctinct from u is still 3−connected. Li and Wu [3] showed that a spanning tree in a 3−connected cubic graph avoids at least two removable edges, and Kang, Li and Wu [4] showed that a spanning tree contains at least two removable edges. We show here how to obtain these results easily from the structure of the sets of non removable edges and we give a characterization of the extremal graphs for these two results.
Keywords : Cubic graph, Removable edge, spanning trees
RR-2010-10 Tools for parsimonious edge-colouring of graphs with maximum degree three
J.L. Fouquet and J.M. Vanherpe
Abstract : In a graph G of maximum degree Delta let gamma denote the largest fraction of edges that can be Delta edge-coloured. Albertson and Haas showed that gamma >=13/15G is cubic . The notion of delta-minimum edge colouring was introduced by the first author in order to extend the so called parcimonious edge-colouring to graphs with maximum degree 3. We propose here an english translation of some structural properties already present in previous papers (in French) for delta-$minimum edge colourings of graphs with maximum degree 3.
Keywords : Cubic graph; Edge-colouring
RR-2010-11 A new bound for parsimonious edge-colouring of graphs with maximum degree three
J.L. Fouquet and J.M. Vanherpe
Abstract : In a graph G of maximum degree 3, let gamma(G) denote the largest fraction of edges that can be 3 edge-coloured. Rizzi showed that gamma(G) >=1-2/(3godd(G)) where godd(G) is the odd girth of G, when G is triangle-free. In a previous paper we extended that result to graph with maximum degree 3. We show here that gamma(G) >=1-2/(3good(G)+2), which leads to gamma(G) >= 15/17 when considering graphs with odd girth at least 5, distinct from the Petersen graph.
Keywords :
RR-2010-12 Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML
Wadoud Bousdira, Frédéric Loulergue, Louis Gesbert
Abstract : Bulk Synchronous Parallel ML (BSML) is an extension of the functional language Objective Caml to program Bulk Synchronous Parallel (BSP) algorithms. BSML programs are deterministic and deadlock free and have predictable performances. Parallelism is expressed with a set of four pure functional primitives on a parallel data structure called parallel vector. However, the programs are often hard to read and so to debug. We propose a new syntax and the associated semantics which allow to write shorter and more readable programs. The formalisation of the classical and new semantics as well as the proofs of confluence are established using the Coq proof assistant.
Keywords :
RR-2010-13 Comparaison des langages d'arbres dans le cadre de la substitution de services web
Joshua Amavi
Abstract : In this paper, we propose algorithm that extend tree inclusion to tree language inclusion. Our algorithm is useful in the context of web service substitution, and precisely in XML schema comparison. The algorithm used the synchronized-contextFree tree-tuple languages. The algorithm is proven correct and an implementation has done.
Keywords : Tree language, inclusion of XML schema, web service, synchronized-contextFree tree-tuple languages, regular expression
LIFO Research Report for Year 2010
RR-2010-01
Systematic Development of Functional Bulk Synchronous Parallel Programs
Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue, Louis Gesbert
Date : 2010-03-22
Abstract Download
RR-2010-02
Functional Term Rewriting Systems
Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen
Date : 2010-05-18
Abstract Download
RR-2010-03
Discriminative Markov Logic Network Structure Learning based on Propositionalization and chi2-test
Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN
Date : 2010-05-21
Abstract Download
RR-2010-04
Interactive and progressive constraint definition for dimensionality reduction and visualization
Lionel Martin, Matthieu Exbrayat, Guillaume Cleuziou, Frédéric Moal
Date : 2010-05-21
Abstract Download
RR-2010-05
Heuristic Method for Discriminative Structure Learning of Markov Logic Networks
Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN
Date : 2010-09-02
Abstract Download
RR-2010-06
Security and Virtualization: a Survey
Patrice Clemente, Jonathan Rouzaud-Cornabas
Date : 2010-12-31
Abstract Download
RR-2010-08
Fractal Parallelism: Solving SAT in bounded space and time.
Denys Duchier, Jérôme Durand-Lose, Maxime Senot.
Date : 2010-09-16
Abstract Download
RR-2010-09
ON REMOVABLE EDGES IN 3−CONNECTED CUBIC GRAPHS
Jean-Luc FOUQUET, Henri THUILLIER
Date : 2010-09-09
Abstract Download
RR-2010-10
Tools for parsimonious edge-colouring of graphs with maximum degree three
J.L. Fouquet and J.M. Vanherpe
Date : 2010-10-12
Abstract Download
RR-2010-11
A new bound for parsimonious edge-colouring of graphs with maximum degree three
J.L. Fouquet and J.M. Vanherpe
Date : 2010-10-12
Abstract Download
RR-2010-12
Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML
Wadoud Bousdira, Frédéric Loulergue, Louis Gesbert
Date : 2010-11-02
Abstract Download
RR-2010-13
Comparaison des langages d'arbres dans le cadre de la substitution de services web
Joshua Amavi
Date : 2010-12-17
Abstract Download
Abstracts of Research Reports
RR-2010-01 Systematic Development of Functional Bulk Synchronous Parallel Programs
Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue, Louis Gesbert
Abstract : With the current generalization of parallel architectures arises the concern of applying formal methods to parallelism, which allows specifications of parallel programs to be precisely stated and the correctness of an implementation to be verified. However, the complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. This calls for a strongly structured form of parallelism, which should not only ease programming by providing abstractions that conceal much of the complexity of parallel computation, but also provide a systematic way of developing practical programs from specification. Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of a proof assistant. The main technical contributions of this paper are as follows: We define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs~; We develop a set of useful theories in Coq for systematic and formal derivation of programs in BH from specification, and we provide a certified parallel implementation of BH in the parallel functional language Bulk Synchronous Parallel ML so that a certified BSP parallel program can be automatically extracted from the proof; We demonstrate with an example that our new framework can be very useful in practice to develop certified BSP parallel programs.
Keywords :
RR-2010-02 Functional Term Rewriting Systems
Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen
Abstract : This reseach report proposes the theoretical foundations of a new formal tool for symbolic verification of finite systems. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs). In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs). First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures. Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round Robin Mutex protocols,...) our tool is not only better than other rewriting tools such as Timbuk or Maude, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).
Keywords :
RR-2010-03 Discriminative Markov Logic Network Structure Learning based on Propositionalization and chi2-test
Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN
Abstract : In this paper we present a bottom-up discriminative algorithm to automatically learn Markov Logic Network structures. Our approach relies on a new propositionalization method that transforms the learning dataset into an approximative representation in the form of a boolean table. Using this table, the algorithm constructs a set of candidate clauses according to a chi2 independence test. To compute and choose clauses, we successively use two different optimization criteria, namely log-likelihood (LL) and conditional log-likelihood (CLL), in order to combine the efficiency of LL optimization algorithms together with the accuracy of CLL ones. First experiments show that our approach outperforms existing discriminative MLN structure learning algorithms.
Keywords : Markov Logic Network, Structure Learning, Relational Learning, Propositionalization, Inductive Logic Programming
RR-2010-04 Interactive and progressive constraint definition for dimensionality reduction and visualization
Lionel Martin, Matthieu Exbrayat, Guillaume Cleuziou, Frédéric Moal
Abstract : In this paper we focus on semi-supervised dimensionality reduction. Projecting and visualizing objects in a low dimension space is a current data analysis task. From another point of view, several works have been conducted recently, that constrain the projection space in order to optimize a given criteria (e.g. classification according to nearest neighbors). Nevertheless, none of those offers a satisfying interaction level. We thus propose an approach that offers to the user the ability to interactively add knowledge in the form of (di)similarity constraints among objects, when those appear either to close or to far in the current observation space. Such constraints can be added iteratively, the projection being modified after each new constraint. We propose several kinds of constraints and present a resolution method that derives from PCA. Experiments have been performed with both synthetic and usual datasets. They show that a satisfying representation (w.r.t a given quality criterion) can be obtained with a small set of constraints.
Keywords : semi supervised learning, dimensionality reduction.
RR-2010-05 Heuristic Method for Discriminative Structure Learning of Markov Logic Networks
Quang-Thang DINH, Matthieu EXBRAYAT, Christel VRAIN
Abstract : Markov Logic Networks (MLNs) combine Markov Networks and first-order logic by attaching weights to firstorder formulas and viewing them as templates for features of Markov Networks. Learning a MLN can be decomposed into structure learning and weights learning. In this paper, we present a heuristic-based algorithm to learn discriminative MLN structures automatically, directly from a training dataset. The algorithm heuristically transforms the relational dataset into boolean tables from which to build candidate clauses for learning the final MLN. Comparisons to the state-of-the-art structure learning algorithms for MLNs in the three real-world domains show that the proposed algorithm outperforms them in terms of the conditional log likelihood (CLL), and the area under the precision-recall curve (AUC).
Keywords : Markov Logic Network, Structure Learning, Discriminative learning, Relational Learning.
RR-2010-06 Security and Virtualization: a Survey
Patrice Clemente, Jonathan Rouzaud-Cornabas
Abstract : In this report, we investigate the security aspects and challenges about computer virtualization. In a few words, virtualization is what allows the execution of multiple operating systems on a single machine at the same time. A virtualization component can be viewed as a layer or a container making some kind of emulation, allowing to execute programs or operating systems on the virtualized layer, for example executing Microsoft Windows and Linux on one single machine at the same time. On one hand, as virtualization can provide a kind of isolation between users/applications/operating systems, it can address some security containment problems. But on the other hand, there exist today many security flaws and attacks focused on such systems, as the virtualization layer controls and monitors all virtualized applications/operating systems. The outline of this report is the following. We first review precisely all the various forms the virtualization layer and related components can take. And what technical aspects it involves. Then we survey more precisely all the vulnerabilities and exploits that currently exist or may appear in the near future. And then we study what are the proposed security protection by actual virtualization technologies. We conclude the report with what is remaining to be done and what are the forthcoming security challenges.
Keywords :
RR-2010-08 Fractal Parallelism: Solving SAT in bounded space and time.
Denys Duchier, Jérôme Durand-Lose, Maxime Senot.
Abstract : Abstract geometrical computation can solve NP-complete problems efficiently: any boolean constraint satisfaction problem, instance of SAT, can be solved in bounded space and time with simple geometrical constructions involving only drawing parallel lines on a Euclidean space-time plane. Complexity as the maximal length of a sequence of consecutive segments is quadratic. The geometrical algorithm achieves massive parallelism: an exponential number of cases are explored simultaneously. The construction relies on a fractal pattern and requires the same amount of space and time independently of the SAT formula.
Keywords : Abstract geometrical computation; Signal machine; Fractal; SAT; Massive parallelism; Model of computation.
RR-2010-09 ON REMOVABLE EDGES IN 3−CONNECTED CUBIC GRAPHS
Jean-Luc FOUQUET, Henri THUILLIER
Abstract : A removable edge in a 3−connected cubic graph G is an edge e = uv such that the cubic graph obtained from G \ {u, v} by adding an edge between the two neighbours of u distinct from v and an edge between the two neighbours of v disctinct from u is still 3−connected. Li and Wu [3] showed that a spanning tree in a 3−connected cubic graph avoids at least two removable edges, and Kang, Li and Wu [4] showed that a spanning tree contains at least two removable edges. We show here how to obtain these results easily from the structure of the sets of non removable edges and we give a characterization of the extremal graphs for these two results.
Keywords : Cubic graph, Removable edge, spanning trees
RR-2010-10 Tools for parsimonious edge-colouring of graphs with maximum degree three
J.L. Fouquet and J.M. Vanherpe
Abstract : In a graph G of maximum degree Delta let gamma denote the largest fraction of edges that can be Delta edge-coloured. Albertson and Haas showed that gamma >=13/15G is cubic . The notion of delta-minimum edge colouring was introduced by the first author in order to extend the so called parcimonious edge-colouring to graphs with maximum degree 3. We propose here an english translation of some structural properties already present in previous papers (in French) for delta-$minimum edge colourings of graphs with maximum degree 3.
Keywords : Cubic graph; Edge-colouring
RR-2010-11 A new bound for parsimonious edge-colouring of graphs with maximum degree three
J.L. Fouquet and J.M. Vanherpe
Abstract : In a graph G of maximum degree 3, let gamma(G) denote the largest fraction of edges that can be 3 edge-coloured. Rizzi showed that gamma(G) >=1-2/(3godd(G)) where godd(G) is the odd girth of G, when G is triangle-free. In a previous paper we extended that result to graph with maximum degree 3. We show here that gamma(G) >=1-2/(3good(G)+2), which leads to gamma(G) >= 15/17 when considering graphs with odd girth at least 5, distinct from the Petersen graph.
Keywords :
RR-2010-12 Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML
Wadoud Bousdira, Frédéric Loulergue, Louis Gesbert
Abstract : Bulk Synchronous Parallel ML (BSML) is an extension of the functional language Objective Caml to program Bulk Synchronous Parallel (BSP) algorithms. BSML programs are deterministic and deadlock free and have predictable performances. Parallelism is expressed with a set of four pure functional primitives on a parallel data structure called parallel vector. However, the programs are often hard to read and so to debug. We propose a new syntax and the associated semantics which allow to write shorter and more readable programs. The formalisation of the classical and new semantics as well as the proofs of confluence are established using the Coq proof assistant.
Keywords :
RR-2010-13 Comparaison des langages d'arbres dans le cadre de la substitution de services web
Joshua Amavi
Abstract : In this paper, we propose algorithm that extend tree inclusion to tree language inclusion. Our algorithm is useful in the context of web service substitution, and precisely in XML schema comparison. The algorithm used the synchronized-contextFree tree-tuple languages. The algorithm is proven correct and an implementation has done.
Keywords : Tree language, inclusion of XML schema, web service, synchronized-contextFree tree-tuple languages, regular expression
University of Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 