TY - CONF
AB - Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.
Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.
AU - Guerraoui, Rachid
AU - Thomas Henzinger
AU - Jobstmann, Barbara
AU - Vasu Singh
ID - 4384
TI - Model checking transactional memories
ER -
TY - JOUR
AU - Feraru, Elena
AU - Friml, Jirí
ID - 3037
IS - 4
JF - Plant Physiology
TI - PIN polar targeting
VL - 147
ER -
TY - JOUR
AB - A complete mitochondrial (mt) genome sequence was reconstructed from a 38,000 year-old Neandertal individual with 8341 mtDNA sequences identified among 4.8 Gb of DNA generated from ∼0.3 g of bone. Analysis of the assembled sequence unequivocally establishes that the Neandertal mtDNA falls outside the variation of extant human mtDNAs, and allows an estimate of the divergence date between the two mtDNA lineages of 660,000 ± 140,000 years. Of the 13 proteins encoded in the mtDNA, subunit 2 of cytochrome c oxidase of the mitochondrial electron transport chain has experienced the largest number of amino acid substitutions in human ancestors since the separation from Neandertals. There is evidence that purifying selection in the Neandertal mtDNA was reduced compared with other primate lineages, suggesting that the effective population size of Neandertals was small.
AU - Green, Richard E
AU - Malaspinas, Anna-Sapfo
AU - Krause, Johannes
AU - Briggs, Adrian W
AU - Johnson, Philip L
AU - Caroline Uhler
AU - Meyer, Matthias
AU - Good, Jeffrey M
AU - Maricic, Tomislav
AU - Stenzel, Udo
AU - Prüfer, Kay
AU - Siebauer, Michael F
AU - Burbano, Hernän A
AU - Ronan, Michael T
AU - Rothberg, Jonathan M
AU - Egholm, Michael
AU - Rudan, Pavao
AU - Brajković, Dejana
AU - Kućan, Željko
AU - Gušić, Ivan
AU - Wikström, Mårten K
AU - Laakkonen, Liisa J
AU - Kelso, Janet F
AU - Slatkin, Montgomery
AU - Pääbo, Svante H
ID - 3307
JF - Cell
TI - A complete neandertal mitochondrial genome sequence determined by highhhroughput sequencing
VL - 134
ER -
TY - JOUR
AB - We develop a new method for estimating effective population sizes, Ne, and selection coefficients, s, from time-series data of allele frequencies sampled from a single diallelic locus. The method is based on calculating transition probabilities, using a numerical solution of the diffusion process, and assuming independent binomial sampling from this diffusion process at each time point. We apply the method in two example applications. First, we estimate selection coefficients acting on the CCR5-Δ32 mutation on the basis of published samples of contemporary and ancient human DNA. We show that the data are compatible with the assumption of s = 0, although moderate amounts of selection acting on this mutation cannot be excluded. In our second example, we estimate the selection coefficient acting on a mutation segregating in an experimental phage population. We show that the selection coefficient acting on this mutation is ~0.43.
AU - Jonathan Bollback
AU - York, Thomas L
AU - Nielsen, Rasmus
ID - 3435
IS - 1
JF - Genetics
TI - Estimation of 2Nes From Temporal Allele Frequency Data
VL - 179
ER -
TY - CONF
AB - Simulation and bisimulation metrics for stochastic systems provide a quantitative gen- eralization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative μ-calculus and related probabilistic logics.
We present algorithms for computing the metrics on Markov decision processes (MDPs), turn- based stochastic games, and concurrent games. For turn-based games and MDPs, we provide a polynomial-time algorithm based on linear programming for the computation of the one-step metric distance between states. The algorithm improves on the previously known exponential-time algo- rithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known bound for Markov chains. For the bisimulation kernel of the metric, which corresponds to probabilistic bisimulation, our algorithm works in time O(n4) for both turn-based games and MDPs; improving the previously best known O(n9 · log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance between states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be accomplished via a reduction to the theory of real closed fields, involving a
formula with three quantifier alternations, yielding O(|G|O(|G|5)) time complexity, improving the previously known reduction with O(|G|O(|G|7)) time complexity. These algorithms can be iterated
to approximate the metrics using binary search.
AU - Chatterjee, Krishnendu
AU - De Alfaro, Luca
AU - Majumdar, Ritankar
AU - Raman, Vishwanath
ID - 3504
TI - Algorithms for game metrics
VL - 2
ER -
TY - JOUR
AB - Eukaryotic chromatin is separated into functional domains differentiated by posttranslational histone modifications, histone variants, and DNA methylation1–6. Methylation is associated with repression of transcriptional initiation in plants and animals, and is frequently found in transposable elements. Proper methylation patterns are critical for eukaryotic development4,5, and aberrant methylation-induced silencing of tumor suppressor genes is a common feature of human cancer7. In contrast to methylation, the histone variant H2A.Z is preferentially deposited by the Swr1 ATPase complex near 5′ ends of genes where it promotes transcriptional competence8–20. How DNA methylation and H2A.Z influence transcription remains largely unknown. Here we show that in the plant Arabidopsis thaliana, regions of DNA methylation are quantitatively deficient in H2A.Z. Exclusion of H2A.Z is seen at sites of DNA methylation in the bodies of actively transcribed genes and in methylated transposons. Mutation of the MET1 DNA methyltransferase, which causes both losses and gains of DNA methylation4,5, engenders opposite changes in H2A.Z deposition, while mutation of the PIE1 subunit of the Swr1 complex that deposits H2A.Z17 leads to genome-wide hypermethylation. Our findings indicate that DNA methylation can influence chromatin structure and effect gene silencing by excluding H2A.Z, and that H2A.Z protects genes from DNA methylation.
AU - ZILBERMAN, Daniel
AU - Coleman-Derr, Devin
AU - Ballinger, Tracy
AU - Henikoff, Steven
ID - 9457
IS - 7218
JF - Nature
KW - Multidisciplinary
SN - 0028-0836
TI - Histone H2A.Z and DNA methylation are mutually antagonistic chromatin marks
VL - 456
ER -
TY - JOUR
AB - It was recently shown by Hansen that the Wigner-Yanase entropy is, for general states of quantum systems, not subadditive with respect to decomposition into two subsystems, although this property is known to hold for pure states. We investigate the question whether the weaker property of subadditivity for pure states with respect to decomposition into more than two subsystems holds. This property would have interesting applications in quantum chemistry. We show, however, that it does not hold in general, and provide a counterexample.
AU - Robert Seiringer
ID - 2367
IS - 3
JF - Letters in Mathematical Physics
TI - On the failure of subadditivity of the Wigner-Yanase entropy
VL - 80
ER -
TY - JOUR
AB - After recalling briefly the connection between spontaneous symmetry breaking and off-diagonal long-range order for models of magnets a general proof of spontaneous breaking of gauge symmetry as a consequence of Bose-Einstein condensation is presented. The proof is based on a rigorous validation of Bogoliubov's c-number substitution for the k = 0 mode operator α0.
AU - Lieb, Élliott H
AU - Robert Seiringer
AU - Yngvason, Jakob
ID - 2370
IS - 3
JF - Reports on Mathematical Physics
TI - Bose-Einstein condensation and spontaneous symmetry breaking
VL - 59
ER -
TY - JOUR
AB - We give a proof of stability of relativistic matter with magnetic fields all the way up to the critical value of the nuclear charge Zα = 2/π.
AU - Frank, Rupert L
AU - Lieb, Élliott H
AU - Robert Seiringer
ID - 2371
IS - 2
JF - Communications in Mathematical Physics
TI - Stability of relativistic matter with magnetic fields for nuclear charges up to the critical value
VL - 275
ER -
TY - JOUR
AB - The increasing interest in the Müller density-matrix-functional theory has led us to a systematic mathematical investigation of its properties. This functional is similar to the Hartree-Fock (HF) functional, but with a modified exchange term in which the square of the density matrix γ(x, x′) is replaced by the square of γ1 2 (x, x′). After an extensive introductory discussion of density-matrix-functional theory we show, among other things, that this functional is convex (unlike the HF functional) and that energy minimizing γ 's have unique densities ρ(r), which is a physically desirable property often absent in HF theory. We show that minimizers exist if N≤Z, and derive various properties of the minimal energy and the corresponding minimizers. We also give a precise statement about the equation for the orbitals of γ, which is more complex than for HF theory. We state some open mathematical questions about the theory together with conjectured solutions.
AU - Frank, Rupert L
AU - Lieb, Élliott H
AU - Robert Seiringer
AU - Siedentop, Heinz K
ID - 2372
IS - 5
JF - Physical Review A - Atomic, Molecular, and Optical Physics
TI - Müller's exchange-correlation energy in density-matrix-functional theory
VL - 76
ER -
TY - JOUR
AB - For the BCS equation with local two-body interaction λV(x), we give a rigorous analysis of the asymptotic behavior of the critical temperature as γ"0. We derive necessary and sufficient conditions onV(x) for the existence of a nontrivial solution for all values of γ>0.
AU - Frank, Rupert L
AU - Hainzl, Christian
AU - Naboko, Serguei N
AU - Robert Seiringer
ID - 2373
IS - 4
JF - Journal of Geometric Analysis
TI - The critical temperature for the BCS equation at weak coupling
VL - 17
ER -
TY - JOUR
AB - We give a Cwikel-Lieb-Rozenblum type bound on the number of bound states of Schrödinger operators with matrix-valued potentials using the functional integral method of Lieb. This significantly improves the constant in this inequality obtained earlier by Hundertmark.
AU - Frank, Rupert L
AU - Lieb, Élliott H
AU - Robert Seiringer
ID - 2375
IS - 2-3
JF - Letters in Mathematical Physics
TI - Number of bound states of Schrödinger operators with matrix-valued potentials
VL - 82
ER -
TY - CHAP
AU - László Erdös
ED - Gesztesy, Fritz
ED - Deift, Percy
ED - Galvez, Percy
ED - Perry, Peter
ED - Schlag, Wilhelm
ID - 2705
T2 - Spectral Theory and Mathematical Physics: a Festschrift in Honor of Barry Simon's 60th Birthday
TI - Recent developments in quantum mechanics with magnetic fields
VL - 76
ER -
TY - JOUR
AB - In quantum information science, the phase of a wave function plays an important role in encoding information. Although most experiments in this field rely on dynamic effects to manipulate this information, an alternative approach is to use geometric phase, which has been argued to have potential fault tolerance. We demonstrated the controlled accumulation of a geometric phase, Berry's phase, in a superconducting qubit; we manipulated the qubit geometrically by means of microwave radiation and observed the accumulated phase in an interference experiment. We found excellent agreement with Berry's predictions and also observed a geometry-dependent contribution to dephasing.
AU - Leek, Peter J
AU - Johannes Fink
AU - Blais, Alexandre
AU - Bianchetti, R
AU - Göppl, M
AU - Gambetta, Jay M
AU - Schuster, David I
AU - Frunzio, Luigi
AU - Schoelkopf, Robert J
AU - Wallraff, Andreas
ID - 1762
IS - 5858
JF - Science
TI - Observation of Berry's phase in a solid-state qubit
VL - 318
ER -
TY - CONF
AB - We present a novel multi-scale representation and acquisition method for the animation of high-resolution facial geometry and wrinkles. We first acquire a static scan of the face including reflectance data at the highest possible quality. We then augment a traditional marker-based facial motion-capture system by two synchronized video cameras to track expression wrinkles. The resulting model consists of high-resolution geometry, motion-capture data, and expression wrinkles in 2D parametric form. This combination represents the facial shape and its salient features at multiple scales. During motion synthesis the motion-capture data deforms the high-resolution geometry using a linear shell-based mesh-deformation method. The wrinkle geometry is added to the facial base mesh using nonlinear energy optimization. We present the results of our approach for performance replay as well as for wrinkle editing.
AU - Bernd Bickel
AU - Botsch, Mario
AU - Angst, Roland
AU - Matusik, Wojciech
AU - Otaduy, Miguel A
AU - Pfister, Hanspeter
AU - Groß, Markus S
ID - 2091
TI - Multi scale capture of facial geometry and motion
ER -
TY - JOUR
AB - We present a novel multi-scale representation and acquisition method for the animation of high-resolution facial geometry and wrinkles. We first acquire a static scan of the face including reflectance data at the highest possible quality. We then augment a traditional marker-based facial motion-capture system by two synchronized video cameras to track expression wrinkles. The resulting model consists of high-resolution geometry, motion-capture data, and expression wrinkles in 2D parametric form. This combination represents the facial shape and its salient features at multiple scales. During motion synthesis the motion-capture data deforms the high-resolution geometry using a linear shell-based mesh-deformation method. The wrinkle geometry is added to the facial base mesh using nonlinear energy optimization. We present the results of our approach for performance replay as well as for wrinkle editing.
AU - Bernd Bickel
AU - Botsch, Mario
AU - Angst, Roland
AU - Matusik, Wojciech
AU - Otaduy, Miguel A
AU - Pfister, Hanspeter
AU - Groß, Markus S
ID - 2093
IS - 3
JF - ACM Transactions on Graphics
TI - Multi scale capture of facial geometry and motion
VL - 26
ER -
TY - JOUR
AB - We extend to infinite dimensions an explicit formula of Chill, Fašangová, Metafune, and Pallara for the optimal angle of analyticity of analytic Ornstein-Uhlenbeck semigroups. The main ingredient is an abstract representation of the Ornstein-Uhlenbeck operator in divergence form.
AU - Jan Maas
AU - van Neerven, Jan M
ID - 2118
IS - 3
JF - Archiv der Mathematik
TI - On analytic Ornstein-Uhlenbeck semigroups in infinite dimensions
VL - 89
ER -
TY - JOUR
AU - De La Bretèche, Régis
AU - Browning, Timothy D
ID - 221
IS - 1
JF - Michigan Mathematical Journal
TI - On Manin's conjecture for singular del Pezzo surfaces of degree four, I
VL - 55
ER -
TY - JOUR
AB - Acknowledgements. The authors are grateful to Ulrich Derenthal and Brendan Hassett for several useful conversations relating to universal torsors for singular del Pezzo surfaces. Special thanks are due to Roger Heath–Brown whose ideas led us to the proof of Lemma 6. The paper was finalised while the first author was at the École Normale Supérieure, and the second author was at Oxford University supported by EPSRC grant number GR/R93155/01. The hospitality and financial support of these institutions is gratefully acknowledged. Finally, the authors would like to thank the anonymous referee for his careful reading of the manuscript and numerous useful suggestions.
AU - de la Bretèche, Régis
AU - Timothy Browning
ID - 222
IS - 3
JF - Mathematical Proceedings of the Cambridge Philosophical Society
TI - On Manin's conjecture for singular del Pezzo surfaces of degree four, II
VL - 143
ER -
TY - JOUR
AB - Let Q be a non-singular diagonal quadratic form in at least four variables. We provide upper bounds for the number of integer solutions to the equation Q = 0, which lie in a box with sides of length 2B, as B → ∞. The estimates obtained are completely uniform in the coefficients of the form, and become sharper as they grow larger in modulus.
AU - Timothy Browning
ID - 223
IS - 1
JF - Monatshefte fur Mathematik
TI - Density of integer solutions to diagonal quadratic forms
VL - 152
ER -