@inproceedings{4527, abstract = {We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification. We use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings.}, author = {Fisher, Jasmin and Thomas Henzinger and Maria Mateescu and Piterman, Nir}, pages = {17 -- 32}, publisher = {Springer}, title = {{Bounded asynchrony: Concurrency for modeling cell-cell interactions}}, doi = {10.1007/978-3-540-68413-8_2}, volume = {5054}, year = {2008}, } @article{4532, abstract = {We consider the equivalence problem for labeled Markov chains (LMCs), where each state is labeled with an observation. Two LMCs are equivalent if every finite sequence of observations has the same probability of occurrence in the two LMCs. We show that equivalence can be decided in polynomial time, using a reduction to the equivalence problem for probabilistic automata, which is known to be solvable in polynomial time. We provide an alternative algorithm to solve the equivalence problem, which is based on a new definition of bisimulation for probabilistic automata. We also extend the technique to decide the equivalence of weighted probabilistic automata.}, author = {Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François}, journal = {International Journal of Foundations of Computer Science}, number = {3}, pages = {549 -- 563}, publisher = {World Scientific Publishing}, title = {{Equivalence of labeled Markov chains}}, doi = {10.1142/S0129054108005814 }, volume = {19}, year = {2008}, } @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{12201, abstract = {The development of plant lateral organs is interesting because, although many of the same genes seem to be involved in the early growth of primordia, completely different gene combinations are required for the complete development of organs such as leaves and stamens. Thus, the genes common to the development of most organs, which generally form and polarize the primordial ‘envelope’, must at some stage interact with those that ‘install’ the functional content of the organ – in the case of the stamen, the four microsporangia. Although distinct genetic pathways of organ initiation, polarity establishment and setting up the reproductive cell line can readily be recognized, they do not occur sequentially. Rather, they are activated early and run in parallel. There is evidence for continuing crosstalk between these pathways.}, author = {Feng, Xiaoqi and Dickinson, Hugh G.}, issn = {0168-9525}, journal = {Trends in Genetics}, keywords = {Genetics}, number = {10}, pages = {503--510}, publisher = {Elsevier BV}, title = {{Packaging the male germline in plants}}, doi = {10.1016/j.tig.2007.08.005}, volume = {23}, year = {2007}, } @article{128, abstract = {A 671 nm diode laser with a mode-hop-free tuning range of 40 GHz is described. This long tuning range is achieved by simultaneously ramping the external cavity length with the laser injection current. The laser output pointing remains fixed, independent of its frequency because of the cover slip cavity design. This system is simple, economical, robust, and easy to use for spectroscopy, as we demonstrate with lithium vapor and lithium atom beam experiments. }, author = {Carr, Adra and Serchest, Yancey and Waitukaitis, Scott R and Perreault, John and Lonij, Vincent and Cronin, Alexander}, journal = {Review of Scientific Instruments}, number = {10}, publisher = {American Institute of Physics}, title = {{Cover slip external cavity diode laser}}, doi = {10.1063/1.2801006}, volume = {78}, year = {2007}, } @article{1297, abstract = {In flies, the large tangential cells of the lobula plate represent an important processing center for visual navigation based on optic flow. Although the visual response properties of these cells have been well studied in blowflies, information on their synaptic organization is mostly lacking. Here we study the distribution of presynaptic release and postsynaptic inhibitory sites in the same set of cells in Drosophila melanogaster. By making use of transgenic tools and immunohistochemistry, our results suggest that HS and VS cells of Drosophila express γ-aminobutyric acid (GABA) receptors in their dendritic region within the lobula plate, thus being postsynaptic to inhibitory input there. At their axon terminals in the protocerebrum, both cell types express synaptobrevin, suggesting the presence of presynaptic specializations there. HS- and VS-cell terminals additionally show evidence for postsynaptic GABAergic input, superimposed on this synaptic polarity. Our findings are in line with the general circuit for visual motion detection and receptive field properties as postulated from electrophysiological and optical recordings in blowflies, suggesting a similar functional organization of lobula plate tangential cells in the two species.}, author = {Raghu, Shamprasad V and Maximilian Jösch and Borst, Alexander and Reiff, Dierk F}, journal = {Journal of Comparative Neurology}, number = {4}, pages = {598 -- 610}, publisher = {Wiley-Blackwell}, title = {{Synaptic organization of lobula plate tangential cells in Drosophila: γ-aminobutyric acid receptors and chemical release sites}}, doi = {10.1002/cne.21319}, volume = {502}, year = {2007}, } @article{8483, abstract = {Atom-resolved real-time studies of kinetic processes in proteins have been hampered in the past by the lack of experimental techniques that yield sufficient temporal and atomic resolution. Here we present band-selective optimized flip-angle short transient (SOFAST) real-time 2D NMR spectroscopy, a method that allows simultaneous observation of reaction kinetics for a large number of nuclear sites along the polypeptide chain of a protein with an unprecedented time resolution of a few seconds. SOFAST real-time 2D NMR spectroscopy combines fast NMR data acquisition techniques with rapid sample mixing inside the NMR magnet to initiate the kinetic event. We demonstrate the use of SOFAST real-time 2D NMR to monitor the conformational transition of α-lactalbumin from a molten globular to the native state for a large number of amide sites along the polypeptide chain. The kinetic behavior observed for the disappearance of the molten globule and the appearance of the native state is monoexponential and uniform along the polypeptide chain. This observation confirms previous findings that a single transition state ensemble controls folding of α-lactalbumin from the molten globule to the native state. In a second application, the spontaneous unfolding of native ubiquitin under nondenaturing conditions is characterized by amide hydrogen exchange rate constants measured at high pH by using SOFAST real-time 2D NMR. Our data reveal that ubiquitin unfolds in a gradual manner with distinct unfolding regimes.}, author = {Schanda, Paul and Forge, V. and Brutscher, B.}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, keywords = {Multidisciplinary}, number = {27}, pages = {11257--11262}, publisher = {National Academy of Sciences}, title = {{Protein folding and unfolding studied at atomic resolution by fast two-dimensional NMR spectroscopy}}, doi = {10.1073/pnas.0702069104}, volume = {104}, year = {2007}, } @article{8484, abstract = {A series of sequential, intra-residue, and bi-directional BEST H–N–CA, H–N–CO, and H–N–CB pulse sequences is presented that extends the BEST concept introduced recently for fast multidimensional protein NMR [Schanda et al., J. Am. Chem. Soc. 128 (2006) 9042] to the complete set of experiments required for sequential resonance assignment. We demonstrate for the protein ubiquitin that 3D BEST H–N–C correlation spectra can be recorded on a 600 MHz NMR spectrometer equipped with a cryogenic probe in only a few minutes of acquisition time with sufficient sensitivity to detect all expected cross peaks.}, author = {Lescop, Ewen and Schanda, Paul and Brutscher, Bernhard}, issn = {1090-7807}, journal = {Journal of Magnetic Resonance}, number = {1}, pages = {163--169}, publisher = {Elsevier}, title = {{A set of BEST triple-resonance experiments for time-optimized protein resonance assignment}}, doi = {10.1016/j.jmr.2007.04.002}, volume = {187}, year = {2007}, } @article{8485, abstract = {High signal to noise is a necessity for the quantification of NMR spectral parameters to be translated into accurate and precise restraints on protein structure and dynamics. An important source of long-range structural information is obtained from 1H–1H residual dipolar couplings (RDCs) measured for weakly aligned molecules. For sensitivity reasons, such measurements are generally performed on highly deuterated protein samples. Here we show that high sensitivity is also obtained for protonated protein samples if the pulse schemes are optimized in terms of longitudinal relaxation efficiency and J-mismatch compensated coherence transfer. The new sensitivity-optimized quantitative J-correlation experiment yields important signal gains reaching factors of 1.5 to 8 for individual correlation peaks when compared to previously proposed pulse schemes.}, author = {Schanda, Paul and Lescop, Ewen and Falge, Mirjam and Sounier, Rémy and Boisbouvier, Jérôme and Brutscher, Bernhard}, issn = {0925-2738}, journal = {Journal of Biomolecular NMR}, keywords = {Spectroscopy, Biochemistry}, pages = {47--55}, publisher = {Springer Nature}, title = {{Sensitivity-optimized experiment for the measurement of residual dipolar couplings between amide protons}}, doi = {10.1007/s10858-006-9138-2}, volume = {38}, year = {2007}, } @article{8486, abstract = {A technique is described that allows reducing acquisition times of multidimensional NMR experiments by extensive spectral folding. The method is simple and has many interesting applications for NMR studies of molecular structure, dynamics, and kinetics.}, author = {Lescop, Ewen and Schanda, Paul and Rasia, Rodolfo and Brutscher, Bernhard}, issn = {0002-7863}, journal = {Journal of the American Chemical Society}, keywords = {Colloid and Surface Chemistry, Biochemistry, General Chemistry, Catalysis}, number = {10}, pages = {2756--2757}, publisher = {American Chemical Society}, title = {{Automated spectral compression for fast multidimensional NMR and increased time resolution in real-time NMR spectroscopy}}, doi = {10.1021/ja068949u}, volume = {129}, year = {2007}, } @article{8487, abstract = {Following unidirectional biophysical events such as the folding of proteins or the equilibration of binding interactions, requires experimental methods that yield information at both atomic-level resolution and at high repetition rates. Toward this end a number of different approaches enabling the rapid acquisition of 2D NMR spectra have been recently introduced, including spatially encoded “ultrafast” 2D NMR spectroscopy and SOFAST HMQC NMR. Whereas the former accelerates acquisitions by reducing the number of scans that are necessary for completing arbitrary 2D NMR experiments, the latter operates by reducing the delay between consecutive scans while preserving sensitivity. Given the complementarities between these two approaches it seems natural to combine them into a single tool, enabling the acquisition of full 2D protein NMR spectra at high repetition rates. We demonstrate here this capability with the introduction of “ultraSOFAST” HMQC NMR, a spatially encoded and relaxation-optimized approach that can provide 2D protein correlation spectra at ∼1 s repetition rates for samples in the ∼2 mM concentration range. The principles, relative advantages, and current limitations of this new approach are discussed, and its application is exemplified with a study of the fast hydrogen−deuterium exchange characterizing amide sites in Ubiquitin.}, author = {Gal, Maayan and Schanda, Paul and Brutscher, Bernhard and Frydman, Lucio}, issn = {0002-7863}, journal = {Journal of the American Chemical Society}, keywords = {Colloid and Surface Chemistry, Biochemistry, General Chemistry, Catalysis}, number = {5}, pages = {1372--1377}, publisher = {American Chemical Society}, title = {{UltraSOFAST HMQC NMR and the repetitive acquisition of 2D protein spectra at Hz rates}}, doi = {10.1021/ja066915g}, volume = {129}, year = {2007}, } @article{8511, abstract = {Here we study an amazing phenomenon discovered by Newhouse [S. Newhouse, Non-density of Axiom A(a) on S2, in: Proc. Sympos. Pure Math., vol. 14, Amer. Math. Soc., 1970, pp. 191–202; S. Newhouse, Diffeomorphisms with infinitely many sinks, Topology 13 (1974) 9–18; S. Newhouse, The abundance of wild hyperbolic sets and nonsmooth stable sets of diffeomorphisms, Publ. Math. Inst. Hautes Études Sci. 50 (1979) 101–151]. It turns out that in the space of Cr smooth diffeomorphisms Diffr(M) of a compact surface M there is an open set U such that a Baire generic diffeomorphism f ∈ U has infinitely many coexisting sinks. In this paper we make a step towards understanding “how often does a surface diffeomorphism have infinitely many sinks.” Our main result roughly says that with probability one for any positive D a surface diffeomorphism has only finitely many localized sinks either of cyclicity bounded by D or those whose period is relatively large compared to its cyclicity. It verifies a particular case of Palis’ Conjecture saying that even though diffeomorphisms with infinitely many coexisting sinks are Baire generic, they have probability zero. One of the key points of the proof is an application of Newton Interpolation Polynomials to study the dynamics initiated in [V. Kaloshin, B. Hunt, A stretched exponential bound on the rate of growth of the number of periodic points for prevalent diffeomorphisms I, Ann. of Math., in press, 92 pp.; V. Kaloshin, A stretched exponential bound on the rate of growth of the number of periodic points for prevalent diffeomorphisms II, preprint, 85 pp.].}, author = {Gorodetski, A. and Kaloshin, Vadim}, issn = {0001-8708}, journal = {Advances in Mathematics}, keywords = {General Mathematics}, number = {2}, pages = {710--797}, publisher = {Elsevier}, title = {{How often surface diffeomorphisms have infinitely many sinks and hyperbolicity of periodic points near a homoclinic tangency}}, doi = {10.1016/j.aim.2006.03.012}, volume = {208}, year = {2007}, } @article{8512, abstract = {For diffeomorphisms of smooth compact finite-dimensional manifolds, we consider the problem of how fast the number of periodic points with period n grows as a function of n. In many familiar cases (e.g., Anosov systems) the growth is exponential, but arbitrarily fast growth is possible; in fact, the first author has shown that arbitrarily fast growth is topologically (Baire) generic for C2 or smoother diffeomorphisms. In the present work we show that, by contrast, for a measure-theoretic notion of genericity we call “prevalence”, the growth is not much faster than exponential. Specifically, we show that for each ρ,δ>0, there is a prevalent set of C1+ρ (or smoother) diffeomorphisms for which the number of periodic n points is bounded above by exp(Cn1+δ) for some C independent of n. We also obtain a related bound on the decay of hyperbolicity of the periodic points as a function of n, and obtain the same results for 1-dimensional endomorphisms. The contrast between topologically generic and measure-theoretically generic behavior for the growth of the number of periodic points and the decay of their hyperbolicity show this to be a subtle and complex phenomenon, reminiscent of KAM theory. Here in Part I we state our results and describe the methods we use. We complete most of the proof in the 1-dimensional C2-smooth case and outline the remaining steps, deferred to Part II, that are needed to establish the general case. The novel feature of the approach we develop in this paper is the introduction of Newton Interpolation Polynomials as a tool for perturbing trajectories of iterated maps.}, author = {Kaloshin, Vadim and Hunt, Brian}, issn = {0003-486X}, journal = {Annals of Mathematics}, number = {1}, pages = {89--170}, publisher = {Princeton University Press}, title = {{Stretched exponential estimates on growth of the number of periodic points for prevalent diffeomorphisms I}}, doi = {10.4007/annals.2007.165.89}, volume = {165}, year = {2007}, } @article{860, abstract = {We identified a mutation in the CRYGD gene (P23S) of the γ-crystallin gene cluster that is associated with a polymorphic congenital cataract that occurs with frequency of ∼0.3% in a human population. To gain insight into the molecular mechanism of the pathogenesis of γ-crystallin isoforms, we undertook an evolutionary analysis of the available mammalian and newly obtained primate sequences of the γ-crystallin genes. The cataract-associated serine at site 23 corresponds to the ancestral state, since it was found in CRYGD of a lower primate and all the surveyed nonprimate mammals. Crystallin proteins include two structurally similar domains, and substitutions in mammalian CRYGD protein at site 23 of the first domain were always associated with substitutions in the structurally reciprocal sites 109 and 136 of the second domain. These data suggest that the cataractogenic effect of serine at site 23 in the N-terminal domain of CRYGD may be compensated indirectly by amino acid changes in a distal domain. We also found that gene conversion was a factor in the evolution of the γ-crystallin gene cluster throughout different mammalian clades. The high rate of gene conversion observed between the functional CRYGD gene and two primate γ-crystallin pseudogenes (CRYGEP1 and CRYGFP1) coupled with a surprising finding of apparent negative selection in primate pseudogenes suggest a deleterious impact of recently derived pseudogenes involved in gene conversion in the γ-crystallin gene cluster.}, author = {Plotnikova, Olga V and Fyodor Kondrashov and Vlasov, Peter K and Grigorenko, Anastasia P and Ginter, Evgeny K and Rogaev, Evgeny I}, journal = {American Journal of Human Genetics}, number = {1}, pages = {32 -- 43}, publisher = {Cell Press}, title = {{Conversion and compensatory evolution of the γ-crystallin genes and identification of a cataractogenic mutation that reverses the sequence of the human CRYGD gene to an ancestral state}}, doi = {10.1086/518616}, volume = {81}, year = {2007}, } @article{861, abstract = {Background: Mitochondrial tRNAs have been the subject of study for structural biologists interested in their secondary structure characteristics, evolutionary biologists have researched patterns of compensatory and structural evolution and medical studies have been directed towards understanding the basis of human disease. However, an up to date, manually curated database of mitochondrially encoded tRNAs from higher animals is currently not available. Description: We obtained the complete mitochondrial sequence for 277 tetrapod species from GenBank and re-annotated all of the tRNAs based on a multiple alignment of each tRNA gene and secondary structure prediction made independently for each tRNA. The mitochondrial (mt) tRNA sequences and the secondary structure based multiple alignments are freely available as Supplemental Information online. Conclusion: We compiled a manually curated database of mitochondrially encoded tRNAs from tetrapods with completely sequenced genomes. In the course of our work, we reannotated more than 10% of all tetrapod mt-tRNAs and subsequently predicted the secondary structures of 6060 mitochondrial tRNAs. This carefully constructed database can be utilized to enhance our knowledge in several different fields including the evolution of mt-tRNA secondary structure and prediction of pathogenic mt-tRNA mutations. In addition, researchers reporting novel mitochondrial genome sequences should check their tRNA gene annotations against our database to ensure a higher level of fidelity of their annotation.}, author = {Popadin, Konstantin Yu and Mamirova, Leila A and Fyodor Kondrashov}, journal = {BMC Bioinformatics}, publisher = {BioMed Central}, title = {{A manually curated database of tetrapod mitochondrially encoded tRNA sequences and secondary structures}}, doi = {10.1186/1471-2105-8-441}, volume = {8}, year = {2007}, }