arXiv subjects

Christian Müller

Publications and source records attributed to Christian Müller.

30 records · Page 2Linked to original sources

arXiv2019

How to Win First-Order Safety Games

First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Desirable properties of these systems such as functional correctness or noninterference have conveniently been formulated as safety properties. In order to automatically synthesize strategies that enforce safety or noninterference, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is in fact, equivalent to second-order quantifier elimination. For the important case of FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of noninterference properties. Based on general techniques for second-order quantifier elimination, we provide abstraction and refinement techniques in order to synthesize FO strategies that enforce safety. We demonstrate the usefulness of our approach by inferring nontrivial FO specifications in a leader election protocol as well as for paper assignment in a conference mangagement system to exclude unappreciated disclosure of reports.

cs.LO↗

arXiv2018

Uniform doping of graphene close to the charge neutrality point by polymer-assisted spontaneous assembly of molecular dopants

Tuning the charge carrier density of two-dimensional (2D) materials by incorporating dopants into the crystal lattice is a challenging task. An attractive alternative is the surface transfer doping by adsorption of molecules on 2D crystals, which can lead to ordered molecular arrays. However, such systems, demonstrated in ultra-high vacuum conditions (UHV), are often unstable in ambient conditions. Here we show that air-stable doping of epitaxial graphene on SiC - achieved by spin-coating deposition of 2,3,5,6-tetrafluoro-tetracyano-quino-dimethane (F4TCNQ) incorporated in poly (methyl-methacrylate) - proceeds via the spontaneous accumulation of dopants at the graphene-polymer interface and by the formation of a charge-transfer complex that yields low-disorder, charge-neutral graphene with carrier mobilities ~70,000 cm2/Vs at cryogenic temperatures. The assembly of dopants on 2D materials assisted by a polymer matrix, demonstrated by spin coating wafer-scale substrates in ambient conditions, opens up a scalable technological route towards expanding the functionality of 2D materials.

cond-mat.mes-hall↗

arXiv2018

A primer to numerical simulations: The perihelion motion of Mercury

Numerical simulations are playing an increasingly important role in modern science. In this work it is suggested to use a numerical study of the famous perihelion motion of the planet Mercury (one of the prime observables supporting Einsteins General Relativity) as a test case to teach numerical simulations to high school students. The paper includes details about the development of the code as well as a discussion of the visualization of the results. In addition a method is discussed that allows one to estimate the size of the effect as well as the uncertainty of the approach a priori. At the same time this enables the students to double check the results found numerically. The course is structured into a basic block and two further refinements which aim at more advanced students.

physics.ed-ph↗

arXiv2018

Prediction Error Bounds for Linear Regression With the TREX

The TREX is a recently introduced approach to sparse linear regression. In contrast to most well-known approaches to penalized regression, the TREX can be formulated without the use of tuning parameters. In this paper, we establish the first known prediction error bounds for the TREX. Additionally, we introduce extensions of the TREX to a more general class of penalties, and we provide a bound on the prediction error in this generalized setting. These results deepen the understanding of TREX from a theoretical perspective and provide new insights into penalized regression in general.

math.ST↗

arXiv2017

Verifying Security Policies in Multi-agent Workflows with Loops

We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number of participating agents. The information flow policies are specified in a temporal logic for hyperproperties. We show that the verification problem can be reduced to the satisfiability of a formula of first-order linear-time temporal logic, and provide decidability results for relevant classes of workflows and specifications. We report on experimental results obtained with an implementation of our approach on a series of benchmarks.

cs.LO↗

arXiv2016

Optical Phonons in Methylammonium Lead Halide Perovskites and Implications for Charge Transport

Lead-halide perovskites are promising materials for opto-electronic applications. Recent reports indicated that their mechanical and electronic properties are strongly affected by the lattice vibrations. Herein we report far-infrared spectroscopy measurements of CH$_{3}$NH$_{3}$Pb(I/Br/Cl)$_{3}$ thin films and single crystals at room temperature and a detailed quantitative analysis of the spectra. We find strong broadening and anharmonicity of the lattice vibrations for all three halide perovskites, which indicates dynamic disorder of the lead-halide cage at room temperature. We determine the frequencies of the transversal and longitudinal optical phonons, and use them to calculate, via appropriate models, the static dielectric constants, polaron masses, electron-phonon coupling constants, and upper limits for the phonon-scattering limited charge carrier mobilities. Within the limitations of the model used, we can place an upper limit of 200$\,$cm$^{2}$V$^{-1}$s$^{-1}$ for the room temperature charge carrier mobility in MAPbI$_{3}$ single crystals. Our findings are important for the basic understanding of charge transport processes and mechanical properties in metal halide perovskites.

cond-mat.mtrl-sci↗

arXiv2016

Non-convex Global Minimization and False Discovery Rate Control for the TREX

