@article{2360, abstract = {An optical lattice model developed that is similar to the Bose-Hubbard model to describe the transition between Bose-Einstein condensation (BEC) and a Mott insulator state was analyzed. It was found that the system was a hard core lattice gas at half of the maximum density and the optical lattice was modeled by a periodic potential of strength λ. It was also observed that the interparticle interaction was essential for this transition that occurred even in the ground state. The results show that all the essential features could be proved rigorously such as the existence of BEC for small λ and its suppression for a large λ.}, author = {Aizenman, Michael and Lieb, Élliott H and Robert Seiringer and Solovej, Jan P and Yngvason, Jakob}, journal = {Physical Review A - Atomic, Molecular, and Optical Physics}, number = {2}, pages = {023612 -- 1--0236121--2}, publisher = {American Physical Society}, title = {{Bose-Einstein quantum phase transition in an optical lattice model}}, doi = {10.1103/PhysRevA.70.023612}, volume = {70}, year = {2004}, } @inbook{2417, author = {Lovász, László and Vesztergombi, Katalin and Uli Wagner and Welzl, Emo}, booktitle = {Towards a Theory of Geometric Graphs}, editor = {Pach, János}, pages = {139 -- 148}, publisher = {American Mathematical Society}, title = {{Convex quadrilaterals and k-sets }}, doi = {10.1090/conm/342}, volume = {342}, year = {2004}, } @article{2425, abstract = {A finite set N ⊂ Rd is a weak ε-net for an n-point set X ⊂ Rd (with respect to convex sets) if N intersects every convex set K with |K ∩ X| ≥ εn. We give an alternative, and arguably simpler, proof of the fact, first shown by Chazelle et al., that every point set X in Rd admits a weak ε-net of cardinality O(ε-dpolylog(1/ε)). Moreover, for a number of special point sets (e.g., for points on the moment curve), our method gives substantially better bounds. The construction yields an algorithm to construct such weak ε-nets in time O(n ln(1/ε)).}, author = {Matoušek, Jiří and Uli Wagner}, journal = {Discrete & Computational Geometry}, number = {2}, pages = {195 -- 206}, publisher = {Springer}, title = {{New constructions of weak ε-nets}}, doi = {10.1007/s00454-004-1116-4}, volume = {32}, year = {2004}, } @article{2426, abstract = {We introduce the adaptive neighborhood graph as a data structure for modeling a smooth manifold M embedded in some Euclidean space ℝ d. We assume that M is known to us only through a finite sample P ⊂ M, as is often the case in applications. The adaptive neighborhood graph is a geometric graph on P. Its complexity is at most min{2O(k)n, n2}, where n = P and k = dim M, as opposed to the n[d/2] complexity of the Delaunay triangulation, which is often used to model manifolds. We prove that we can correctly infer the connected components and the dimension of M from the adaptive neighborhood graph provided a certain standard sampling condition is fulfilled. The running time of the dimension detection algorithm is d20(k7 log k) for each connected component of M. If the dimension is considered constant, this is a constant-time operation, and the adaptive neighborhood graph is of linear size. Moreover, the exponential dependence of the constants is only on the intrinsic dimension k, not on the ambient dimension d. This is of particular interest if the co-dimension is high, i.e., if k is much smaller than d, as is the case in many applications. The adaptive neighborhood graph also allows us to approximate the geodesic distances between the points in P.}, author = {Giesen, Joachim and Uli Wagner}, journal = {Discrete & Computational Geometry}, number = {2}, pages = {245 -- 267}, publisher = {Springer}, title = {{Shape dimension and intrinsic metric from samples of manifolds}}, doi = {10.1007/s00454-004-1120-8}, volume = {32}, year = {2004}, } @article{7333, abstract = {The analysis of the complete H2/air polymer electrolyte fuel cell system shows that process air humidification is one of the biggest obstacles for a high performance portable system in the kW range. Therefore, a new concept, with passive process air humidification integrated into the stack, has been developed. Humidification in each cell makes the process independent from the number of cells and the operation mode, thus making the concept fully scalable. Without external humidification the system is simpler, smaller, and cheaper. The humidification of the process air is achieved by transfer of product water from the exhaust air, through part of the membrane, to the dry intake air. Tests have shown that cells using the concept of internal humidification and operated with dry air at 70 ° have almost the same performance as when operated with external humidification. A 42‐cell stack with this internal humidification concept was built and integrated into a portable 1 kW power generator system.}, author = {Santis, M. and Schmid, D. and Ruge, M. and Freunberger, Stefan Alexander and Büchi, F.N.}, issn = {1615-6846}, journal = {Fuel Cells}, number = {3}, pages = {214--218}, publisher = {Wiley}, title = {{Modular stack-internal air humidification concept-verification in a 1 kW stack}}, doi = {10.1002/fuce.200400028}, volume = {4}, year = {2004}, } @article{7334, abstract = {Fundamental and phenomenological models for cells, stacks, and complete systems of PEFC and SOFC are reviewed and their predictive power is assessed by comparing model simulations against experiments. Computationally efficient models suited for engineering design include the (1+1) dimensionality approach, which decouples the membrane in-plane and through-plane processes, and the volume-averaged-method (VAM) that considers only the lumped effect of pre-selected system components. The former model was shown to capture the measured lateral current density inhomogeneities in a PEFC and the latter was used for the optimization of commercial SOFC systems. State Space Modeling (SSM) was used to identify the main reaction pathways in SOFC and, in conjunction with the implementation of geometrically well-defined electrodes, has opened a new direction for the understanding of electrochemical reactions. Furthermore, SSM has advanced the understanding of the COpoisoning-induced anode impedance in PEFC. Detailed numerical models such as the Lattice Boltzmann (LB) method for transport in porous media and the full 3-D Computational Fluid Dynamics (CFD) Navier-Stokes simulations are addressed. These models contain all components of the relevant physics and they can improve the understanding of the related phenomena, a necessary condition for the development of both appropriate simplified models as well as reliable technologies. Within the LB framework, a technique for the characterization and computer-reconstruction of the porous electrode structure was developed using advanced pattern recognition algorithms. In CFD modeling, 3-D simulations were used to investigate SOFC with internal methane steam reforming and have exemplified the significance of porous and novel fractal channel distributors for the fuel and oxidant delivery, as well as for the cooling of PEFC. As importantly, the novel concept has been put forth of functionally designed, fractal-shaped fuel cells, showing promise of significant performance improvements over the conventional rectangular shaped units. Thermo-economic modeling for the optimization of PEFC is finally addressed. }, author = {Mantzaras, John and Freunberger, Stefan Alexander and Büchi, Felix N. and Roos, Markus and Brandstätter, Wilhelm and Prestat, Michel and Gauckler, Ludwig J. and Andreaus, Bernhard and Hajbolouri, Faegheh and Senn, Stephan M. and Poulikakos, Dimos and Chaniotis, Andreas K. and Larrain, Diego and Autissier, Nordahl and Maréchal, François}, issn = {0009-4293}, journal = {CHIMIA International Journal for Chemistry}, number = {12}, pages = {857--868}, publisher = {Swiss Chemical Society}, title = {{Fuel cell modeling and simulations}}, doi = {10.2533/000942904777677029}, volume = {58}, year = {2004}, } @article{7706, abstract = {The Sir2 deacetylase modulates organismal life-span in various species. However, the molecular mechanisms by which Sir2 increases longevity are largely unknown. We show that in mammalian cells, the Sir2 homolog SIRT1 appears to control the cellular response to stress by regulating the FOXO family of Forkhead transcription factors, a family of proteins that function as sensors of the insulin signaling pathway and as regulators of organismal longevity. SIRT1 and the FOXO transcription factor FOXO3 formed a complex in cells in response to oxidative stress, and SIRT1 deacetylated FOXO3 in vitro and within cells. SIRT1 had a dual effect on FOXO3 function: SIRT1 increased FOXO3's ability to induce cell cycle arrest and resistance to oxidative stress but inhibited FOXO3's ability to induce cell death. Thus, one way in which members of the Sir2 family of proteins may increase organismal longevity is by tipping FOXO-dependent responses away from apoptosis and toward stress resistance.}, author = {Brunet, Anne and Sweeney, Lora Beatrice Jaeger and Sturgill, J Fitzhugh and Chua, Katrin and Greer, Paul and Lin, Yingxi and Tran, Hien and Ross, Sarah and Mostoslavsky, Raul and Cohen, Haim and Hu, Linda and Chen, Hwei-Ling and Jedrychowski, Mark and Gygi, Steven and Sinclair, David and Alt, Frederick and Greenberg, Michael}, issn = {0036-8075}, journal = {Science}, number = {5666}, pages = {2011--2015}, publisher = {American Association for the Advancement of Science}, title = {{Stress-dependent regulation of FOXO transcription factors by the SIRT1 deacetylase}}, doi = {10.1126/science.1094637}, volume = {303}, year = {2004}, } @inproceedings{4577, abstract = {While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems - assertion checking, reachability analysis, dead code analysis, and test generation - directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code.}, author = {Beyer, Dirk and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, pages = {251 -- 255}, publisher = {IEEE}, title = {{An eclipse plug-in for model checking}}, doi = {10.1109/WPC.2004.1311069 }, year = {2004}, } @inproceedings{4578, abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Blast is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the Blast specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications. }, author = {Beyer, Dirk and Chlipala, Adam J and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, pages = {2 -- 18}, publisher = {Springer}, title = {{The BLAST query language for software verification}}, doi = {10.1007/978-3-540-27864-1_2}, volume = {3148}, year = {2004}, } @inproceedings{4581, abstract = {We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test vector generation is fully automatic (no user intervention) and exact (no false positives).}, author = {Beyer, Dirk and Chlipala, Adam J and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, pages = {326 -- 335}, publisher = {IEEE}, title = {{Generating tests from counterexamples}}, doi = {10.1109/ICSE.2004.1317455}, year = {2004}, } @inproceedings{4629, abstract = {Temporal logic is two-valued: a property is either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic Ctl which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. We interpret the resulting logic Dctl over transition systems, Markov chains, and Markov decision processes. We present two semantics for Dctl: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for Dctl, and we provide model-checking algorithms for both semantics.}, author = {de Alfaro, Luca and Faella, Marco and Thomas Henzinger and Majumdar, Ritankar S and Stoelinga, Mariëlle}, pages = {77 -- 92}, publisher = {Springer}, title = {{Model checking discounted temporal properties}}, doi = {10.1007/978-3-540-24730-2_6}, volume = {2988}, year = {2004}, } @article{6155, abstract = {The genome of the nematode Caenorhabditis elegans encodes seven soluble guanylate cyclases (sGCs) [1]. In mammals, sGCs function as α/β heterodimers activated by gaseous ligands binding to a haem prosthetic group 2, 3. The principal activator is nitric oxide, which acts through sGCs to regulate diverse cellular events. In C. elegans the function of sGCs is mysterious: the worm genome does not appear to encode nitric oxide synthase, and all C. elegans sGC subunits are more closely related to mammalian β than α subunits [1]. Here, we show that two of the seven C. elegans sGCs, GCY-35 and GCY-36, promote aggregation behavior. gcy-35 and gcy-36 are expressed in a small number of neurons. These include the body cavity neurons AQR, PQR, and URX, which are directly exposed to the blood equivalent of C. elegans and regulate aggregation behavior [4]. We show that GCY-35 and GCY-36 act as α-like and β-like sGC subunits and that their function in the URX sensory neurons is sufficient for strong nematode aggregation. Neither GCY-35 nor GCY-36 is absolutely required for C. elegans to aggregate. Instead, these molecules may transduce one of several pathways that induce C. elegans to aggregate or may modulate aggregation by responding to cues in C. elegans body fluid.}, author = {Cheung, Benny H.H and Arellano-Carbajal, Fausto and Rybicki, Irene and de Bono, Mario}, issn = {0960-9822}, journal = {Current Biology}, number = {12}, pages = {1105--1111}, publisher = {Elsevier}, title = {{Soluble guanylate cyclases act in neurons exposed to the body fluid to promote C. elegans aggregation behavior}}, doi = {10.1016/j.cub.2004.06.027}, volume = {14}, year = {2004}, } @article{1456, abstract = {We study the space of L2 harmonic forms on complete manifolds with metrics of fibred boundary or fibred cusp type. These metrics generalize the geometric structures at infinity of several different well-known classes of metrics, including asymptotically locally Euclidean manifolds, the (known types of) gravitational instantons, and also Poincaré metrics on ℚ-rank 1 ends of locally symmetric spaces and on the complements of smooth divisors in Kähler manifolds. The answer in all cases is given in terms of intersection cohomology of a stratified compactification of the manifold. The L2 signature formula implied by our result is closely related to the one proved by Dai and more generally by Vaillant and identifies Dai's τ-invariant directly in terms of intersection cohomology of differing perversities. This work is also closely related to a recent paper of Carron and the forthcoming paper of Cheeger and Dai. We apply our results to a number of examples, gravitational instantons among them, arising in predictions about L2 harmonic forms in duality theories in string theory.}, author = {Tamas Hausel and Hunsicker, Eugénie and Mazzeo, Rafe R}, journal = {Duke Mathematical Journal}, number = {3}, pages = {485 -- 548}, publisher = {Duke University Press}, title = {{Hodge cohomology of gravitational instantons}}, doi = {10.1215/S0012-7094-04-12233-X}, volume = {122}, year = {2004}, } @article{1464, abstract = {The moduli space of stable vector bundles on a Riemann surface is smooth when the rank and degree are coprime, and is diffeomorphic to the space of unitary connections of central constant curvature. A classic result of Newstead and Atiyah and Bott asserts that its rational cohomology ring is generated by the universal classes, that is, by the Kunneth components of the Chern classes of the universal bundle. This paper studies the larger, non-compact moduli space of Higgs bundles, as introduced by Hitchin and Simpson, with values in the canonical bundle K. This is diffeomorphic to the space of all connections of central constant curvature, whether unitary or not. The main result of the paper is that, in the rank 2 case, the rational cohomology ring of this space is again generated by universal classes. The spaces of Higgs bundles with values in K(n) for n > 0 turn out to be essential to the story. Indeed, we show that their direct limit has the homotopy type of the classifying space of the gauge group, and hence has cohomology generated by universal classes. 2000 Mathematics Subject Classification 14H60 (primary), 14D20, 14H81, 32Q55, 58D27 (secondary). }, author = {Tamas Hausel and Thaddeus, Michael}, journal = {Proceedings of the London Mathematical Society}, number = {3}, pages = {632 -- 658}, publisher = {Oxford University Press}, title = {{Generators for the cohomology ring of the moduli space of rank 2 higgs bundles}}, doi = {10.1112/S0024611503014618}, volume = {88}, year = {2004}, } @article{13434, abstract = {Thin films of ionically doped gelatin have been color-patterned with submicrometer precision using the wet-stamping technique. Inorganic salts are delivered onto the gelatin surface from an agarose stamp, and diffuse into the gelatine layer, producting deeply colored precipitates. Reaction fronts originating from different features of the stamp cease within < 1 μm of each other, leaving sharp, transparent regions in between.}, author = {Campbell, C. J. and Fialkowski, M. and Klajn, Rafal and Bensemann, I. T. and Grzybowski, B. A.}, issn = {1521-4095}, journal = {Advanced Materials}, keywords = {Mechanical Engineering, Mechanics of Materials, General Materials Science}, number = {21}, pages = {1912--1917}, publisher = {Wiley}, title = {{Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts}}, doi = {10.1002/adma.200400383}, volume = {16}, year = {2004}, } @article{13435, abstract = {Micropatterning of surfaces with several chemicals at different spatial locations usually requires multiple stamping and registration steps. Here, we describe an experimental method based on reaction–diffusion phenomena that allows for simultaneous micropatterning of a substrate with several coloured chemicals. In this method, called wet stamping (WETS), aqueous solutions of two or more inorganic salts are delivered onto a film of dry, ionically doped gelatin from an agarose stamp patterned in bas relief. Once in conformal contact, these salts diffuse into the gelatin, where they react to give deeply coloured precipitates. Separation of colours in the plane of the surface is the consequence of the differences in the diffusion coefficients, the solubility products, and the amounts of different salts delivered from the stamp, and is faithfully reproduced by a theoretical model based on a system of reaction–diffusion partial differential equations. The multicolour micropatterns are useful as non-binary optical elements, and could potentially form the basis of new applications in microseparations and in controlled delivery.}, author = {Klajn, Rafal and Fialkowski, Marcin and Bensemann, Igor T. and Bitner, Agnieszka and Campbell, C. J. and Bishop, Kyle and Smoukov, Stoyan and Grzybowski, Bartosz A.}, issn = {1476-4660}, journal = {Nature Materials}, keywords = {Mechanical Engineering, Mechanics of Materials, Condensed Matter Physics, General Materials Science, General Chemistry}, pages = {729--735}, publisher = {Springer Nature}, title = {{Multicolour micropatterning of thin films of dry gels}}, doi = {10.1038/nmat1231}, volume = {3}, year = {2004}, } @article{902, abstract = {We compare the functional spectrum of protein evolution in two separate animal lineages with respect to two hypotheses: (1) rates of divergence are distributed similarly among functional classes within both lineages, indicating that selective pressure on the proteome is largely independent of organismic-level biological requirements; and (2) rates of divergence are distributed differently among functional classes within each lineage, indicating species-specific selective regimes impact genome-wide substitutional patterns. Integrating comparative genome sequence with data from tissue-specific expressed-sequence-tag (EST) libraries and detailed database annotations, we find a functional genomic signature of rapid evolution and selective constraint shared between mammalian and nematode lineages despite their extensive morphological and ecological differences and distant common ancestry. In both phyla, we find evidence of accelerated evolution among components of molecular systems involved in coevolutionary change. In mammals, lineage-specific fast evolving genes include those involved in reproduction, immunity, and possibly, maternal-fetal conflict. Likelihood ratio tests provide evidence for positive selection in these rapidly evolving functional categories in mammals. In contrast, slowly evolving genes, in terms of amino acid or insertion/deletion (indel) change, in both phyla are involved in core molecular processes such as transcription, translation, and protein transport. Thus, strong purifying selection appears to act on the same core cellular processes in both mammalian and nematode lineages, whereas positive and/or relaxed selection acts on different biological processes in each lineage.}, author = {Castillo-Davis, Cristian I and Fyodor Kondrashov and Hartl, Daniel L and Kulathinal, Rob J}, journal = {Genome Research}, number = {5}, pages = {802 -- 811}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{The functional genomic distribution of protein divergence in two animal phyla: Coevolution, genomic conflict, and constraint}}, doi = {10.1101/gr.2195604}, volume = {14}, year = {2004}, } @article{9454, author = {Chan, Simon W.-L. and Zilberman, Daniel and Xie, Zhixin and Johansen, Lisa K. and Carrington, James C. and Jacobsen, Steven E.}, issn = {1095-9203}, journal = {Science}, keywords = {Multidisciplinary}, number = {5662}, pages = {1336}, publisher = {American Association for the Advancement of Science}, title = {{RNA silencing genes control de novo DNA methylation}}, doi = {10.1126/science.1095989}, volume = {303}, year = {2004}, } @article{9493, abstract = {In a number of organisms, transgenes containing transcribed inverted repeats (IRs) that produce hairpin RNA can trigger RNA-mediated silencing, which is associated with 21-24 nucleotide small interfering RNAs (siRNAs). In plants, IR-driven RNA silencing also causes extensive cytosine methylation of homologous DNA in both the transgene "trigger" and any other homologous DNA sequences--"targets". Endogenous genomic sequences, including transposable elements and repeated elements, are also subject to RNA-mediated silencing. The RNA silencing gene ARGONAUTE4 (AGO4) is required for maintenance of DNA methylation at several endogenous loci and for the establishment of methylation at the FWA gene. Here, we show that mutation of AGO4 substantially reduces the maintenance of DNA methylation triggered by IR transgenes, but AGO4 loss-of-function does not block the initiation of DNA methylation by IRs. AGO4 primarily affects non-CG methylation of the target sequences, while the IR trigger sequences lose methylation in all sequence contexts. Finally, we find that AGO4 and the DRM methyltransferase genes are required for maintenance of siRNAs at a subset of endogenous sequences, but AGO4 is not required for the accumulation of IR-induced siRNAs or a number of endogenous siRNAs, suggesting that AGO4 may function downstream of siRNA production.}, author = {Zilberman, Daniel and Cao, Xiaofeng and Johansen, Lisa K. and Xie, Zhixin and Carrington, James C. and Jacobsen, Steven E.}, issn = {1879-0445}, journal = {Current Biology}, number = {13}, pages = {1214--1220}, publisher = {Elsevier}, title = {{Role of Arabidopsis ARGONAUTE4 in RNA-directed DNA methylation triggered by inverted repeats}}, doi = {10.1016/j.cub.2004.06.055}, volume = {14}, year = {2004}, } @article{9511, abstract = {Recent progress in understanding the silencing of transposable elements in the model plant Arabidopsis has revealed an interplay between DNA methylation, histone methylation and small interfering RNAs. DNA and histone methylation are not always sufficient to maintain silencing, and RNA-based reinforcement can be needed to maintain as well as initiate it.}, author = {Zilberman, Daniel and Henikoff, Steven}, issn = {1465-6906}, journal = {Genome Biology}, number = {12}, publisher = {Springer Nature}, title = {{Silencing of transposons in plant genomes: kick them when they're down}}, doi = {10.1186/gb-2004-5-12-249}, volume = {5}, year = {2004}, }