Jurnal Edukasi
Not a member yet
4879 research outputs found
Sort by
Fourth-order energy-preserving locally implicit time discretization for linear wave equations
No full textInternational audienceA family of fourth order locally implicit schemes is presented as a special case of fourth order coupled implicit schemes for linear wave equations. The domain of interest is decomposed into several regions where different (explicit or implicit) fourth order time discretization are used. The coupling is based on a Lagrangian formulation on the boundaries between the several non conforming meshes of the regions. Fourth order accuracy follows from global energy identities. Numerical results in 1d and 2d illustrate the good behavior of the schemes and their potential for the simulation of realistic highly heterogeneous media or strongly refined geometries, for which using everywhere an explicit scheme can be extremely penalizing. Fourth order accuracy reduces the numerical dispersion inherent to implicit methods used with a large time step, and makes this family of schemes attractive compared to classical approaches
Tropicalizing Semialgebraic Pivoting Rules, Or How to Solve Mean Payoff Games in Polynomial Time on Average
No full textMinisymposia "Complexity Issues in Control Computation and Max-Plus Methods"International audienceWe introduce an algorithm which solves mean payoff games in polynomial time on average, assuming the distribution of the games satisfies a flip invariance property on the set of actions associated with every state. The algorithm is a tropical analogue of the shadow-vertex simplex algorithm, which solves mean payoff games via linear feasibility problems over the tropical semiring. The proof relies on the observation that certain semi-algebraic pivoting rules can be tropicalized
KGSrna: Efficient 3D Kinematics-Based Sampling for Nucleic Acids
No full textInternational audienceNoncoding ribonucleic acids (RNA) play a critical role in a wide variety of cellular processes, ranging from regulating gene expression to post-translational modification and protein synthesis. Their activity is modulated by highly dynamic exchanges between three-dimensional conformational substates, which are difficult to characterize experimentally and computationally. Here, we present an innovative, entirely kinematic computational procedure to efficiently explore the native ensemble of RNA molecules. Our procedure projects degrees of freedom onto a subspace of conformation space defined by distance constraints in the tertiary structure. The dimensionality reduction enables efficient exploration of conformational space. We show that the conformational distributions obtained with our method broadly sample the conformational landscape observed in NMR experiments. Compared to normal mode analysis-based exploration, our procedure diffuses faster through the experimental ensemble while also accessing conformational substates to greater precision. Our results suggest that conformational sampling with a highly reduced but fully atomistic representation of noncoding RNA expresses key features of their dynamic nature
Stochastic analysis of the time evolution of laminar-turbulent bands of plane Couette flow.
No full textInternational audienceThis article is concerned with the time evolution of the oblique laminar-turbulent bands of transitional plane Couette flow under the influence of turbulent noise. Our study is focused on the amplitude of modulation of turbulence (the bands). In order to guide the numerical study of the flow, we first perform an analytical and numerical analysis of a Stochastic Ginzburg-Landau (GL) equation for a complex order parameter. The modulus of this order parameter models the amplitude of modulation of turbulence. Firstly, we compute the autocorrelation function of said modulus once the band is established. Secondly, we perform a calculation of average and fluctuations around the exponential growth of the order parameter. This type of analysis is similar to the Stochastic Structural Stability Theory (S3T). We then perform numerical simulations of the Navier-Stokes equations in order to confront these predictions with the actual behaviour of the bands. Computation of the autocorrelation function of the modulation of turbulence shows quantitative agreement with the model: in the established band regime, the amplitude of modulation follows an Ornstein-Uhlenbeck process. In order to test the S3T predictions, we perform quench experiments, sudden decreases of the Reynolds number from uniform turbulence, in which modulation appears. We compute the average evolution of the amplitude of modulation and the fluctuations around it. We find good agreement between numerics and modeling. The average trajectory grows exponentially, at a rate clearly smaller than that of the formation of laminar holes. Meanwhile, the actual time evolution remains in a flaring envelope, centered on the average, and expanding at the same rate. These results provide further validation of the stochastic modeling for the time evolution of the bands for further studies. Besides, they stress on the difference between the oblique band formation and the formation of laminar holes
2D time−resolved measurement and modeling of electric fields associated with atmospheric pressure plasma streams propagation in dielectric capillaries
No full textInternational audienc
Tropical bounds for the eigenvalues of block structured matrices
No full textInternational audienceWe establish a log-majorization inequality, which relates the moduli of the eigenvalues of a block structured matrix with the tropical eigenvalues of the matrix obtained by replacing every block entry of the original matrix by its norm. This inequality involves combinatorial constants depending on the size and pattern of the matrix. Its proof relies on diagonal scalings, constructed from the optimal dual variables of a parametric optimal assignment problem
On the information leakage of differentially-private mechanisms
No full textInternational audienceDifferential privacy aims at protecting the privacy of participants instatistical databases. Roughly, a mechanism satisfies differential privacy ifthe presence or value of a single individual in the database does notsignificantly change the likelihood of obtaining a certain answer to anystatistical query posed by a data analyst. Differentially-private mechanisms areoften oblivious: first the query is processed on the database to produce a trueanswer, and then this answer is adequately randomized before being reported tothe data analyst. Ideally, a mechanism should minimize leakage, i.e., obfuscateas much as possible the link between reported answers and individuals' data,while maximizing utility, i.e., report answers as similar as possible to thetrue ones. These two goals, however, are in conflict with each other, thusimposing a trade-off between privacy and utility.In this paper we use quantitative information flow principles to analyze leakageand utility in oblivious differentially-private mechanisms. We introduce atechnique that exploits graph symmetries of the adjacency relation on databasesto derive bounds on the min-entropy leakage of the mechanism. We consider anotion of utility based on identity gain functions, which is closely related tomin-entropy leakage, and we derive bounds for it. Finally, given some graphsymmetries, we provide a mechanism that maximizes utility while preserving therequired level of differential privacy
Learning spatio-temporal trajectories from manifold-valued longitudinal data
No full textInternational audienceWe propose a Bayesian mixed-effects model to learn typical scenarios of changesfrom longitudinal manifold-valued data, namely repeated measurements of thesame objects or individuals at several points in time. The model allows to estimatea group-average trajectory in the space of measurements. Random variations ofthis trajectory result from spatiotemporal transformations, which allow changes inthe direction of the trajectory and in the pace at which trajectories are followed.The use of the tools of Riemannian geometry allows to derive a generic algorithmfor any kind of data with smooth constraints, which lie therefore on a Riemannianmanifold. Stochastic approximations of the Expectation-Maximization algorithmis used to estimate the model parameters in this highly non-linear setting. Themethod is used to estimate a data-driven model of the progressive impairments ofcognitive functions during the onset of Alzheimer’s disease. Experimental resultsshow that the model correctly put into correspondence the age at which each in-dividual was diagnosed with the disease, thus validating the fact that it effectivelyestimated a normative scenario of disease progression. Random effects provideunique insights into the variations in the ordering and timing of the succession ofcognitive impairments across different individuals
Modelling of the anthropogenic tritium transient and its decay product helium-3 in the Mediterranean Sea using a high-resolution regional model
No full textInternational audienceThis numerical study provides the first simulation of the anthropogenic tritium invasion and its decay product helium-3 (3 He) in the Mediterranean Sea. The simulation covers the entire tritium (3 H) transient generated by the atmospheric nuclear weapons tests performed in the 1950s and early 1960s and is run till 2011. Tritium, helium-3 and their derived age estimates are particularly suitable for studying intermediate and deep-water ventilation and spreading of water masses at intermediate/deep levels. The simulation is made using a high-resolution regional model NEMO (Nucleus for European Modelling of the Ocean), in a regional configuration for the Mediterranean Sea called MED12, forced at the surface with prescribed tritium evolution derived from observations. The simulation is compared to measurements of tritium and helium-3 performed along large-scale transects in the Mediterranean Sea during the last few decades on cruises of R/V Meteor: M5/6, M31/1, M44/4, M51/2, M84/3, and R/V Poseidon: 234. The results show that the input function used for the tritium generates a realistic distribution of the main hydrographic features of the Mediterranean Sea circulation. In the eastern basin, the results highlight the weak formation of Adriatic Deep Water in the model, which explains its weak contribution to the Eastern Mediterranean Deep Water (EMDW) in the Ionian sub-basin. It produces a realistic representation of the Eastern Mediterranean Transient (EMT) signal, simulating a deep-water formation in the Aegean sub-basin at the beginning of 1993, with a realistic timing of deep-water renewal in the eastern basin
Un cadre de définition de logiques calculatoires d’ordre supérieur
No full textThe main aim of this thesis is to make formal proofs more universal by expressing them in a common logical framework. More specifically, we use the lambda-Pi-calculus modulo rewriting, a lambda calculus equipped with dependent types and term rewriting, as a language for defining logics and expressing proofs in those logics. By representing propositions as types and proofs as programs in this language, we design translations of various systems in a way that is efficient and that preserves their meaning. These translations can then be used for independent proof checking and proof interoperability. In this work, we focus on the translation of logics based on type theory that allow both computation and higher-order quantification as steps of reasoning.Pure type systems are a well-known example of such computational higher-order systems, and form the basis of many modern proof assistants. We design a translation of functional pure type systems to the lambda-Pi-calculus modulo rewriting based on previous work by Cousineau and Dowek. The translation preserves typing, and in particular it therefore also preserves computation. We show that the translation is adequate by proving that it is conservative with respect to the original systems.We also adapt the translation to support universe cumulativity, a feature that is present in modern systems such as intuitionistic type theory and the calculus of inductive constructions. We propose to use explicit coercions to handle the implicit subtyping that is present in cumulativity, bridging the gap between pure type systems and type theory with universes à la Tarski. We also show how to preserve the expressivity of the original systems by adding equations to guarantee that types have a unique term representation, thus maintaining the completeness of the translation.The results of this thesis have been applied in automated proof translation tools. We implemented programs that automatically translate the proofs of HOL, Coq, and Matita, to Dedukti, a type-checker for the lambda-Pi-calculus modulo rewriting. These proofs can then be re-checked and combined together to form new theories in Dedukti, which thus serves as an independent proof checker and a platform for proof interoperability. We tested our tools on a variety of libraries. Experimental results confirm that our translations are correct and that they are efficient compared to the state of the art.L'objectif de cette thèse est de rendre les preuves formelles plus universelles en les exprimant dans un cadre logique commun. Plus précisément nous utilisons le lambda-Pi-calcul modulo réécriture, un lambda calcul équipé de types dépendants et de réécriture, comme langage pour définir des logiques et exprimer des preuves dans ces logiques. En représentant les propositions comme des types et les preuves comme des programmes dans ce langage, nous concevons des traductions de différents systèmes qui sont efficaces et qui préservent leur sens. Ces traductions peuvent ensuite être utilisées pour la vérification indépendante de preuves et l'interopérabilité de preuves. Dans ce travail, nous nous intéressons à la traduction de logiques basées sur la théorie des types qui permettent à la fois le calcul et la quantification d'ordre supérieur comme étapes de raisonnement.Les systèmes de types purs sont un exemple notoire de tels systèmes calculatoires d'ordre supérieur, et forment la base de plusieurs assistants de preuve modernes. Nous concevons une traduction des systèmes de types purs en lambda-Pi calcul modulo réécriture basée sur les travaux de Cousineau et Dowek. La traduction préserve le typage et en particulier préserve donc aussi l'évaluation et le calcul. Nous montrons que la traduction est adéquate en prouvant qu'elle est conservative par rapport au système original.Nous adaptons également la traduction pour inclure la cumulativité d'univers, qui est une caractéristique présente dans les systèmes modernes comme la théorie des types intuitionniste et le calcul des constructions inductives. Nous proposons d'utiliser des coercitions explicites pour traiter le sous-typage implicite présent dans la cumulativité, réconciliant ainsi les systèmes de types purs et la théorie des types avec univers à la Tarski. Nous montrons comment préserver l'expressivité des systèmes d'origine en ajoutant des équations pour garantir que les types ont une représentation unique en tant que termes, conservant ainsi la complétude de la traduction.Les résultats de cette thèse ont été appliqués dans des outils de traduction automatique de preuve. Nous avons implémenté des programmes qui traduisent automatiquement les preuves de HOL, Coq, et Matita, en Dedukti, un vérificateur de types pour le lambda-Pi-calcul modulo réécriture. Ces preuves peuvent ensuite être revérifiées et combinées ensemble pour former de nouvelles théories dans Dedukti, qui joue ainsi le rôle de vérificateur de preuves indépendant et de plateforme pour l'interopérabilité de preuves. Nous avons testé ces outils sur plusieurs bibliothèques. Les résultats expérimentaux confirment que nos traductions sont correctes et qu'elles sont efficaces comparées à l'état des outils actuels