International Professional University of Technology in Nagoya Repository
Not a member yet
15131 research outputs found
Sort by
Formalization and closedness of finite dimensional subspaces
No full textInternational audienceThis article presents a Coq formalization of finite dimensional subspaces of Hilbert spaces: we prove that such subspaces are closed submodules. This result is one of the basic blocks to prove the correctness of the finite element method which approaches the solution of partial differential equations. The exact solution is valued in a continuous volume (Hilbert space) while the approximation is valued in a mesh (finite dimensional subspace) which fits the shape of the volume. When applied to a submodule which is finite dimensional, Lax– Milgram Theorem and Céa Lemma ensure the finite element method is sufficiently precise. We rely on filters as basis for topological reasoning: filters provide a very general framework to express local properties and limits. However, most such mathematical literature does not rely on filters, making our Coq formalization unusual
Modèles de prévision de la production d’électricité d’origine photovoltaïque : où sont les facteurs d’incertitude ?
No full textNational audienc
Bridging the Gap Between Imitation Learning and Inverse Reinforcement Learning
No full textInternational audience—Learning from Demonstrations (LfD) is a paradigm by which an apprentice agent learns a control policy for a dynamic environment by observing demonstrations delivered by an expert agent. It is usually implemented as either Imitation Learning (IL) or Inverse Reinforcement Learning (IRL) in the literature. On the one hand, IRL is a paradigm relying on Markov Decision Processes (MDPs), where the goal of the apprentice agent is to find a reward function from the expert demonstrations that could explain the expert behavior. On the other hand, IL consists in directly generalizing the expert strategy, observed in the demonstrations, to unvisited states (and it is therefore close to classification, when there is a finite set of possible decisions). While these two visions are often considered as opposite to each other, the purpose of this paper is to exhibit a formal link between these approaches from which new algorithms can be derived. We show that IL and IRL can be redefined in a way that they are equivalent, in the sense that there exists an explicit bijective operator (namely the inverse optimal Bellman operator) between their respective spaces of solutions. To do so, we introduce the set-policy framework which creates a clear link between IL and IRL. As a result, IL and IRL solutions making the best of both worlds are obtained. In addition, it is a unifying framework from which existing IL and IRL algorithms can be derived and which opens the way for IL methods able to deal with the environment's dynamics. Finally, the IRL algorithms derived from the set-policy framework are compared to algorithms belonging to the more common trajectory-matching family. Experiments demonstrate that the set-policy-based algorithms outperform both standard IRL and IL ones and result in more robust solutions
Spectroscopic and chemiometrics supported studies on discrimination, phase transition and concentration identifications of 1,2-propylene glycol solutions, and of a mixture of potassium acetate with 1,3-propanediol solutions as anti-icing fluids
No full textInternational audienc
An Automated Formal Process for Detecting Fault Injection Vulnerabilities in Binaries and Case Study on PRESENT
No full textInternational audienceRecently fault injection has increasingly been used both to attack software applications, and to test system robustness. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. This paper proposes a general process without these limitations that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy of this process is demonstrated by detecting vulnerabilities in the PRESENT binary
Testing Testbeds Towards Reproducibility
No full textInternational audienceWhen using testbeds in the context of experimental computer science, the ability to produce trustworthy and reproducible experiments results depends greatly on the trustworthiness of the infrastructure itself. Unfortunately, several factors many issues such as software misconfiguration, hardware heterogeneity, or service failures, can remain undetected and affect the quality of experimental results. This paper presents the design and implementation of an automated testbed testing framework. This framework was deployed in the context of the Grid'5000 project, and uncovered more than one hundred of issues.(see also https://hal.inria.fr/hal-01538682 for an extended version of this work
Secure Composition of PKIs with Public Key Protocols
No full textInternational audienceWe use symbolic formal models to study the composition of public key-based protocols with public key infras-tructures (PKIs). We put forth a minimal set of requirements which a PKI should satisfy and then identify several reasons why composition may fail. Our main results are positive and offer various trade-offs which align the guarantees provided by the PKI with those required by the analysis of protocol with which they are composed. We consider both the case of ideally distributed keys but also the case of more realistic PKIs. Our theorems are broadly applicable. Protocols are not limited to specific primitives and compositionality asks only for minimal requirements on shared ones. Secure composition holds with respect to arbitrary trace properties that can be specified within a reasonably powerful logic. For instance, secrecy and various forms of authentication can be expressed in this logic. Finally, our results alleviate the common yet demanding assumption that protocols are fully tagged
Micro-expression detection using integral projections
No full textInternational audienceAutomatic detection of micro-expression from a video is the first step in the micro-expression analysis. In this paper, we present a method addressing the micro-expression detection problem based on the differences in the Integral Projection (IP) of sequential frames. The method can detect the temporal location of the micro-expression. It involves an observation of the Chi-squared distance of the IP to measure the difference between frames. The main advantage of using IP for micro-expression detection is its low computation cost, which brings an important merit in real-time application. To evaluate our method, experiments are completed on two micro-expression databases namely CASME and CASME II. Results on these two datasets show that the proposed method obtains positive promising results with much less computation time against state-of-the-art methods. © 2017, Vaclav Skala Union Agency. All rights reserved