@inproceedings{4533, abstract = {Interface theories have been proposed to support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, maintaining compatibility. We show that these interface theories provide no formal support for component reuse, meaning that the same component cannot be used to implement several different interfaces in a design. We add a new operation to interface theories in order to support such reuse. For example, different interfaces for the same component may refer to different aspects such as functionality, timing, and power consumption. We give both stateless and stateful examples for interface theories with component reuse. To illustrate component reuse in interface-based design, we show how the stateful theory provides a natural framework for specifying and refining PCI bus clients.}, author = {Doyen, Laurent and Thomas Henzinger and Jobstmann, Barbara and Tatjana Petrov}, pages = {79 -- 88}, publisher = {ACM}, title = {{Interface theories with component reuse}}, doi = {10.1145/1450058.1450070}, year = {2008}, } @article{4534, abstract = {A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives, and mean-payoff (or limit-average) objectives. These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of stochastic parity games to stochastic mean-payoff games.}, author = {Krishnendu Chatterjee and Thomas Henzinger}, journal = {Information Processing Letters}, number = {1}, pages = {1 -- 7}, publisher = {Elsevier}, title = {{Reduction of stochastic parity to stochastic mean-payoff games}}, doi = {10.1016/j.ipl.2007.08.035}, volume = {106}, year = {2008}, } @inproceedings{4546, abstract = {We propose the notion of logical reliability for real-time program tasks that interact through periodically updated program variables. We describe a reliability analysis that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The resulting analysis can be combined with an incremental schedulability analysis for interacting real-time tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination language for distributed real-time systems. We implemented a logical-reliability-enhanced prototype of the compiler and runtime infrastructure for HTL.}, author = {Krishnendu Chatterjee and Ghosal, Arkadeb and Thomas Henzinger and Iercan, Daniel and Kirsch, Christoph M and Pinello, Claudio and Sangiovanni-Vincentelli, Alberto}, pages = {909 -- 914}, publisher = {IEEE}, title = {{Logical reliability of interacting real-time tasks}}, doi = {10.1145/1403375.1403595}, year = {2008}, } @article{4548, abstract = {The value of a finite-state two-player zero-sum stochastic game with limit-average payoff can be approximated to within ε in time exponential in a polynomial in the size of the game times polynomial in logarithmic in 1/ε, for all ε > 0.}, author = {Krishnendu Chatterjee and Majumdar, Ritankar S and Thomas Henzinger}, journal = {International Journal of Game Theory}, number = {2}, pages = {219 -- 234}, publisher = {Springer}, title = {{Stochastic limit-average games are in EXPTIME}}, doi = {10.1007/s00182-007-0110-5}, volume = {37}, year = {2008}, } @inproceedings{4568, abstract = {We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking.}, author = {Beyer, Dirk and Thomas Henzinger and Théoduloz, Grégory}, pages = {29 -- 38}, publisher = {ACM}, title = {{Program analysis with dynamic change of precision}}, doi = {10.1109/ASE.2008.13}, year = {2008}, } @article{517, author = {Barton, Nicholas H}, journal = {Genetics Research}, number = {5-6}, pages = {475 -- 477}, publisher = {Cambridge University Press}, title = {{Identity and coalescence in structured populations: A commentary on 'Inbreeding coefficients and coalescence times' by Montgomery Slatkin}}, doi = {10.1017/S0016672308009683}, volume = {89}, year = {2008}, } @article{581, abstract = {We have detected a spin-dependent displacement perpendicular to the refractive index gradient for photons passing through an air-glass interface. The effect is the photonic version of the spin Hall effect in electronic systems, indicating the universality of the effect for particles of different nature. Treating the effect as a weak measurement of the spin projection of the photons, we used a preselection and postselection technique on the spin state to enhance the original displacement by nearly four orders of magnitude, attaining sensitivity to displacements of ∼1 angstrom. The spin Hall effect can be used for manipulating photonic angular momentum states, and the measurement technique holds promise for precision metrology.}, author = {Onur Hosten and Kwiat, Paul}, journal = {Science}, number = {5864}, pages = {787 -- 790}, publisher = {American Association for the Advancement of Science}, title = {{Observation of the spin hall effect of light via weak measurements}}, doi = {10.1126/science.1152697}, volume = {319}, year = {2008}, } @inproceedings{584, abstract = {Using “quantum weak-measurements” as a coherent enhancement technique for small signals, we have measured the recently proposed “spin Hall effect” of light at an air-glass interface, and are working on the smoothly varying refractive-index case.}, author = {Hosten, Onur and Kwiat, Paul}, isbn = {978-155752859-9}, issn = {21622701}, location = {San Jose, CA, United States}, publisher = {Optica Publishing Group}, title = {{Spin hall effect of light via weak measurements: Sharp and smooth index variations}}, year = {2008}, } @article{6146, abstract = {Homeostasis of internal carbon dioxide (CO2) and oxygen (O2) levels is fundamental to all animals. Here we examine the CO2 response of the nematode Caenorhabditis elegans. This species inhabits rotting material, which typically has a broad CO2 concentration range. We show that well fed C. elegans avoid CO2 levels above 0.5%. Animals can respond to both absolute CO2 concentrations and changes in CO2 levels within seconds. Responses to CO2 do not reflect avoidance of acid pH but appear to define a new sensory response. Sensation of CO2 is promoted by the cGMP-gated ion channel subunits TAX-2 and TAX-4, but other pathways are also important. Robust CO2 avoidance in well fed animals requires inhibition of the DAF-16 forkhead transcription factor by the insulin-like receptor DAF-2. Starvation, which activates DAF-16, strongly suppresses CO2 avoidance. Exposure to hypoxia (<1% O2) also suppresses CO2 avoidance via activation of the hypoxia-inducible transcription factor HIF-1. The npr-1 215V allele of the naturally polymorphic neuropeptide receptor npr-1, besides inhibiting avoidance of high ambient O2 in feeding C. elegans, also promotes avoidance of high CO2. C. elegans integrates competing O2 and CO2 sensory inputs so that one response dominates. Food and allelic variation at NPR-1 regulate which response prevails. Our results suggest that multiple sensory inputs are coordinated by C. elegans to generate different coherent foraging strategies.}, author = {Bretscher, A. J. and Busch, K. E. and de Bono, Mario}, issn = {0027-8424}, journal = {Proceedings of the National Academy of Sciences}, number = {23}, pages = {8044--8049}, publisher = {Proceedings of the National Academy of Sciences}, title = {{A carbon dioxide avoidance behavior is integrated with responses to ambient oxygen and food in Caenorhabditis elegans}}, doi = {10.1073/pnas.0707607105}, volume = {105}, year = {2008}, } @article{6148, author = {Kammenga, Jan E. and Phillips, Patrick C. and de Bono, Mario and Doroszuk, Agnieszka}, issn = {0168-9525}, journal = {Trends in Genetics}, number = {4}, pages = {178--185}, publisher = {Elsevier}, title = {{Beyond induced mutants: using worms to study natural variation in genetic pathways}}, doi = {10.1016/j.tig.2008.01.001}, volume = {24}, year = {2008}, } @article{6149, author = {Olofsson, Birgitta and de Bono, Mario}, issn = {0960-9822}, journal = {Current Biology}, number = {5}, pages = {R204--R206}, publisher = {Elsevier}, title = {{Sleep: dozy worms and sleepy flies}}, doi = {10.1016/j.cub.2008.01.002}, volume = {18}, year = {2008}, } @article{1982, abstract = {In the bacterium Escherichia coli, the Min proteins oscillate between the cell poles to select the cell center as division site. This dynamic pattern has been proposed to arise by self-organization of these proteins, and several models have suggested a reaction-diffusion type mechanism. Here, we found that the Min proteins spontaneously formed planar surface waves on a flat membrane in vitro. The formation and maintenance of these patterns, which extended for hundreds of micrometers, required adenosine 5′-triphosphate (ATP), and they persisted for hours. We present a reaction-diffusion model of the MinD and MinE dynamics that accounts for our experimental observations and also captures the in vivo oscillations.}, author = {Martin Loose and Fischer-Friedrich, Elisabeth and Ries, Jonas and Kruse, Karsten and Schwille, Petra }, journal = {Science}, number = {5877}, pages = {789 -- 792}, publisher = {American Association for the Advancement of Science}, title = {{Spatial regulators for bacterial cell division self-organize into surface waves in vitro}}, doi = {10.1126/science.1154413}, volume = {320}, year = {2008}, } @article{2065, abstract = {Population genetics models show that, under certain conditions, the X chromosome is expected to be under more efficient selection than the autosomes. This could lead to 'faster-X evolution', if a large proportion of mutations are fixed by positive selection, as suggested by recent studies in Drosophila. We used a multispecies approach to test this: Muller's element D, an autosomal arm, is fused to the ancestral X chromosome in Drosophila pseudoobscura and its sister species, Drosophila affinis. We tested whether the same set of genes had higher rates of non-synonymous evolution when they were X-linked (in the D. pseudoobscura/D. affinis comparison) than when they were autosomal (in Drosophila melanogaster/Drosophila yakuba). Although not significant, our results suggest this may be the case, but only for genes under particularly strong positive selection/weak purifying selection. They also suggest that genes that have become X-linked have higher levels of codon bias and slower synonymous site evolution, consistent with more effective selection on codon usage at X-linked sites.}, author = {Beatriz Vicoso and Haddrill, Penelope R and Charlesworth, Brian}, journal = {Genetical Research}, number = {5}, pages = {421 -- 431}, publisher = {Cambridge University Press}, title = {{A multispecies approach for comparing sequence evolution of X-linked and autosomal sites in Drosophila}}, doi = {10.1017/S0016672308009804}, volume = {90}, year = {2008}, } @inproceedings{2078, abstract = {This paper presents a novel method for real-time animation of highly-detailed facial expressions based on a multi-scale decomposition of facial geometry into large-scale motion and fine-scale details, such as expression wrinkles. Our hybrid animation is tailored to the specific characteristics of large- and fine-scale facial deformations: Large-scale deformations are computed with a fast linear shell model, which is intuitively and accurately controlled through a sparse set of motion-capture markers or user-defined handle points. Fine-scale facial details are incorporated using a novel pose-space deformation technique, which learns the correspondence of sparse measurements of skin strain to wrinkle formation from a small set of example poses. Our hybrid method features real-time animation of highly-detailed faces with realistic wrinkle formation, and allows both large-scale deformations and fine-scale wrinkles to be edited intuitively. Furthermore, our pose-space representation enables the transfer of facial details to novel expressions or other facial models.}, author = {Bickel, Bernd and Lang, Manuel and Botsch, Mario and Otaduy, Miguel and Gross, Markus}, pages = {57 -- 66}, publisher = {ACM}, title = {{Pose-space animation and transfer of facial details}}, doi = {10.2312/SCA/SCA08/057-066}, year = {2008}, } @article{1036, abstract = {We report on the control of interaction-induced dephasing of Bloch oscillations for an atomic Bose-Einstein condensate in an optical lattice. We quantify the dephasing in terms of the width of the quasimomentum distribution and measure its dependence on time for different interaction strengths which we control by means of a Feshbach resonance. For minimal interaction, the dephasing time is increased from a few to more than 20 thousand Bloch oscillation periods, allowing us to realize a BEC-based atom interferometer in the noninteracting limit.}, author = {Gustavsson, Mattias and Haller, Elmar and Mark, Manfred and Danzl, Johann G and Rojas Kopeinig, Gabriel and Nägerl, Hanns}, journal = {Physical Review Letters}, number = {8}, publisher = {American Physical Society}, title = {{Control of interaction-induced dephasing of bloch oscillations}}, doi = {10.1103/PhysRevLett.100.080404}, volume = {100}, year = {2008}, } @article{1037, abstract = {We experimentally demonstrate Cs2 Feshbach molecules well above the dissociation threshold, which are stable against spontaneous decay on the time scale of 1s. An optically trapped sample of ultracold dimers is prepared in a high rotational state and magnetically tuned into a region with a negative binding energy. The metastable character of these molecules arises from the large centrifugal barrier in combination with negligible coupling to states with low rotational angular momentum. A sharp onset of dissociation with increasing magnetic field is mediated by a crossing with a lower rotational dimer state and facilitates dissociation on demand with a well-defined energy.}, author = {Knoop, Steven and Mark, Michael and Ferlaino, Francesca and Danzl, Johann G and Kraemer, Tobias and Nägerl, Hanns and Grimm, Rudolf}, journal = {Physical Review Letters}, number = {8}, publisher = {American Physical Society}, title = {{Metastable feshbach molecules in high rotational states}}, doi = {10.1103/PhysRevLett.100.083002}, volume = {100}, year = {2008}, } @article{1039, abstract = {Molecular cooling techniques face the hurdle of dissipating translational as well as internal energy in the presence of a rich electronic, vibrational, and rotational energy spectrum. In our experiment, we create a translationally ultracold, dense quantum gas of molecules bound by more than 1000 wave numbers in the electronic ground state. Specifically, we stimulate with 80% efficiency, a two-photon transfer of molecules associated on a Feshbach resonance from a Bose-Einstein condensate of cesium atoms. In the process, the initial loose, long-range electrostatic bond of the Feshbach molecule is coherently transformed into a tight chemical bond. We demonstrate coherence of the transfer in a Ramsey-type experiment and show that the molecular sample is not heated during the transfer. Our results show that the preparation of a quantum gas of molecules in specific rovibrational states is possible and that the creation of a Bose-Einstein condensate of molecules in their rovibronic ground state is within reach.}, author = {Danzl, Johann G and Haller, Elmar and Gustavsson, Mattias and Mark, Manfred and Hart, Russell and Bouloufa, Nadia and Dulieu, Olivier and Ritsch, Helmut and Nägerl, Hanns}, journal = {Science}, number = {5892}, pages = {1062 -- 1066}, publisher = {American Association for the Advancement of Science}, title = {{Quantum gas of deeply bound ground state molecules}}, doi = {10.1126/science.1159909}, volume = {321}, year = {2008}, } @article{10392, abstract = {Protonated formylmetallocenes [M(C5H5)(C5H4-CHOH)]+ (M = Fe, Ru) and their isomers have been studied at the BP86 and B3LYP levels of density functional theory. Oxygen-protonated isomers are the most stable forms in each case, with a plethora of ring- or metal-protonated species at least ca. 14 and 10 kcal/mol higher in energy for M = Fe and Ru, respectively. The computed rotational barriers around the C−C bond connecting the cyclopentadienyl and protonated formyl moieties, ca. 18 kcal/mol, are indicative of substantial conjugation between these moieties. Some of the ring- and iron-protonated species are models for possible intermediates in Friedel–Crafts acylation of ferrocene, and the computations provide further evidence that exo attack is clearly favored over endo attack of the electrophile in this reaction. The structures of the most stable mono- and diprotonated formylferrocenes are corroborated by the good agreement between GIAO-B3LYP-computed and experimental NMR chemical shifts.}, author = {Šarić, Anđela and Vrček, Valerije and Bühl, Michael}, issn = {1520-6041}, journal = {Organometallics}, keywords = {Inorganic Chemistry, Organic Chemistry, Physical and Theoretical Chemistry}, number = {3}, pages = {394--401}, publisher = {American Chemical Society}, title = {{Density functional study of protonated formylmetallocenes}}, doi = {10.1021/om700916f}, volume = {27}, year = {2008}, } @inproceedings{3170, abstract = {Geodesic active contours and graph cuts are two standard image segmentation techniques. We introduce a new segmentation method combining some of their benefits. Our main intuition is that any cut on a graph embedded in some continuous space can be interpreted as a contour (in 2D) or a surface (in 3D). We show how to build a grid graph and set its edge weights so that the cost of cuts is arbitrarily close to the length (area) of the corresponding contours (surfaces) for any anisotropic Riemannian metric. There are two interesting consequences of this technical result. First, graph cut algorithms can be used to find globally minimum geodesic contours (minimal surfaces in 3D) under arbitrary Riemannian metric for a given set of boundary conditions. Second, we show how to minimize metrication artifacts in existing graph-cut based methods in vision. Theoretically speaking, our work provides an interesting link between several branches of mathematics -differential geometry, integral geometry, and combinatorial optimization. The main technical problem is solved using Cauchy-Crofton formula from integral geometry.}, author = {Boykov, Yuri and Kolmogorov, Vladimir}, isbn = {0769519504}, location = {Nice, France}, pages = {26 -- 33}, publisher = {IEEE}, title = {{Computing geodesics and minimal surfaces via graph cuts}}, doi = {10.1109/ICCV.2003.1238310}, volume = {1}, year = {2008}, } @inproceedings{3174, abstract = {We address visual correspondence problems without assuming that scene points have similar intensities in different views. This situation is common, usually due to non-lambertian scenes or to differences between cameras. We use maximization of mutual information, a powerful technique for registering images that requires no a priori model of the relationship between scene intensities in different views. However, it has proven difficult to use mutual information to compute dense visual correspondence. Comparing fixed-size windows via mutual information suffers from the well-known problems of fixed windows, namely poor performance at discontinuities and in low-texture regions. In this paper, we show how to compute visual correspondence using mutual information without suffering from these problems. Using 'a simple approximation, mutual information can be incorporated into the standard energy minimization framework used in early vision. The energy can then be efficiently minimized using graph cuts, which preserve discontinuities and handle low-texture regions. The resulting algorithm combines the accurate disparity maps that come from graph cuts with the tolerance for intensity changes that comes from mutual information.}, author = {Kim, Junhwan and Kolmogorov, Vladimir and Zabih, Ramin}, booktitle = {Proceedings Ninth International Conference on Computer Vision}, isbn = {0769519504}, location = {Nice, France}, pages = {1033 -- 1040}, publisher = {IEEE}, title = {{Visual correspondence using energy minimization and mutual information}}, doi = {10.1109/ICCV.2003.1238463}, volume = {2}, year = {2008}, }