@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}, } @inproceedings{11804, abstract = {This paper shows how a general technique, called lock-step search, used in dynamic graph algorithms, can be used to improve the running time of two problems arising in program verification and communication protocol design. (1)We consider the nonemptiness problem for Streett automata: We are given a directed graph G = (V, E) with n = ¦V¦ and m = ¦E¦, and a collection of pairs of subsets of vertices, called Streett pairs,〈L i , U i 〉, i = 1.k. The question is whether G has a cycle (not necessarily simple) which, for each 1 ≤ i ≤ k, if it contains a vertex from L i then it also contains a vertex of U i . Let b=Σ i=1..k |L i |+|U i |. The previously best algorithm takes time O((m + b) min{n, k}). We present an algorithm that takes time 𝑂(𝑚min{𝑚𝑙𝑜𝑔𝑛,‾‾‾‾‾‾√𝑘,𝑛}+𝑏𝑚𝑖𝑛{𝑙𝑜𝑔𝑛,𝑘}). (2)In communication protocol pruning we are given a directed graph G = (V, E) with l special vertices. The problem is to efficiently maintain the strongly-connected components of the special vertices on a restricted set of edge deletions. Let m i be the number of edges in the strongly connected component of the ith special vertex. The previously best algorithm repeatedly recomputes the strongly-connected components which leads to a running time of O(Σ i m 2i). We present an algorithm with time 𝑂(𝑙√∑𝑖𝑚1.5𝑖).}, author = {Henzinger, Monika H and Telle, Jan Arne}, booktitle = {5th Scandinavian Workshop on Algorithm Theory}, isbn = {9783540614227}, issn = {1611-3349}, location = {Reykjavik, Iceland}, pages = {16–27}, publisher = {Springer Nature}, title = {{Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning}}, doi = {10.1007/3-540-61422-2_117}, volume = {1097}, year = {1996}, } @inproceedings{11910, abstract = {We state a new sampling lemma and use it to improve the running time of dynamic graph algorithms. For the dynamic connectivity problem the previously best randomized algorithm takes expected time O(log3 n) per update, amortized over Ω(m) updates. Using the new sampling lemma, we improve its running time to O(log2 n). There exists a lower bound in the cell probe model for the time per operation of Ω(log n/ log log n) for this problem. Similarly improved running times are achieved for 2-edge connectivity, k-weight minimum spanning tree, and bipartiteness.}, author = {Henzinger, Monika H and Thorup, Mikkel}, booktitle = {23rd International Colloquium on Automata, Languages, and Programming}, isbn = {9783540614401}, issn = {1611-3349}, location = {Paderborn, Germany}, pages = {290--299}, publisher = {Springer Nature}, title = {{Improved sampling with applications to dynamic graph algorithms}}, doi = {10.1007/3-540-61440-0_136}, volume = {1099}, year = {1996}, } @inproceedings{11927, abstract = {We are given a set 7 = {Tl , Tz, . . . , Tk} of rooted binary trees, each Ti leaf-labeled by a subset L(x) c {1,2 )...) n}. IfT is a tree on {1,2, . . , n}, we let T]L denote the subtree of T induced by the nodes of L and all their ancestors. The consensus tree problem asks whether there exists a tree T* such that for every I, T’ IC(Ti) is homeomorphic to Ti. We present algorithms which test if a given set of trees has a consensus tree and if so, construct one. The deterministic algorithm takes time min{O(mn’/‘), O(m + n2 logn)}, where m = Ci IZl and uses linear space. The randomized algorithm takes time O(m log3 n) and uses linear space. The previous best for this problem was an 1981 O(mn) algorithm by Aho et al. Our faster deterministic algorithm uses a new efficient algorithm for the following interesting dynamic graph problem: Given a graph G with n nodes and m edges and a sequence of b batches of one or more edge deletions, then after each batch, either find a new component that has just been created or determine that there is no such component. For this problem, we have a simple algorithm with running time O(n2 log n + be min{ n2, m log n}), where be is the number of batches which do not result in a new component. For our particular application, bc 5 1. If all edges are deleted, then the best previously known deterministic algorithm requires time O(mJ;ii) to solve this problem. computational evolutionary biology. The first application is in the problem of inferring consensus of trees when there can be disagreement[l6]. There have, been several models suggested for this problem[2, 3, 4, 8, ?, 11, 17, 181, of which one is called the Local Consensus Tree[l5]. The local consensus tree model presumes that the user provides a local consensus rule which determines the form of the output tree on (perhaps) each triple of leaves, and the objective is to determine whether a tree exists which is consistent with each of the constraints. We will show that we can construct the local consensus tree of k trees on n species in O(kn3) time, improving on the O(lcn3 + n”) running time if we use the Aho et al algorithm. The second application is a heuristic for constructing the maximum likelihood tree based upon combining solutions to small subproblems. This is a simple and yet potentially significantly interesting approach to the evolutionary tree construction problem. }, author = {Henzinger, Monika H and King, Valerie and Warnow, Tandy}, booktitle = {7th Annual ACM-SIAM Symposium on Discrete Algorithms}, isbn = {0898713668}, location = {Atlanta, GA, United States}, pages = {333 --340}, publisher = {Society for Industrial and Applied Mathematics}, title = {{Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology}}, 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}, } @article{4025, abstract = {Questions of chemical reactivity can often be cast as questions of molecular geometry. Common geometric models for proteins and other molecules are the space-filling diagram, the solvent accessible surface and the molecular surface. In this paper we present a new approach to triangulating the surface of a molecule under the three models, which is fast, robust, and results in topologically correct triangulations. Our computations are based on a simplicial complex dual to the molecule models. All proposed algorithms are parallelizable.}, author = {Akkiraju, Nataraj and Edelsbrunner, Herbert}, issn = {0166-218X}, journal = {Discrete Applied Mathematics}, number = {1-3}, pages = {5 -- 22}, publisher = {Elsevier}, title = {{Triangulating the surface of a molecule}}, doi = {10.1016/S0166-218X(96)00054-6}, volume = {71}, year = {1996}, } @article{4026, abstract = {A set of n weighted points in general position in R(d) defines a unique regular triangulation. This paper proves that if the points are added one by one, then flipping in a topological order will succeed in constructing this triangulation. If, in addition, the points are added in a random sequence and the history of the flips is used for locating the next point, then the algorithm takes expected time at most O(n log n + n(inverted left perpendicular d/2 inverted right perpendicular)). Under the assumption that the points and weights are independently and identically distributed, the expected running time is between proportional to and a factor log n more than the expected size of the regular triangulation. The expectation is over choosing the points and over independent coin-flips performed by the algorithm.}, author = {Edelsbrunner, Herbert and Shah, Nimish}, issn = {0178-4617}, journal = {Algorithmica}, number = {3}, pages = {223 -- 241}, publisher = {Springer}, title = {{Incremental topological flipping works for regular triangulations}}, doi = {10.1007/BF01975867}, volume = {15}, year = {1996}, } @article{4027, abstract = {Questions about lines in space arise frequently as subproblems in three-dimensional computational geometry. In this paper we study a number of fundamental combinatorial and algorithmic problems involving arrangements of n lines in three-dimensional space. Our main results include: 1. A tight Θ(n2) bound on the maximum combinatorial description complexity of the set of all oriented lines that have specified orientations relative to the n given lines. 2. A similar bound of Θ(n3) for the complexity of the set of all lines passing above the n given lines. 3. A preprocessing procedure using O(n2+ε) time and storage, for any ε > 0, that builds a structure supporting O(logn)-time queries for testing if a line lies above all the given lines. 4. An algorithm that tests the "towering property" in O(n4/3+ε) time, for any ε > 0: do n given red lines lie all above n given blue lines? The tools used to obtain these and other results include Plücker coordinates for lines in space and ε-nets for various geometric range spaces.}, author = {Chazelle, Bernard and Edelsbrunner, Herbert and Guibas, Leonidas and Sharir, Micha and Stolfi, Jorge}, issn = {0178-4617}, journal = {Algorithmica}, number = {5}, pages = {428 -- 447}, publisher = {Springer}, title = {{Lines in space: Combinatorics and algorithms}}, doi = {10.1007/BF01955043}, volume = {15}, year = {1996}, } @misc{4030, author = {Liang, Jie and Edelsbrunner, Herbert and Subramaniam, Shankar}, booktitle = {Fortieth Annual Meeting}, number = {2, Part 2}, pages = {A224 -- A224}, publisher = {Cell Press}, title = {{Effects of molecular shape representations on boundary element method for protein electrostatics computations}}, doi = {10.1016/S0006-3495(96)79664-9}, volume = {70}, year = {1996}, } @misc{4031, author = {Liang, Jie and Edelsbrunner, Herbert and Pamidghantam, Sudhakar and Subramaniam, Shankar}, booktitle = {Fortieth Annual Meeting}, number = {2, Part 2}, pages = {A377 -- A377}, publisher = {Cell Press}, title = {{Analytical method for molecular shapes: Area, volume, cavities, interface and pockets}}, doi = {10.1016/S0006-3495(96)79670-4}, volume = {70}, year = {1996}, } @article{4142, abstract = {Mutations giving rise to anatomical defects in the inner ear have been isolated in a large scale screen for mutations causing visible abnormalities in the zebrafish embryo (Haffter, P., Granato, M., Brand, M. et al. (1996) Development 123, 1-36). 58 mutants have been classified as having a primary ear phenotype; these fall into several phenotypic classes, affecting presence or size of the otoliths, size and shape of the otic vesicle and formation of the semicircular canals, and define at least 20 complementation groups. Mutations in seven genes cause loss of one or both otoliths, but do not appear to affect development of other structures within the ear. Mutations in seven genes affect morphology and patterning of the inner ear epithelium, including formation of the semicircular canals and, in some, development of sensory patches (maculae and cristae). Within this class, dog-eared mutants show abnormal development of semicircular canals and lack cristae within the ear, while in van gogh, semicircular canals fail to form altogether, resulting in a tiny otic vesicle containing a single sensory patch. Both these mutants show defects in the expression of homeobox genes within the otic vesicle. In a further class of mutants, ear size is affected while patterning appears to be relatively normal; mutations in three genes cause expansion of the otic vesicle, while in little ears and microtic, the ear is abnormally small, but still contains all five sensory patches, as in the wild type. Many of the ear and otolith mutants show an expected behavioural phenotype: embryos fail to balance correctly, and may swim on their sides, upside down, or in circles. Several mutants with similar balance defects have also been isolated that have no obvious structural ear defect, but that may include mutants with vestibular dysfunction of the inner ear (Granato, M., van Eeden, F. J. M., Schach, U. et al. (1996) Development, 123, 399-413,). Mutations in 19 genes causing primary defects in other structures also show an ear defect. In particular, ear phenotypes are often found in conjunction with defects of neural crest derivatives (pigment cells and/or cartilaginous elements of the jaw). At least one mutant, dog-eared, shows defects in both the ear and another placodally derived sensory system, the lateral line, while hypersensitive mutants have additional trunk lateral line organs.}, author = {Whitfield, Tanya and Granato, Michael and Van Eeden, Fredericus and Schach, Ursula and Brand, Michael and Furutani Seiki, Makoto and Haffter, Pascal and Hammerschmidt, Matthias and Heisenberg, Carl-Philipp J and Jiang, Yunjin and Kane, Donald and Kelsh, Robert and Mullins, Mary and Odenthal, Jörg and Nüsslein Volhard, Christiane}, issn = {0950-1991}, journal = {Development}, pages = {241 -- 254}, publisher = {Company of Biologists}, title = {{Mutations affecting development of the zebrafish inner ear and lateral line}}, doi = {10.1242/dev.123.1.241}, volume = {123}, year = {1996}, }