@article{1951, author = {Sazanov, Leonid A and Burrows, Paul and Nixon, Peter}, issn = {0300-5127}, journal = {Biochemical Society Transactions}, number = {3}, pages = {739 -- 743}, publisher = {Portland Press}, title = {{Detection and characterization of a complex I-like NADH-specific dehydrogenase from pea thylakoids}}, doi = {10.1042/bst0240739}, volume = {24}, year = {1996}, } @article{1952, abstract = {Two strains of Rhodospirillum rubrum were constructed in which, by a gene dosage effect, the transhydrogenase activity of isolated chromatophores was increased 7-10-fold and 15-20-fold, respectively. The H+/H- ratio (the ratio of protons translocated per hydride ion equivalent transferred from NADPH to an NAD+ analogue, acetyl pyridine adenine dinucleotide), determined by a spectroscopic technique, was approximately 1.0 for chromatophores from the over-expressing strains, but was only approximately 0.6 for wild-type chromatophores. Highly-coupled proteoliposomes were prepared containing purified transhydrogenase from beef-heart mitochondria. Using the same technique, the H+/H- ratio was close to 1.0 for these proteoliposomes. It is suggested that the mechanistic H+/H- ratio is indeed unity, but that a low ratio is obtained in wild-type chromatophores because of inhomogeneity in the vesicle population.}, author = {Bizouarn, Tania and Sazanov, Leonid A and Aubourg, Sébastien and Jackson, Julie}, issn = {0005-2728}, journal = {Biochimica et Biophysica Acta - Bioenergetics}, number = {1}, pages = {4 -- 12}, publisher = {Elsevier}, title = {{Estimation of the H+/H- ratio of the reaction catalysed by the nicotinamide nucleotide transhydrogenase in chromatophores from over-expressing strains of Rhodospirillum rubrum and in liposomes inlaid with the purified bovine enzyme}}, doi = {10.1016/0005-2728(95)00125-5}, volume = {1273}, year = {1996}, } @phdthesis{4419, abstract = {A {\em hybrid automaton\/} consists of a finite automaton interacting with a dynamical system. Hybrid automata are used to model embedded controllers and other systems that consist of interacting discrete and continuous components. A hybrid automaton is {\em rectangular\/} if each of its continuous variables~x satisfies a nondeterministic differential equation of the form a≤dxdt≤b, where a and~b are rational constants. Rectangular hybrid automata are particularly useful for the analysis of communication protocols in which local clocks have bounded drift, and for the conservative approximation of systems with more complex continuous behavior. We examine several verification problems on the class of rectangular hybrid automata, including reachability, temporal logic model checking, and controller synthesis. Both dense-time and discrete-time models are considered. We identify subclasses of rectangular hybrid automata for which these problems are decidable and give complexity analyses. An investigation of the structural properties of rectangular hybrid automata is undertaken. One method for proving the decidability of verification problems on infinite-state systems is to find finite quotient systems on which analysis can proceed. Three state-space equivalence relations with strong connections to temporal logic are bisimilarity, similarity, and language equivalence. We characterize the quotient spaces of rectangular hybrid automata with respect to these equivalence relations.}, author = {Kopke, Peter}, publisher = {Cornell University}, title = {{The Theory of Rectangular Hybrid Automata}}, year = {1996}, } @inproceedings{4426, abstract = {We use linear hybrid automata to define linear approximations of the phase portraits of nonlinear hybrid systems. The approximating automata can be analyzed automatically using the symbolic model checker HyTech. We demonstrate the technique through the study of predator-prey systems, where we compute population bounds for both species. We also identify a class of nonlinear hybrid automata for which linear phase-portrait approximations can be generated automatically.}, author = {Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Hybrid Systems III: Verification and Control}, editor = {Alur, Rajeev and Henzinger, Thomas A and Sontag, Eduardo}, isbn = {9783540611554}, pages = {377 -- 388}, publisher = {Springer}, title = {{Linear phase-portrait approximations for nonlinear hybrid systems}}, doi = {10.1007/BFb0020961}, volume = {1066}, year = {1996}, } @inbook{4427, abstract = {We model a steam-boiler control system using hybrid automata. We provide two abstracted linear models of the nonlinear behavior of the boiler. For each model, we define and verify a controller that maintains safe operation of the boiler. The less abstract model permits the design of a more efficient controller. We also demonstrate how the tool HyTech can be used to automatically synthesize control parameter constraints that guarantee safety of the boiler.}, author = {Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control}, isbn = {9783540495666}, pages = {265 -- 282}, publisher = {Springer}, title = {{Using HyTech to synthesize control parameters for a steam boiler}}, doi = {10.1007/BFb0027241}, volume = {1165}, year = {1996}, } @inproceedings{4443, abstract = {Three natural equivalence relations on the infinite state space of a hybrid automaton are language equivalence, simulation equivalence, and bisimulation equivalence. When one of these equivalence relations has a finite quotient, certain model checking and controller synthesis problems are decidable. When bounds on the number of equivalence classes are obtained, bounds on the running times of model checking and synthesis algorithms follow as corollaries. We characterize the time-abstract versions of these equivalence relations on the state spaces of rectangular hybrid automata (RHA), in which each continuous variable is a clock with bounded drift. These automata are useful for modeling communications protocols with drifting local clocks, and for the conservative approximation of more complex hybrid systems. Of our two main results, one has positive implications for automatic verification, and the other has negative implications. On the positive side, we find that the (finite) language equivalence quotient for RHA is coarser than was previously known by a multiplicative exponential factor. On the negative side, we show that simulation equivalence for RHA is equality (which obviously has an infinite quotient). Our main positive result is established by analyzing a subclass of timed automata, called one-sided timed automata (OTA), for which the language equivalence quotient is coarser than for the class of all timed automata. An exact characterization of language equivalence for OTA requires a distinction between synchronous and asynchronous definitions of (bi)simulation: if time actions are silent, then the induced quotient for OTA is coarser than if time actions (but not their durations) are visible.}, author = {Henzinger, Thomas A and Kopke, Peter}, booktitle = {7th International Conference on Concurrency Theory}, isbn = {9783540616047}, location = {Pisa, Italy}, pages = {530 -- 545}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{State equivalences for rectangular hybrid automata}}, doi = {10.1007/3-540-61604-7_74}, volume = {1119}, year = {1996}, } @inproceedings{4495, abstract = {In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The main practical limitation of model checking is caused by the size of the state space of the program, which grows exponentially with the number of concurrent components. This problem, known as the state-explosion problem, becomes more difficult when we consider real-time model checking, where the program and the specification involve quantitative references to time. In particular, when use timed automata to describe real-time programs and we specify timed behaviors in the logic TCTL, a real-time extension of the temporal logic CTL with clock variables, then the state space under consideration grows exponentially not only with the number of concurrent components, but also with the number of clocks and the length of the clock constraints used in the program and the specification. Two powerful methods for coping with the state-explosion problem are on-the-fly and space-efficient model checking. In on-the-fly model checking, we explore only the portion of the state space of the program whose exploration is essential for determining the satisfaction of the specification. In space-efficient model checking, we store in memory the minimal information required, preferring to spend time on reconstructing information rather than spend space on storing it. In this work we develop an automata-theoretic approach to TCTL model checking that combines both methods. We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for TCTL.}, author = {Henzinger, Thomas A and Kupferman, Orna and Vardi, Moshe}, booktitle = {7th International Conference on Concurrency Theory}, isbn = {978-3-540-70625-0}, location = {Pisa, Italy}, pages = {514 -- 529}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{A space-efficient on-the-fly algorithm for real-time model checking}}, doi = {10.1007/3-540-61604-7_73}, volume = {1119}, year = {1996}, } @inproceedings{4519, abstract = {We summarize several recent results about hybrid automata. Our goal is to demonstrate that concepts from the theory of discrete concurrent systems can give insights into partly continuous systems, and that methods for the verification of finite-state systems can be used to analyze certain systems with uncountable state spaces}, author = {Henzinger, Thomas A}, booktitle = {Proceedings 11th Annual IEEE Symposium on Logic in Computer Science}, issn = {1043-6871}, location = {New Brunswick, NJ, United States of America}, pages = {278 -- 292}, publisher = {IEEE}, title = {{The theory of hybrid automata}}, doi = {10.1109/LICS.1996.561342 }, year = {1996}, } @proceedings{4585, editor = {Henzinger, Thomas A and Alur, Rajeev}, location = {New Brunswick, NJ, United States of America}, publisher = {Springer}, title = {{ 8th International Conference on Computer Aided Verification}}, doi = {10.1007/3-540-61474-5}, volume = {1102}, year = {1996}, } @inproceedings{4588, abstract = {We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise refinement) reasoning. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message passing}, author = {Alur, Rajeev and Henzinger, Thomas A}, booktitle = {Proceedings 11th Annual IEEE Symposium on Logic in Computer Science}, issn = {0018-9162}, location = {New Brunswick, NJ, USA}, pages = {207 -- 218}, publisher = {IEEE}, title = {{Reactive modules}}, doi = {10.1109/LICS.1996.561320}, year = {1996}, } @article{4610, abstract = {The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability of timing constraints that are capable of expressing punctuality in this model, however, is known to be undecidable. We introduce a temporal language that can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics.}, author = {Alur, Rajeev and Feder, Tomás and Henzinger, Thomas A}, issn = {0004-5411}, journal = {Journal of the ACM}, number = {1}, pages = {116 -- 146}, publisher = {ACM}, title = {{The benefits of relaxing punctuality}}, doi = {10.1145/227595.227602}, volume = {43}, year = {1996}, } @article{4611, abstract = {Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms}, author = {Alur, Rajeev and Henzinger, Thomas A and Ho, Pei}, issn = {0018-9162}, journal = {IEEE Transactions on Software Engineering}, number = {3}, pages = {181 -- 201}, publisher = {IEEE}, title = {{Automatic symbolic verification of embedded systems}}, doi = {10.1109/32.489079}, volume = {22}, year = {1996}, } @book{4612, editor = {Alur, Rajeev and Henzinger, Thomas A and Sontag, Eduardo D}, isbn = {978-3-540-61155-4}, issn = {0302-9743}, pages = {IX, 619}, publisher = {Springer}, title = {{Hybrid Systems III: Verification and Control}}, doi = {10.1007/BFb0020931}, volume = {1066}, year = {1996}, } @article{6161, abstract = {The tra-1 gene is a terminal regulator of somatic sex in Caenorhabditis elegans: high tra-1 activity elicits female development, low tra-1 activity elicits male development. To investigate the function and evolution of tra- 1, we examined the tra-1 gene from the closely related nematode C. briggsae. Ce-tra-1 and Cb-tra-1 are unusually divergent. Each gene generates two transcripts, but only one of these is present in both species. This common transcript encodes TRA-1A, which shows only 44% amino acid identity between the species, a figure much lower than that for previously compared genes. A Cb-tra-1 transgene rescues many tissues of tra-1(null) mutants of C. elegans but not the somatic gonad or germ line. This transgene also causes nongonadal feminization of XO animals, indicating incorrect sexual regulation. Alignment of Ce-TRA-1A and Cb-TRA-1A defined several conserved regions likely to be important for tra-1 function. The phenotype differences between Ce-tra- 1(null) mutants rescued by Cb-tra-1 transgenes and wild-type C. elegans indicate significant divergence of regulatory regions. These molecular and functional studies suggest that evolution of sex determination in nematodes is rapid and genetically complex.}, author = {de Bono, Mario and Hodgkin, J.}, issn = {00166731}, journal = {Genetics}, keywords = {amino acid sequence, article, caenorhabditis elegans, evolution, genetic variability, nonhuman, priority journal, sex determination, Amino Acid Sequence, Animals, Animals, Genetically Modified, Base Sequence, Caenorhabditis, Caenorhabditis elegans, Caenorhabditis elegans Proteins, DNA, Helminth, DNA-Binding Proteins, Evolution, Molecular, Female, Helminth Proteins, Membrane Proteins, Molecular Sequence Data, Mutagenesis, RNA, Messenger, Sequence Homology, Amino Acid, Sex Determination (Analysis), Transcription Factors, Transgenes, Turner Syndrome, Animalia, Caenorhabditis, Caenorhabditis briggsae, Caenorhabditis elegans, Nematoda}, number = {2}, pages = {587--595}, publisher = {Genetics Society of America}, title = {{Evolution of sex determination in Caenorhabditis: Unusually high divergence of tra-1 and its functional consequences}}, volume = {144}, year = {1996}, } @article{3462, author = {Melcher, Thorsten and Geiger, Jörg and Jonas, Peter M and Monyer, Hannah}, issn = {0197-0186}, journal = {Neurochemistry International}, number = {2}, pages = {141 -- 144}, publisher = {Elsevier}, title = {{Analysis of molecular determinants in native AMPA receptors}}, doi = {10.1016/0197-0186(95)00077-1}, volume = {28}, year = {1996}, } @inproceedings{3553, abstract = {Virtual environments open up new opportunities and challenges for geometric modeling systems. A general approach to geometric modeling suitable for the Cave Automatic Virtual Environment is described. The approach is based on alpha complexes, and some of its capabilities are demonstrated by applying it to the study of biomolecules.}, author = {Edelsbrunner, Herbert and Fu, Ping and Quian, Jiang}, booktitle = {Proceedings of the ACM Symposium on Virtual Reality Software and Technology}, isbn = {9780897918251}, location = {Hong Kong}, pages = {35--41 and -- 193--194}, publisher = {ACM}, title = {{Geometric modeling in CAVE}}, doi = {10.1145/3304181.3304190}, year = {1996}, } @article{3634, abstract = {The evolutionary processes responsible for adaptation and speciation on islands differ in several ways from those on the mainland. Most attention has been given to the random genetic drift that arises when a population is founded from just a few colonizing genomes. Theoretical obstacles to 'founder effect speciation' are discussed, together with recent proposals for avoiding them. It is argued that although certain kinds of epistasis can facilitate the evolution of strong reproductive isolation, this favours divergence by selection as much as by random drift.}, author = {Barton, Nicholas H and Mallet, James}, issn = {0962-8436}, journal = {Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences}, number = {1341}, pages = {785 -- 795}, publisher = {Royal Society of London}, title = {{Natural selection and random genetic drift as causes of evolution on islands}}, doi = {10.1098/rstb.1996.0073}, volume = {351}, year = {1996}, } @article{3635, abstract = {Experiments on Drosophila suggest that genetic recombination may result in lowered fitness of progeny (a 'recombination load'). This has been interpreted as evidence either for a direct effect of recombination on fitness, or for the maintenance of linkage disequilibria by epistatic selection. Here we show that such a recombination load is to be expected even if selection favours increased genetic recombination. This is because of the fact that, although a modifier may suffer an immediate loss of fitness if it increases recombination, it eventually becomes associated with a higher additive genetic variance in fitness, which allows a faster response to direction selection. This argument applies to mutation-selection balance with synergistic epistasis, directional selection on quantitative traits, and ectopic exchange among transposable elements. Further experiments are needed to determine whether the selection against recombination due to the immediate load is outweighed by the increased additive variance in fitness produced by recombination.}, author = {Charlesworth, Brian and Barton, Nicholas H}, issn = {0016-6723}, journal = {Genetical Research}, number = {1}, pages = {27 -- 41}, publisher = {Cambridge University Press}, title = {{Recombination load associated with selection for increased recombination}}, doi = {10.1017/S0016672300033450}, volume = {67}, year = {1996}, } @article{3756, abstract = {In many eukaryotic cells going through M-phase, a bipolar spindle is formed by microtubules nucleated from centrosomes. These microtubules, in addition to being `'captured” by kinetochores, may be stabilized by chromatin in two different ways: short-range stabilization effects may affect microtubules in close contact with the chromatin, while long-range stabilization effects may `'guide” microtubule growth towards the chromatin (e.g., by introducing a diffusive gradient of an enzymatic activity that affects microtubule assembly). Here, we use both meiotic and mitotic extracts from Xenopus laevis eggs to study microtubule aster formation and microtubule dynamics in the presence of chromatin. In `'low-speed” meiotic extracts, in the presence of salmon sperm chromatin, we find that short-range stabilization effects lead to a strong anisotropy of the microtubule asters. Analysis of the dynamic parameters of microtubule growth shows that this anisotropy arises from a decrease in the catastrophe frequency, an increase in the rescue frequency and a decrease in the growth velocity. In this system we also find evidence for long-range `'guidance” effects, which lead to a weak anisotropy of the asters. Statistically relevant results on these long-range effects are obtained in `'high-speed” mitotic extracts in the presence of artificially constructed chromatin stripes. We find that aster anisotropy is biased in the direction of the chromatin and that the catastrophe frequency is reduced in its vicinity. In this system we also find a surprising dependence of the catastrophe and the rescue frequencies on the length of microtubules nucleated from centrosomes: the catastrophe frequency increases and the rescue frequency decreases with microtubule length.}, author = {Dogterom, Marileen and Felix, M. and Guet, Calin C and Leibler, Stanislas}, issn = {0021-9525}, journal = {Journal of Cell Biology}, number = {1}, pages = {125 -- 140}, publisher = {Rockefeller University Press}, title = {{Influence of M-phase chromatin on the anisotropy of microtubule asters}}, doi = {doi: 10.1083/jcb.133.1.125 }, volume = {133}, year = {1996}, } @article{4024, abstract = {We have developed general modeling software for a Cave Automatic Virtual Environment (CAVE); one of its applications is modeling 3D protein structures, generating both outside-in and inside-out views of geometric models. An advantage of the CAVE over other virtual environments is that multiple viewers can observe the same scene at the same time and place. Our software is scalable-from high-end virtual environments such as the CAVE, to mid-range immersive desktop systems, down to low-end graphics workstations. In the current configuration, a parallel Silicon Graphics Power Challenge supercomputer architecture performs the computationally intensive construction of surface patches remotely, and sends the results through the I-WAY (Information Wide Area Year) using VBNS (Very-high-Bandwidth Network Systems) to the graphics machines that drive the CAVE and our graphics visualization software, Valvis (Virtual ALpha shapes VISualizer).}, author = {Akkiraju, Nataraj and Edelsbrunner, Herbert and Fu, Ping and Qian, Jiang}, issn = {0018-9162}, journal = {IEEE Computer Graphics and Applications}, number = {4}, pages = {58 -- 61}, publisher = {IEEE}, title = {{Viewing geometric protein structures from inside a CAVE}}, doi = {10.1109/38.511855}, volume = {16}, year = {1996}, }