@inproceedings{4383, abstract = {Pseudo-code descriptions of STMs assume sequentially consistent program execution and atomicity of high-level STM operations like read, write, and commit. These assumptions are often violated in realistic settings, as STM implementations run on relaxed memory models, with the atomicity of operations as provided by the hardware. This paper presents the first approach to verify STMs under relaxed memory models with atomicity of 32 bit loads and stores, and read-modify-write operations. We present RML, a new high-level language for expressing concurrent algorithms with a hardware-level atomicity of instructions, and whose semantics is parametrized by various relaxed memory models. We then present our tool, FOIL, which takes as input the RML description of an STM algorithm and the description of a memory model, and automatically determines the locations of fences, which if inserted, ensure the correctness of the STM algorithm under the given memory model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of sequential consistency, total store order, partial store order, and relaxed memory order.}, author = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh}, pages = {321 -- 336}, publisher = {Springer}, title = {{Software transactional memory on relaxed memory models}}, doi = {10.1007/978-3-642-02658-4_26}, volume = {5643}, year = {2009}, } @inproceedings{4403, abstract = {For programs whose data variables range over boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, we consider algorithmic verification of programs that use boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over a potentially unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly-nested loops. The second result establishes connections to automata and logics defining languages over data words.}, author = {Alur, Rajeev and Cerny, Pavol and Weinstein, Scott}, location = {Coimbra, Portugal}, pages = {86 -- 101}, publisher = {Springer}, title = {{Algorithmic analysis of array-accessing programs}}, doi = {10.1007/978-3-642-04027-6_9}, volume = {5771}, year = {2009}, } @inproceedings{4453, abstract = {We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology.}, author = {Thomas Henzinger and Maria Mateescu and Wolf, Verena}, pages = {337 -- 352}, publisher = {Springer}, title = {{Sliding-window abstraction for infinite Markov chains}}, doi = {10.1007/978-3-642-02658-4_27}, volume = {5643}, year = {2009}, } @inproceedings{4542, abstract = {Weighted automata are finite automata with numerical weights on transitions. Nondeterministic weighted automata define quantitative languages L that assign to each word w a real number L(w) computed as the maximal value of all runs over w, and the value of a run r is a function of the sequence of weights that appear along r. There are several natural functions to consider such as Sup, LimSup, LimInf, limit average, and discounted sum of transition weights. We introduce alternating weighted automata in which the transitions of the runs are chosen by two players in a turn-based fashion. Each word is assigned the maximal value of a run that the first player can enforce regardless of the choices made by the second player. We survey the results about closure properties, expressiveness, and decision problems for nondeterministic weighted automata, and we extend these results to alternating weighted automata. For quantitative languages L 1 and L 2, we consider the pointwise operations max(L 1,L 2), min(L 1,L 2), 1 − L 1, and the sum L 1 + L 2. We establish the closure properties of all classes of alternating weighted automata with respect to these four operations. We next compare the expressive power of the various classes of alternating and nondeterministic weighted automata over infinite words. In particular, for limit average and discounted sum, we show that alternation brings more expressive power than nondeterminism. Finally, we present decidability results and open questions for the quantitative extension of the classical decision problems in automata theory: emptiness, universality, language inclusion, and language equivalence.}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A}, location = {Wroclaw, Poland}, pages = {3 -- 13}, publisher = {Springer}, title = {{Alternating weighted automata}}, doi = {10.1007/978-3-642-03409-1_2}, volume = {5699}, year = {2009}, } @inproceedings{4544, abstract = {We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. We present in this paper a strategy improvement algorithm for computing the value of a concurrent safety game, that is, the maximal probability with which player 1 can enforce the safety objective. The algorithm yields a sequence of player-1 strategies which ensure probabilities of winning that converge monotonically to the value of the safety game. Our result is significant because the strategy improvement algorithm provides, for the first time, a way to approximate the value of a concurrent safety game from below. Since a value iteration algorithm, or a strategy improvement algorithm for reachability games, can be used to approximate the same value from above, the combination of both algorithms yields a method for computing a converging sequence of upper and lower bounds for the values of concurrent reachability and safety games. Previous methods could approximate the values of these games only from one direction, and as no rates of convergence are known, they did not provide a practical way to solve these games.}, author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger}, pages = {197 -- 206}, publisher = {SIAM}, title = {{Termination criteria for solving concurrent safety and reachability games}}, doi = {10.1137/1.9781611973068.23}, year = {2009}, } @inproceedings{4545, abstract = {A stochastic game is a two-player game played oil a graph, where in each state the successor is chosen either by One of the players, or according to a probability distribution. We Survey Stochastic games with limsup and liminf objectives. A real-valued re-ward is assigned to each state, and the value of all infinite path is the limsup (resp. liminf) of all rewards along the path. The value of a stochastic game is the maximal expected value of an infinite path that call he achieved by resolving the decisions of the first player. We present the complexity of computing values of Stochastic games and their subclasses, and the complexity, of optimal strategies in such games. }, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A}, location = {Rhodos, Greece}, pages = {1 -- 15}, publisher = {Springer}, title = {{A survey of stochastic games with limsup and liminf objectives}}, doi = {10.1007/978-3-642-02930-1_1}, volume = {5556}, year = {2009}, } @inproceedings{2702, abstract = {We review our proof that in a scaling limit, the time evolution of a quantum particle in a static random environment leads to a diffusion equation. In particular, we discuss the role of Feynman graph expansions and of renormalization. }, author = {László Erdös and Salmhofer, Manfred and Yau, Horng-Tzer}, pages = {167 -- 182}, publisher = {World Scientific Publishing}, title = {{Feynman graphs and renormalization in quantum diffusion}}, doi = {10.1142/9789812833556_0011}, year = {2008}, } @article{3037, author = {Feraru, Elena and Friml, Jirí}, journal = {Plant Physiology}, number = {4}, pages = {1553 -- 1559}, publisher = {American Society of Plant Biologists}, title = {{PIN polar targeting}}, doi = {10.1104/pp.108.121756}, volume = {147}, year = {2008}, } @article{3307, abstract = {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.}, author = {Green, Richard E and Malaspinas, Anna-Sapfo and Krause, Johannes and Briggs, Adrian W and Johnson, Philip L and Caroline Uhler and Meyer, Matthias and Good, Jeffrey M and Maricic, Tomislav and Stenzel, Udo and Prüfer, Kay and Siebauer, Michael F and Burbano, Hernän A and Ronan, Michael T and Rothberg, Jonathan M and Egholm, Michael and Rudan, Pavao and Brajković, Dejana and Kućan, Željko and Gušić, Ivan and Wikström, Mårten K and Laakkonen, Liisa J and Kelso, Janet F and Slatkin, Montgomery and Pääbo, Svante H}, journal = {Cell}, pages = {416 -- 426}, publisher = {Cell Press}, title = {{A complete neandertal mitochondrial genome sequence determined by highhhroughput sequencing}}, doi = {10.1016/j.cell.2008.06.021}, volume = {134}, year = {2008}, } @article{11113, abstract = {The nuclear envelope (NE), a double membrane enclosing the nucleus of eukaryotic cells, controls the flow of information between the nucleoplasm and the cytoplasm and provides a scaffold for the organization of chromatin and the cytoskeleton. In dividing metazoan cells, the NE breaks down at the onset of mitosis and then reforms around segregated chromosomes to generate the daughter nuclei. Recent data from intact cells and cell-free nuclear assembly systems suggest that the endoplasmic reticulum (ER) is the source of membrane for NE assembly. At the end of mitosis, ER membrane tubules are targeted to chromatin via tubule ends and reorganized into flat nuclear membrane sheets by specific DNA-binding membrane proteins. In contrast to previous models, which proposed vesicle fusion to be the principal mechanism of NE formation, these new studies suggest that the nuclear membrane forms by the chromatin-mediated reshaping of the ER.}, author = {Anderson, Daniel J. and HETZER, Martin W}, issn = {1477-9137}, journal = {Journal of Cell Science}, keywords = {Cell Biology}, number = {2}, pages = {137--142}, publisher = {The Company of Biologists}, title = {{Shaping the endoplasmic reticulum into the nuclear envelope}}, doi = {10.1242/jcs.005777}, volume = {121}, year = {2008}, } @article{11114, abstract = {We present a miniaturized pull-down method for the detection of protein-protein interactions using standard affinity chromatography reagents. Binding events between different proteins, which are color-coded with quantum dots (QDs), are visualized on single affinity chromatography beads by fluorescence microscopy. The use of QDs for single molecule detection allows the simultaneous analysis of multiple protein-protein binding events and reduces the amount of time and material needed to perform a pull-down experiment.}, author = {Schulte, Roberta and Talamas, Jessica and Doucet, Christine and HETZER, Martin W}, issn = {1932-6203}, journal = {PLoS ONE}, keywords = {Multidisciplinary}, number = {4}, publisher = {Public Library of Science}, title = {{Single bead affinity detection (SINBAD) for the analysis of protein-protein interactions}}, doi = {10.1371/journal.pone.0002061}, volume = {3}, year = {2008}, } @article{1763, abstract = {The field of cavity quantum electrodynamics (QED), traditionally studied in atomic systems, has gained new momentum by recent reports of quantum optical experiments with solid-state semiconducting and superconducting systems. In cavity QED, the observation of the vacuum Rabi mode splitting is used to investigate the nature of matter-light interaction at a quantum-mechanical level. However, this effect can, at least in principle, be explained classically as the normal mode splitting of two coupled linear oscillators. It has been suggested that an observation of the scaling of the resonant atom-photon coupling strength in the Jaynes-Cummings energy ladder with the square root of photon number n is sufficient to prove that the system is quantum mechanical in nature. Here we report a direct spectroscopic observation of this characteristic quantum nonlinearity. Measuring the photonic degree of freedom of the coupled system, our measurements provide unambiguous spectroscopic evidence for the quantum nature of the resonant atom-field interaction in cavity QED. We explore atom-photon superposition states involving up to two photons, using a spectroscopic pump and probe technique. The experiments have been performed in a circuit QED set-up, in which very strong coupling is realized by the large dipole coupling strength and the long coherence time of a superconducting qubit embedded in a high-quality on-chip microwave cavity. Circuit QED systems also provide a natural quantum interface between flying qubits (photons) and stationary qubits for applications in quantum information processing and communication.}, author = {Johannes Fink and Göppl, M and Baur, Matthias P and Bianchetti, R and Leek, Peter J and Blais, Alexandre and Wallraff, Andreas}, journal = {Nature}, number = {7202}, pages = {315 -- 318}, publisher = {Nature Publishing Group}, title = {{Climbing the Jaynes-Cummings ladder and observing its √n nonlinearity in a cavity QED system}}, doi = {10.1038/nature07112}, volume = {454}, year = {2008}, } @article{1765, abstract = {High quality on-chip microwave resonators have recently found prominent new applications in quantum optics and quantum information processing experiments with superconducting electronic circuits, a field now known as circuit quantum electrodynamics (QED). They are also used as single photon detectors and parametric amplifiers. Here we analyze the physical properties of coplanar waveguide resonators and their relation to the materials properties for use in circuit QED. We have designed and fabricated resonators with fundamental frequencies from 2 to 9 GHz and quality factors ranging from a few hundreds to a several hundred thousands controlled by appropriately designed input and output coupling capacitors. The microwave transmission spectra measured at temperatures of 20 mK are shown to be in good agreement with theoretical lumped element and distributed element transmission matrix models. In particular, the experimentally determined resonance frequencies, quality factors, and insertion losses are fully and consistently explained by the two models for all measured devices. The high level of control and flexibility in design renders these resonators ideal for storing and manipulating quantum electromagnetic fields in integrated superconducting electronic circuits.}, author = {Göppl, M and Fragner, A and Baur, Matthias P and Bianchetti, R and Filipp, Stefan and Johannes Fink and Leek, Peter J and Puebla, G and Steffen, L. Kraig and Wallraff, Andreas}, journal = {Journal of Applied Physics}, number = {11}, publisher = {American Institute of Physics}, title = {{Coplanar waveguide resonators for circuit quantum electrodynamics}}, doi = {10.1063/1.3010859}, volume = {104}, year = {2008}, } @article{2120, abstract = {We consider the linear stochastic Cauchy problem dX (t) =AX (t) dt +B dWH (t), t≥ 0, where A generates a C0-semigroup on a Banach space E, WH is a cylindrical Brownian motion over a Hilbert space H, and B: H → E is a bounded operator. Assuming the existence of a unique minimal invariant measure μ∞, let Lp denote the realization of the Ornstein-Uhlenbeck operator associated with this problem in Lp (E, μ∞). Under suitable assumptions concerning the invariance of the range of B under the semigroup generated by A, we prove the following domain inclusions, valid for 1 < p ≤ 2: Image omitted. Here WHk, p (E, μinfin; denotes the kth order Sobolev space of functions with Fréchet derivatives up to order k in the direction of H. No symmetry assumptions are made on L p.}, author = {Jan Maas and van Neerven, Jan M}, journal = {Infinite Dimensional Analysis, Quantum Probability and Related Topics}, number = {4}, pages = {603 -- 626}, publisher = {World Scientific Publishing}, title = {{On the domain of non-symmetric Ornstein-Uhlenbeck operators in banach spaces}}, doi = {10.1142/S0219025708003245}, volume = {11}, year = {2008}, } @article{2121, abstract = {Let H be a separable real Hubert space and let double struck F sign = (ℱt)t∈[0,T] be the augmented filtration generated by an H-cylindrical Brownian motion (WH(t))t∈[0,T] on a probability space (Ω, ℱ ℙ). We prove that if E is a UMD Banach space, 1 ≤ p < ∞, and F ∈ double struck D sign1,p(Ω E) is ℱT-measurable, then F = double struck E sign(F) + ∫0T Pdouble struck F sign(DF) dW H, where D is the Malliavin derivative of F and P double struck F sign is the projection onto the F-adapted elements in a suitable Banach space of Lp-stochastically integrable ℒ(H, E)-valued processes.}, author = {van Neerven, Jan M and Jan Maas}, journal = {Electronic Communications in Probability}, pages = {151 -- 164}, publisher = {Institute of Mathematical Statistics}, title = {{A Clark-Ocone formula in UMD Banach spaces}}, volume = {13}, year = {2008}, } @article{2146, abstract = {We present an analytic model of thermal state-to-state rotationally inelastic collisions of polar molecules in electric fields. The model is based on the Fraunhofer scattering of matter waves and requires Legendre moments characterizing the “shape” of the target in the body-fixed frame as its input. The electric field orients the target in the space-fixed frame and thereby effects a striking alteration of the dynamical observables: both the phase and amplitude of the oscillations in the partial differential cross sections undergo characteristic field-dependent changes that transgress into the partial integral cross sections. As the cross sections can be evaluated for a field applied parallel or perpendicular to the relative velocity, the model also offers predictions about steric asymmetry. We exemplify the field-dependent quantum collision dynamics with the behavior of the Ne–OCS(Σ1) and Ar–NO(Π2) systems. A comparison with the close-coupling calculations available for the latter system [Chem. Phys. Lett.313, 491 (1999)] demonstrates the model’s ability to qualitatively explain the field dependence of all the scattering features observed.}, author = {Mikhail Lemeshko and Friedrich, Břetislav}, journal = {Journal of Chemical Physics}, number = {2}, publisher = {American Institute of Physics}, title = {{An analytic model of rotationally inelastic collisions of polar molecules in electric fields}}, doi = {10.1063/1.2948392}, volume = {129}, year = {2008}, } @inproceedings{2331, abstract = {We present a review of recent work on the mathematical aspects of the BCS gap equation, covering our results of Ref. 9 as well our recent joint work with Hamza and Solovej and with Frank and Naboko, respectively. In addition, we mention some related new results.}, author = {Hainzl, Christian and Robert Seiringer}, pages = {117 -- 136}, publisher = {World Scientific Publishing}, title = {{ Spectral properties of the BCS gap equation of superfluidity}}, doi = {10.1142/9789812832382_0009}, year = {2008}, } @inproceedings{2332, abstract = {We present a rigorous proof of the appearance of quantized vortices in dilute trapped Bose gases with repulsive two-body interactions subject to rotation, which was obtained recently in joint work with Elliott Lieb.14 Starting from the many-body Schrödinger equation, we show that the ground state of such gases is, in a suitable limit, well described by the nonlinear Gross-Pitaevskii equation. In the case of axially symmetric traps, our results show that the appearance of quantized vortices causes spontaneous symmetry breaking in the ground state.}, author = {Robert Seiringer}, pages = {241 -- 254}, publisher = {World Scientific Publishing}, title = {{Vortices and Spontaneous Symmetry Breaking in Rotating Bose Gases}}, doi = {10.1142/9789812832382_0017}, year = {2008}, } @article{2374, abstract = {A lower bound is derived on the free energy (per unit volume) of a homogeneous Bose gas at density Q and temperature T. In the dilute regime, i.e., when a3 1, where a denotes the scattering length of the pair-interaction potential, our bound differs to leading order from the expression for non-interacting particles by the term 4πa(2 2}-[ - c]2+). Here, c(T) denotes the critical density for Bose-Einstein condensation (for the non-interacting gas), and [ · ]+ = max{ ·, 0} denotes the positive part. Our bound is uniform in the temperature up to temperatures of the order of the critical temperature, i.e., T ~ 2/3 or smaller. One of the key ingredients in the proof is the use of coherent states to extend the method introduced in [17] for estimating correlations to temperatures below the critical one.}, author = {Robert Seiringer}, journal = {Communications in Mathematical Physics}, number = {3}, pages = {595 -- 636}, publisher = {Springer}, title = {{Free energy of a dilute Bose gas: Lower bound}}, doi = {10.1007/s00220-008-0428-2}, volume = {279}, year = {2008}, } @article{2376, abstract = {We derive upper and lower bounds on the critical temperature Tc and the energy gap Ξ (at zero temperature) for the BCS gap equation, describing spin- 1 2 fermions interacting via a local two-body interaction potential λV(x). At weak coupling λ 1 and under appropriate assumptions on V(x), our bounds show that Tc ∼A exp(-B/λ) and Ξ∼C exp(-B/λ) for some explicit coefficients A, B, and C depending on the interaction V(x) and the chemical potential μ. The ratio A/C turns out to be a universal constant, independent of both V(x) and μ. Our analysis is valid for any μ; for small μ, or low density, our formulas reduce to well-known expressions involving the scattering length of V(x).}, author = {Hainzl, Christian and Robert Seiringer}, journal = {Physical Review B - Condensed Matter and Materials Physics}, number = {18}, publisher = {American Physical Society}, title = {{Critical temperature and energy gap for the BCS equation}}, doi = {10.1103/PhysRevB.77.184517}, volume = {77}, year = {2008}, }