The TREX is a recently introduced method for performing sparse high-dimensional regression. Despite its statistical promise as an alternative to the lasso, square-root lasso, and scaled lasso, the TREX is computationally challenging in that it requires solving a non-convex optimization problem. This paper shows a remarkable result: despite the non-convexity of the TREX problem, there exists a polynomial-time algorithm that is guaranteed to find the global minimum. This result adds the TREX to a very short list of non-convex optimization problems that can be globally optimized (principal components analysis being a famous example). After deriving and developing this new approach, we demonstrate that (i) the ability of the preexisting TREX heuristic to reach the global minimum is strongly dependent on the difficulty of the underlying statistical problem, (ii) the new polynomial-time algorithm for TREX permits a novel variable ranking and selection scheme, (iii) this scheme can be incorporated into a rule that controls the false discovery rate (FDR) of included features in the model. To achieve this last aim, we provide an extension of the results of Barber & Candes (2015) to establish that the knockoff filter framework can be applied to the TREX. This investigation thus provides both a rare case study of a heuristic for non-convex optimization and a novel way of exploiting non-convexity for statistical inference.

stat.ML↗

arXiv2015

Three-dimensional spectral analysis of compositional heterogeneity at Arruntia crater on (4) Vesta using Dawn FC

We introduce an innovative three-dimensional spectral approach (three band parameter space with polyhedrons) that can be used for both qualitative and quantitative analyses improving the characterization of surface heterogeneity of (4) Vesta. It is an advanced and more robust methodology compared to the standard two-dimensional spectral approach (two band parameter space). The Dawn Framing Camera (FC) color data obtained during High Altitude Mapping Orbit (resolution ~ 60 m/pixel) is used. The main focus is on the howardite-eucrite-diogenite (HED) lithologies containing carbonaceous chondritic material, olivine, and impact-melt. The archived spectra of HEDs and their mixtures, from RELAB, HOSERLab and USGS databases as well as our laboratory-measured spectra are used for this study. Three-dimensional convex polyhedrons are defined using computed band parameter values of laboratory spectra. Polyhedrons based on the parameters of Band Tilt (R0.92μm/R0.96μm), Mid Ratio ((R0.75μm/R0.83μm)/(R0.83μm/R0.92μm)) and reflectance at 0.55 μm (R0.55μm) are chosen for the present analysis. An algorithm in IDL programming language is employed to assign FC data points to the respective polyhedrons. The Arruntia region in the northern hemisphere of Vesta is selected for a case study because of its geological and mineralogical importance. We observe that this region is eucrite-dominated howarditic in composition. The extent of olivine-rich exposures within an area of 2.5 crater radii is ~ 12% larger than the previous finding (Thangjam et al., 2014). Lithologies of nearly pure CM2-chondrite, olivine, glass, and diogenite are not found in this region. Our spectral approach can be extended to the entire Vestan surface to study the heterogeneous surface composition and its geology.

astro-ph.EP↗

arXiv2015

Don't Fall for Tuning Parameters: Tuning-Free Variable Selection in High Dimensions With the TREX

Lasso is a seminal contribution to high-dimensional statistics, but it hinges on a tuning parameter that is difficult to calibrate in practice. A partial remedy for this problem is Square-Root Lasso, because it inherently calibrates to the noise variance. However, Square-Root Lasso still requires the calibration of a tuning parameter to all other aspects of the model. In this study, we introduce TREX, an alternative to Lasso with an inherent calibration to all aspects of the model. This adaptation to the entire model renders TREX an estimator that does not require any calibration of tuning parameters. We show that TREX can outperform cross-validated Lasso in terms of variable selection and computational efficiency. We also introduce a bootstrapped version of TREX that can further improve variable selection. We illustrate the promising performance of TREX both on synthetic data and on a recent high-dimensional biological data set that considers riboflavin production in B. subtilis.

stat.ME↗

arXiv2015

Thermal Covert Channels on Multi-core Platforms

Side channels remain a challenge to information flow control and security in modern computing platforms. Resource partitioning techniques that minimise the number of shared resources among processes are often used to address this challenge. In this work, we focus on multi-core platforms and we demonstrate that even seemingly strong isolation techniques based on dedicated cores and memory can be circumvented through the use of thermal side channels. Specifically, we show that the processor core temperature can be used both as a side channel as well as a covert communication channel even when the system implements strong spatial and temporal partitioning. Our experiments on an x86-based platform demonstrate covert thermal channels that achieve up to 12.5 bps and a weak side channel that can detect processes executed on neighbouring cores. This work therefore shows a limitation in the isolation that can be achieved on existing multi-core systems.

cs.CR↗

arXiv2014

Topology Adaptive Graph Estimation in High Dimensions

We introduce Graphical TREX (GTREX), a novel method for graph estimation in high-dimensional Gaussian graphical models. By conducting neighborhood selection with TREX, GTREX avoids tuning parameters and is adaptive to the graph topology. We compare GTREX with standard methods on a new simulation set-up that is designed to assess accurately the strengths and shortcomings of different methods. These simulations show that a neighborhood selection scheme based on Lasso and an optimal (in practice unknown) tuning parameter outperforms other standard methods over a large spectrum of scenarios. Moreover, we show that GTREX can rival this scheme and, therefore, can provide competitive graph estimation without the need for tuning parameter calibration.

stat.ML↗

arXiv2007

Response of incompressible fractional quantum Hall states to magnetic and non-magnetic impurities

Using exact diagonalization we examine the response of several most prominent fractional quantum Hall states to a single local impurity. The 2/3 singlet state is found to be more inert than the polarized one in spite of its smaller incompressibility gap. Based on its spin-spin correlation functions we interpret it as a liquid of electron pairs with opposite spin. A comparison of different types of impurities, non-magnetic and magnetic, is presented.

cond-mat.mes-hall↗