@article{3638, abstract = {Any sample of genes traces back to a single common ancestor. Each gene also has other properties: its sequence, its geographic location and the phenotype and fitness of the organism that carries it. With sexual reproduction, different genes have different genealogies, which gives us much more information, but also greatly complicates population genetic analysis. We review the close relation between the distribution of genealogies and the classic theory of identity by descent in spatially structured populations, and develop a simple diffusion approximation to the distribution of coalescence times in a homogeneous two-dimensional habitat. This shows that when neighbourhood size is large (as in most populations) only a small fraction of pairs of genes are closely related, and only this fraction gives information about current rates of gene flow. The increase of spatial dispersion with lineage age is thus a poor estimator of gene flow. The bulk of the genealogy depends on the long-term history of the population; we discuss ways of inferring this history from the concordance between genealogies across loci.}, author = {Barton, Nicholas H and Wilson, I}, issn = {0962-8436}, journal = {Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences}, number = {1327}, pages = {49 -- 59}, publisher = {Royal Society, The}, title = {{Genealogies and geography}}, doi = {10.1098/rstb.1995.0090}, volume = {349}, year = {1995}, } @article{3639, abstract = {A general representation of multilocus selection is extended to allow recombination to depend on genotype. The equations simplify if modifier alleles have small effects on recombination. The evolution of such modifiers only depends on how they alter recombination between the selected loci, and does not involve dominance in modifier effects. The net selection on modifiers can be found explicitly if epistasis is weak relative to recombination. This analysis shows that recombination can be favoured in two ways: because it impedes the response to epistasis which fluctuates in sign, or because it facilitates the response to directional selection. The first mechanism is implausible, because epistasis must change sign over periods of a few generations: faster or slower fluctuations favour reduced recombination. The second mechanism requires weak negative epistasis between favourable alleles, which may either be increasing, or held in check by mutation. The selection (si) on recombination modifiers depends on the reduction in additive variance of log (fitness) due to linkage disequilibria (υ1 < 0), and on non-additive variance in log (fitness) (V′2, V′3,.. epistasis between 2, 3.. loci). For unlinked loci and pairwise epistasis, si = − (υ1 + 4V2/3)δr, where δr is the average increase in recombination caused by the modifier. The approximations are checked against exact calculations for three loci, and against Charlesworth's analyses of mutation/selection balance (1990), and directional selection (1993). The analysis demonstrates a general relation between selection on recombination and observable components of fitness variation, which is open to experimental test.}, author = {Barton, Nicholas H}, issn = {0016-6723}, journal = {Genetical Research}, number = {2}, pages = {123 -- 144}, publisher = {Cambridge University Press}, title = {{A general model for the evolution of recombination}}, doi = {10.1017/S0016672300033140}, volume = {65}, year = {1995}, } @article{3640, abstract = {The probability of fixation of a favorable mutation is reduced if selection at other loci causes inherited variation in fitness. A general method for calculating the fixation probability of an allele that can find itself in a variety of genetic backgrounds is applied to find the effect of substitutions, fluctuating polymorphisms, and deleterious mutations in a large population. With loose linkage, r, the effects depend on the additive genetic variance in relative fitness, var(W), and act by reducing effective population size by (N/Ne) = 1 + var(W)/2r2. However, tightly linked loci can have a substantial effect not predictable from Ne. Linked deleterious mutations reduce the fixation probability of weakly favored alleles by exp (-2U/R), where U is the total mutation rate and R is the map length in Morgans. Substitutions can cause a greater reduction: an allele with advantage s < scrit = (pi 2/6) loge (S/s) [var(W)/R] is very unlikely to be fixed. (S is the advantage of the substitution impeding fixation.) Fluctuating polymorphisms at many (n) linked loci can also have a substantial effect, reducing fixation probability by exp [square root of 2Kn var(W)/R] [K = -1/E((u-u)2/uv) depending on the frequencies (u,v) at the selected polymorphisms]. Hitchhiking due to all three kinds of selection may substantially impede adaptation that depends on weakly favored alleles.}, author = {Barton, Nicholas H}, issn = {0016-6731}, journal = {Genetics}, number = {2}, pages = {821 -- 841}, publisher = {Genetics Society of America}, title = {{Linkage and the limits to natural selection}}, doi = {http://www.genetics.org/content/140/2/821.long}, volume = {140}, year = {1995}, } @article{4028, abstract = {Efficient algorithms are described for computing topological, combinatorial, and metric properties of the union of finitely many spherical balls in R(d) These algorithms are based on a simplicial complex dual to a decomposition of the union of balls using Voronoi cells, and on short inclusion-exclusion formulas derived from this complex. The algorithms are most relevant in R(3) where unions of finitely many balls are commonly used as models of molecules.}, author = {Edelsbrunner, Herbert}, issn = {0179-5376}, journal = {Discrete & Computational Geometry}, number = {1}, pages = {415 -- 440}, publisher = {Springer}, title = {{The union of balls and its dual shape}}, doi = {10.1007/BF02574053}, volume = {13}, year = {1995}, } @article{4029, abstract = {A general and direct method for computing the Betti numbers of a finite simplicial complex in Bd is given. This method is complete for d less than or equal to 3, where versions of this method run in time O(n alpha(n)) and O(n), n the number of simplices. An implementation of the algorithm is applied to alpha shapes, which is a novel geometric modeling tool.}, author = {Delfinado, Cecil and Edelsbrunner, Herbert}, issn = {0167-8396}, journal = {Computer Aided Geometric Design}, number = {7}, pages = {771 -- 784}, publisher = {Elsevier}, title = {{An incremental algorithm for Betti numbers of simplicial complexes on the 3-sphere}}, doi = {10.1016/0167-8396(95)00016-Y}, volume = {12}, year = {1995}, } @inproceedings{4034, abstract = {Any arbitrary polyhedron P contained as a subset within Rd can be written as algebraic sum of simple terms, each an integer multiple of the intersection of d or fewer half-spaces defined by facets of P. P can be non-convex and can have holes of any kind. Among the consequences of this result are a short boolean formula for P, a fast parallel algorithm for point classification, and a new proof of the Gram-Sommerville angle relation.}, author = {Edelsbrunner, Herbert}, booktitle = {Proceedings of IEEE 36th Annual Foundations of Computer Science}, issn = {0272-5428}, location = {Milwaukee, WI, United States of America}, pages = {248 -- 257}, publisher = {IEEE}, title = {{Algebraic decomposition of non-convex polyhedra}}, year = {1995}, } @article{4035, abstract = {Let S be a set of n points in ℝd . A set W is a weak ε-net for (convex ranges of)S if, for any T⊆S containing εn points, the convex hull of T intersects W. We show the existence of weak ε-nets of size {Mathematical expression}, where β2=0, β3=1, and βd ≈0.149·2d-1(d-1)!, improving a previous bound of Alon et al. Such a net can be computed effectively. We also consider two special cases: when S is a planar point set in convex position, we prove the existence of a net of size O((1/ε) log1.6(1/ε)). In the case where S consists of the vertices of a regular polygon, we use an argument from hyperbolic geometry to exhibit an optimal net of size O(1/ε), which improves a previous bound of Capoyleas.}, author = {Chazelle, Bernard and Edelsbrunner, Herbert and Grigni, Michelangelo and Guibas, Leonidas and Sharir, Micha and Welzl, Emo}, issn = {0179-5376}, journal = {Discrete & Computational Geometry}, number = {1}, pages = {1 -- 15}, publisher = {Springer}, title = {{Improved bounds on weak ε-nets for convex sets}}, doi = {10.1007/BF02574025}, volume = {13}, year = {1995}, } @article{4153, author = {Ransom, D. and Brownlie, Alison and Haffter, Pascal and Odenthal, Jörg and Kelsh, Robert and Brand, Michael and Furutani Seiki, Makoto and Granato, Michael and Hammerschmidt, Matthias and Heisenberg, Carl-Philipp J and Jiang, Yunjin and Kane, David and Mullins, Mary and Van Eden, Fredericus and Warga, Rachel and Nüsslein Volhard, Christiane and Zon, L.}, issn = {0006-4971}, journal = {Blood}, number = {10}, pages = {1912 -- 1912}, publisher = {American Society of Hematology}, title = {{Hematopoietic mutants identified in a saturation screen of the zebrafish genome}}, volume = {86}, year = {1995}, } @article{4296, abstract = {Three replicate lines of Drosophila melanogaster were cultured at each of two temperatures (16.5⚬C and 25⚬C) in population cages for 4 yr. The lifespans of both sexes and the fecundity and fertility of the females were then measured at both experimental temperatures. The characters showed evidence of adaptation; flies of both sexes from each selection regime showed higher longevity, and females showed higher fecundity and fertility, than flies from the other selection regime when they were tested at the experimental temperature at which they had evolved. Calculation of intrinsic rates of increase under different assumptions about the rate of population increase showed that the difference between the lines from the two selection regimes became less the higher the rate of population increase, because the lines were more similar in early adulthood than they were later. Despite the increased adaptation of the low-temperature lines to the low temperature, like the high temperature lines they produced progeny at a higher rate at the higher temperature. The lines may have independently evolved adaptations to their respective thermal regimes during the experiment, or there may have been a trade-off between adaptation to the two temperatures, or mutation pressure may have lowered adaptation to the temperature that the flies no longer encountered.}, author = {Partridge, Linda and Barrie, Brian and Barton, Nicholas H and Fowler, Kevin and French, Vernon}, issn = {0014-3820}, journal = {Evolution}, number = {3}, pages = {538 -- 544}, publisher = {Wiley-Blackwell}, title = {{Rapid laboratory evolution of adult life history traits in Drosophila melanogaster in response to temperature}}, doi = {10.1111/j.1558-5646.1995.tb02285.x}, volume = {49}, year = {1995}, } @article{4297, abstract = {The F5 (2n = 34) and FM2 (2n = 44-46) chromosome races of the Sceloporus grammicus complex form a parapatric hybrid zone in the Mexican state of Hidalgo, characterized by steep concordant clines among three diagnostic chromosome markers across a straight-line distance of about 2 km. Here, we show that this zone is actually structured into local patches in which hybridization extends over an extremely irregular front. The distribution of hybrid-index (HI) scores across the transect reveals some hybridization at almost all localities mapped in a central 7 km x 3 km area. Pooling the central samples produces both a strong heterozygote deficit for all diagnostic markers and strong linkage disequilibria between all pairwise combinations of these (unlinked) markers. Moreover, a highly significant association exists between the habitat on which each individual was caught and its karyotype (F5 chromosomes are more likely to be found on oak). Analysis of genotype frequencies over a range of spatial scales shows that there is no significant heterozygote deficit or habitat association within local areas of less than about 200 m; however, there is significant linkage disequilibrium over the smallest scales (R = D (pquv)1/2 = 0.29, support limits, 0.18-0.36) over 100 m. These patterns suggest that lizards mate and choose habitats randomly within local patches. This conclusion is supported by mark-recapture estimates of dispersal (≈ 80 m in a generation) and by inference of matings from embryo and maternal karyotypes. Closer examination of the two-dimensional pattern reveals a convoluted cline for all three markers, with a width of 830 m (support limits 770 m-930 m). This cline width, combined with the strength of local linkage disequilibrium, implies a dispersal rate of σ = 160 m in a generation and an effective selection pressure of 30% on each chromosome marker. The proportion of inviable embryos is greater in females from the center of the hybrid zone; this is caused by effects associated with both karyotype and location. The hybrid zone is likely to be maintained by selection against chromosomal heterozygotes, by other kinds of selection against hybrids, and by selection adapting the chromosome races to different habitats. The structure of the contact may be caused by both random drift and by selection in relation to habitat.}, author = {Sites, Jack and Barton, Nicholas H and Reed, Kent}, issn = {0014-3820}, journal = {Evolution}, number = {1}, pages = {9 -- 36}, publisher = {Wiley-Blackwell}, title = {{The genetic structure of a mosaic hybrid zone between two chromosome races of the Sceloporus grammicus complex (Sauria, Phrynosomatidae) in central Mexico}}, doi = {10.1111/j.1558-5646.1995.tb05955.x}, volume = {49}, year = {1995}, } @article{4298, author = {Barton, Nicholas H}, issn = {1558-5646}, journal = {Evolution}, number = {6}, pages = {1038 -- 1045}, publisher = {Wiley}, title = {{Appendix to "A simulation study of multilocus clines" by S J E Baird}}, doi = {10.1111/j.1558-5646.1995.tb04431.x}, volume = {49}, year = {1995}, } @phdthesis{4428, abstract = {Hybrid systems are real-time systems that react to both discrete and continuous activities (such as analog signals, time, temperature, and speed). Typical examples of hybrid systems are embedded systems, timing-based communication protocols, and digital circuits at the transistor level. Due to the rapid development of microprocessor technology, hybrid systems directly control much of what we depend on in our daily lives. Consequently, the formal specification and verification of hybrid systems has become an active area of research. This dissertation presents the first general framework for the formal specification and verification of hybrid systems, as well as the first hybrid-system analysis tool--HyTech. The framework consists of a graphical finite-state-machine-like language for modeling hybrid systems, a temporal logic for modeling the requirements of hybrid systems, and a computer procedure that verifies modeled hybrid systems against modeled requirements. The tool HyTech is the implementation of the framework using C++ and Mathematica. More specifically, our hybrid-system modeling language, Hybrid Automata, is an extension of timed automata with discrete and continuous variables whose dynamics are governed by differential equations. Our requirement modeling language, ICTL, is a branching-time temporal logic, and is an extension of TCTL with stop-watch variables. Our verification procedure is a symbolic model-checking procedure that verifies linear hybrid automata against ICTL formulas. To make HyTech more efficient and effective, we use model-checking strategies and abstract operators that can expedite the verification process. To enable HyTech to verify nonlinear hybrid automata, we introduce two translations from nonlinear hybrid automata to linear hybrid automata. We have applied HyTech to analyze more than 30 hybrid-system benchmarks. In this dissertation, we present the application of HyTech to three nontrivial hybrid systems taken from the literature.}, author = {Ho, Pei}, pages = {1 -- 188}, publisher = {Cornell University}, title = {{Automatic analysis of hybrid systems}}, year = {1995}, } @inproceedings{4447, abstract = {This paper is addressed to potential users of HyTech, the Cornell Hybrid Technology Tool, an automatic tool for analyzing hybrid systems. We review the formal technologies that have been incorporated into HyTech, and we illustrate the use of HyTech with three nontrivial case studies.}, author = {Henzinger, Thomas A and Ho, Pei}, booktitle = {4th International Hybrid Systems Workshop}, editor = {Panos, Antsaklis and Kohn, Wolf and Nerode, Anil and Sastry, Shankar}, isbn = {9783540683346}, location = { New Brunswick, NJ, United States of America}, pages = {265 -- 293}, publisher = {Springer}, title = {{HyTech: The Cornell Hybrid Technology Tool}}, doi = {10.1007/3-540-60472-3_14}, volume = {999}, year = {1995}, } @inproceedings{4448, abstract = {We report on several abstract interpretation strategies that are designed to improve the performance of HyTech, a symbolic model checker for linear hybrid systems. We (1) simultaneously compute the target region from different directions, (2) conservatively approximate the target region by dropping constraints, and (3) iteratively refine the approximation until sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator.}, author = {Henzinger, Thomas A and Ho, Pei}, booktitle = {3rd International Hybrid Systems Workshop}, editor = {Panos, Antsaklis and Kohn, Wolf and Nerode, Anil and Sastry, Shankar}, isbn = {9783540604723}, location = {Ithaca, NY, United States of America}, pages = {252 -- 264}, publisher = {Springer}, title = {{A note on abstract-interpretation strategies for hybrid automata}}, doi = {10.1007/3-540-60472-3_13}, volume = {999}, year = {1995}, } @inproceedings{4450, abstract = {Hybrid systems model discrete programs that are embedded in continuous environments. Model-checking tools are available for the analysis of linear hybrid systems, whose continuous variables are bounded by piecewise-linear trajectories. Most embedded programs, however, operate in nonlinear environments. We present, analyze, and apply two algorithms for translating nonlinear hybrid systems into linear hybrid systems. The clock translation replaces nonlinear variables by clock variables; the rate translation approximates nonlinear variables by piecewise-linear envelopes. Both translations are sound for reachability; that is, if we establish a safety property of the translated linear system, we may conclude that the original nonlinear system satisfies the property. The clock translation is also complete for reachability; that is, the original system and the translated system satisfy the same safety properties. The two translations apply to incomparable classes of nonlinear hybrid systems. From the clock translation we obtain a new decidability result for hybrid systems. With the help of Hytech, a symbolic model checker for linear hybrid systems, we automatically verify a nonlinear railroad gate control program using the clock translation, and a nonlinear temperature control program using the rate translation.}, author = {Henzinger, Thomas A and Ho, Pei}, booktitle = {7th International Conference on Computer Aided Verification}, isbn = {9783540494133}, location = {Liege, Belgium}, pages = {225 -- 238}, publisher = {Springer}, title = {{Algorithmic analysis of nonlinear hybrid systems}}, doi = {10.1007/3-540-60045-0_53}, volume = {939}, year = {1995}, } @inproceedings{4497, abstract = {HyTech is a tool for the automated analysis of embedded systems. This document, designed for the first-time user of HyTech, guides the reader through the underlying system model, and through the input language for describing and analyzing systems. The guide gives several examples of usage, and some hints for gaining maximal computational efficiency from the tool. The version of HyTech described in this guide was released in August 1995, and is available through anonymous ftp from ftp.cs.cornell.edu in the directory pub/tah/HyTech, and through the World-Wide Web via HyTech's home page http:/www.cs.cornell.edu/Info/People/tah/hytech.html.}, author = {Henzinger, Thomas A and Ho, Pei and Wong Toi, Howard}, booktitle = {1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783540606307}, location = {Aarhus, Denmark}, pages = {41 -- 71}, publisher = {Springer}, title = {{A user guide to HyTech}}, doi = {10.1007/3-540-60630-0_3}, volume = {1019}, year = {1995}, } @inproceedings{4498, abstract = {We present algorithms for computing similarity relations of labeled graphs. Similarity relations have applications for the refinement and verification of reactive systems. For finite graphs, we present an O(mn) algorithm for computing the similarity relation of a graph with n vertices and m edges (assuming m⩾n). For effectively presented infinite graphs, we present a symbolic similarity-checking procedure that terminates if a finite similarity relation exists. We show that 2D rectangular automata, which model discrete reactive systems with continuous environments, define effectively presented infinite graphs with finite similarity relations. It follows that the refinement problem and the ∀CTL* model-checking problem are decidable for 2D rectangular automata}, author = {Henzinger, Monika H and Henzinger, Thomas A and Kopke, Peter}, booktitle = {Proceedings of IEEE 36th Annual Foundations of Computer Science}, isbn = {0818671831}, issn = {0272-5428}, location = {Milwaukee, WI, United States of America}, pages = {453 -- 462}, publisher = {IEEE}, title = {{Computing simulations on finite and infinite graphs}}, doi = {10.1109/SFCS.1995.492576}, year = {1995}, } @inproceedings{4499, abstract = {We describe a new implementation of HYTECH, a symbolic model checker for hybrid systems. Given a parametric description of an embedded system as a collection of communicating automata, HYTECH automatically computes the conditions on the parameters under which the system satisfies its safety and timing requirements. While the original HYTECH prototype was based on the symbolic algebra tool Mathematica, the new implementation is written in C++ and builds on geometric algorithms instead of formula manipulation. The new HYTECH offers a cleaner and more expressive input language, greater portability, superior performance (typically two to three orders of magnitude), and new features such as diagnostic error-trace generation. We illustrate the effectiveness of the new implementation by applying HYTECH to the automatic parametric analysis of the generic railroad crossing benchmark problem and to an active structure control algorithm}, author = {Henzinger, Thomas A and Ho, Pei and Wong Toi, Howard}, booktitle = {Proceedings 16th IEEE Real-Time Systems Symposium}, isbn = {0818673370}, location = {Pisa, Italy}, pages = {56 -- 65}, publisher = {IEEE}, title = {{HyTech: The next generation}}, doi = {10.1109/REAL.1995.495196 }, year = {1995}, } @inproceedings{4500, abstract = {We investigate the expressive power of timing restrictions on labeled transition systems. In particular, we show how constraints on clock variables together with a uniform liveness condition—the divergence of time—can express Büchi, Muller, Streett, Rabin, and weak and strong fairness conditions on a given labeled transition system. We then consider the effect, on both timed and time-abstract expressiveness, of varying the following parameters: time domain (discrete or dense), number of clocks, number of states, and size of constants used in timing restrictions.}, author = {Henzinger, Thomas A and Kopke, Peter and Wong Toi, Howard}, booktitle = {22nd International Colloquium on Automata, Languages and Programming }, isbn = {9783540600848}, location = {Szeged, Hungary}, pages = {417 -- 428}, publisher = {Springer}, title = {{The expressive power of clocks}}, doi = {10.1007/3-540-60084-1_93}, volume = {944}, year = {1995}, } @inproceedings{4502, abstract = {Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify the precise boundary between decidability and undecidability of the reachability problem for hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves the omega-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch.}, author = {Henzinger, Thomas A and Kopke, Peter and Puri, Anuj and Varaiya, P.}, booktitle = {Proceedings of the 27th annual ACM symposium on Theory of computing}, isbn = {9780897917186}, location = {Las Vegas, NV, United States of America}, pages = {373 -- 382}, publisher = {ACM}, title = {{What's decidable about hybrid automata?}}, doi = {10.1145/225058.225162}, year = {1995}, }