TY - JOUR
AB - In the present paper, we give a definition of prevalent ("metrically prevalent" ) sets in nonlinear function
spaces. A subset of a Euclidean space is said to be metrically prevalent if its complement has measure zero.
There is no natural way to generalize the definition of a set of measure zero in a finite-dimensional space
to the infinite-dimensional case [6]. Therefore, it is necessary to give a special definition of a metrically
prevalent set (set of full measure) in an infinite-dimensional space. There are various ways to do so. We
suggest one of the possible ways to define the class of metrically prevalent sets in the space of smooth maps
of one smooth manifold into another. It is shown in this paper that the class of metrically prevalent sets
has natural properties; in particular, the intersection of finitely many metrically prevalent sets is metrically
prevalent. The main result of the paper is a prevalent version of Thorn's transversality theorem.
It is common practice in singularity theory and the theory of dynamical systems to say that a property
holds for "almost every" map (or flow) if it holds for a residual set, i.e., a set that contains a countable
intersection of open dense sets in the corresponding function space. However, even in finite-dimensional
spaces such a set can have arbitrarily small (say, zero) Lebesgue measure. We prove that Thorn's transversality theorem holds for an essentially "thicker" set than a residual set. It seems reasonable to revise from
the prevalent point of view the classical results of singularity theory and theory of dynamical systems,
including the multijet transversality theorem, Mather's stability theorem, Kupka-Smale's theorem for dynamical systems, etc. We shall do this elsewhere. The notion of prevalence in linear Banach spaces was
introduced and investigated in [8]. One of the possible ways to define a class of prevalent sets in the space
of smooth maps of manifolds, which essentially differs from that presented in this paper, is given in [7].
Definitions of typicalness based on the Lebesgue measure in a finite-dimensional space were suggested
by Kolmogorov [10] and Arnold [11]. These definitions were cited and discussed in [9]. Here we only point
out that the finite-dimensional analog of Arnold's definition allows prevalent sets to have arbitrarily small
measure, whereas the prevalent sets in the sense of the finite-dimensional analog of the definition given in
the present paper are necessarily of full measure. Our definition is a modification of that due to Arnold.
I wish to thank Yu. S. Illyashenko for constant attention to this work and useful discussions and
R. I. Bogdanov for help in the preparation of this paper.
AU - Kaloshin, Vadim
ID - 8528
IS - 2
JF - Functional Analysis and Its Applications
KW - Applied Mathematics
KW - Analysis
SN - 0016-2663
TI - Prevalence in the space of finitely smooth maps
VL - 31
ER -
TY - CONF
AB - A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. In this survey, we demonstrate symbolic algorithms for the verification of and controller synthesis for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Wong-Toi, Howard
ID - 4605
TI - Symbolic analysis of hybrid systems
ER -
TY - JOUR
AB - We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
ID - 4607
IS - 2
JF - Formal Methods in System Design
TI - Computing accumulated delays in real-time systems
VL - 11
ER -
TY - CONF
AB - State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.
AU - Alur, Rajeev
AU - Brayton, Robert K
AU - Thomas Henzinger
AU - Qadeer,Shaz
AU - Rajamani, Sriram K
ID - 4608
TI - Partial-order reduction in symbolic state-space exploration
VL - 1254
ER -
TY - CONF
AB - Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Kupferman, Orna
ID - 4609
TI - Alternating-time temporal logic
ER -
TY - JOUR
AB - Given a subspace X subset of or equal to R-d and a finite set S subset of or equal to R-d, we introduce the Delaunay complex, D-X, restricted by X. Its simplices are spanned by subsets T subset of or equal to S for which the common intersection of Voronoi cells meets X in a non-empty set. By the nerve theorem, boolean OR D-X and X are homotopy equivalent if all such sets are contractible. This paper proves a sufficient condition for boolean OR D-X and X be homeomorphic.
AU - Herbert Edelsbrunner
AU - Shah, Nimish R
ID - 4018
IS - 4
JF - International Journal of Computational Geometry and Applications
TI - Triangulating topological spaces
VL - 7
ER -
TY - JOUR
AB - A homeomorphism from R-2 to itself distorts metric quantities, such as distance and area. We describe an algorithm that constructs homeomorphisms with prescribed area distortion. Such homeomorphisms can be used to generate cartograms, which are geographic maps purposely distorted so their area distributions reflects a variable different from area, as for example population density. The algorithm generates the homeomorphism through a sequence of local piecewise linear homeomorphic changes. Sample results produced by the preliminary implementation of the method are included.
AU - Herbert Edelsbrunner
AU - Waupotitsch, Roman
ID - 4021
IS - 5-6
JF - Computational Geometry: Theory and Applications
TI - A combinatorial approach to cartograms
VL - 7
ER -
TY - JOUR
AB - A halving hyperplane of a set S of n points in R(d) contains d affinely independent points of S so that equally many of the points off the hyperplane lie in each of the two half-spaces. We prove bounds on the number of halving hyperplanes under the condition that the ratio of largest over smallest distance between any two points is at most delta n(1/d), delta some constant. Such a set S is called dense. In d = 2 dimensions the number of halving lines for a dense set can be as much as Omega(n log n), and it cannot exceed O (n(5/4)/log* n). The upper bound improves over the current best bound of O (n(3/2)/log* n) which holds more generally without any density assumption. In d = 3 dimensions we show that O (n(7/3)) is an upper bound on the number of halving planes for a dense set, The proof is based on a metric argument that can be extended to d greater than or equal to 4 dimensions, where it leads to O (n(d-2/d)) as an upper bound for the number of halving hyperplanes.
AU - Herbert Edelsbrunner
AU - Valtr, Pavel
AU - Welzl, Emo
ID - 4022
IS - 3
JF - Discrete & Computational Geometry
TI - Cutting dense point sets in half
VL - 17
ER -
TY - JOUR
AB - Let B be a finite pseudodisk collection in the plane. By the principle of inclusion-exclusion, the area or any other measure of the union is [GRAPHICS] We show the existence of a two-dimensional abstract simplicial complex, X subset of or equal to 2(B), so the above relation holds even if X is substituted for 2(B). In addition, X can be embedded in R(2) SO its underlying space is homotopy equivalent to int Boolean OR B, and the frontier of X is isomorphic to the nerve of the set of boundary contributions.
AU - Herbert Edelsbrunner
AU - Ramos, Edgar A
ID - 4023
IS - 3
JF - Discrete & Computational Geometry
TI - Inclusion-exclusion complexes for pseudodisk collections
VL - 17
ER -
TY - JOUR
AB - The epiphysial region of the dorsal diencephalon is the first site at which neurogenesis occurs in the roof of the zebrafish forebrain. We show that the homeobox containing gene floating head (flh) is required for neurogenesis to proceed in the epiphysis. In flh(-) embryos, the first few epiphysial neurons are generated, but beyond the 18 somite stage, neuronal production ceases. In contrast, in masterblind(-) (mbl(-)) embryos, epiphysial neurons are generated throughout the dorsal forebrain. We show that mbl is required to prevent the expression of flh in dorsal forebrain cells rostral to the epiphysis. Furthermore, epiphysial neurons are not ectopically induced in mbl(-)/flh(-) embryos, demonstrating that the epiphysial phenotype of mbl(-) embryos is mediated by ectopic Flh activity. We propose a role for Flh in linking the signaling pathways that regulate regional patterning to the signaling pathways that regulate neurogenesis.
AU - Masai, Ichiro
AU - Heisenberg, Carl-Philipp J
AU - Barth, K Anukampa
AU - Macdonald, Rachel
AU - Adamek, Sylwia
AU - Wilson, Stephen
ID - 4174
IS - 1
JF - Neuron
TI - Floating head and masterblind regulate neuronal patterning in the roof of the forebrain
VL - 18
ER -
TY - JOUR
AB - In zebrafish, as in other vertebrates, an initially singular eye held within the neural plate has to split during morphogenesis to allow the development of two separated eyes. It has been suggested that anterior progression of midline tissue within the neural plate is involved in the bilateralization of the eye held. Mutations in the recently identified silberblick (slb) gene cause an incomplete separation of the eyes. During gastrulation and early somitogenesis, the ventral midline of the central nervous system (CNS) together with the underlying axial mesendoderm is shortened and broadened in slb embryos. While in wild-type embryos the ventral CNS midline extends to the anterior limit of the neural plate at the end of gastrulation, there is a gap between the anterior tip of the ventral CNS midline and the anterior edge of the neural plate in slb. To investigate the cause for the shortening of the ventral CNS midline in slb we determined the fate of labeled ventral CNS midline cells in wild-type and slb embryos at different stages of development. In slb, anterior migration of ventral CNS midline cells is impaired, which indicates that migration of these cells is needed for elongation of the ventral CNS midline. The anterior shortening of the ventral CNS midline in slb leads to medial instead of bilateral induction of optic stalks followed by a partial fusion of the eyes at later developmental stages. The analysis of the sIb phenotype indicates that anterior migration of midline cells within the neural plate is required for proper induction and subsequent bilateralization of an initially singular eye field. These findings may therefore provide a starting point in elucidating the role of neural plate morphogenesis in positioning of the eyes. (C) 1997 Academic Press.
AU - Heisenberg, Carl-Philipp J
AU - Nüsslein Volhard, Christiane
ID - 4201
IS - 1
JF - Developmental Biology
TI - The function of silberblick in the positioning of the eye anlage in the zebrafish embryo
VL - 184
ER -
TY - CHAP
AU - Nicholas Barton
ID - 4284
T2 - Evolution on islands
TI - Natural selection and random genetic drift as causes of evolution on islands
ER -
TY - JOUR
AB - One of the oldest hypotheses for the advantage of recombination is that recombination allo rvs beneficial mutations that arise in different individuals to be placed together on the same chromosome. Unless recombination occurs, one of the beneficial alleles is doomed to extinction, slowing the rate at which adaptive mutations are incorporated within a population. We model the effects of a modifier of recombination on the fixation probability of beneficial mutations when beneficial alleles are segregating at other loci. We find that modifier alleles that increase recombination do increase the fixation probability of beneficial mutants and subsequently hitchhike along as the mutants rise in frequency. The strength of selection favoring a modifier that increases recombination is proportional to lambda(2)S delta r/r when linkage is tight and lambda(2)S(3) delta r/N when linkage is loose, where lambda is the beneficial mutation rate per genome per generation throughout a population of size N, S is the average mutant effect, r is the average recombination rate, and delta ris the amount that recombination is modified. We conclude that selection for recombination will be substantial only if there is tight linkage within the genome or if many loci are subject to directional selection as during periods of rapid evolutionary change.
AU - Otto, Sarah P
AU - Nicholas Barton
ID - 4285
IS - 2
JF - Genetics
TI - The evolution of recombination: Removing the limits to natural selection
VL - 147
ER -
TY - JOUR
AB - A local barrier to gene flow will delay the spread of an advantageous allele. Exact calculations for the deterministic case show that an allele that is favorable when rare is delayed very little even by a strong barrier; its spread is allowed by a time proportional to log((B/σ)√2S)/S, where B is the barrier strength, σ the dispersal range, and fitnesses are 1:1 + S:1 + 2S. However, when there is selection against heterozytes, such that the allele cannot increase from low frequency, a barrier can cause a much greater delay. If gene flow is reduced below a critical value, spread is entirely prevented. Stochastic simulations show that with additive selection, random drift slows down the spread of the allele, below the deterministic speed of σ√2S. The delay to the advance of an advantageous allele caused by a strong barrier can be substantially increased by random drift and increases with B/(2Sρσ2) in a one-dimensional habitat of density ρ. However, with selection against heterozygotes, drift can facilitate the spread and can free an allele that would otherwise be trapped indefinitely by a strong barrier. We discuss the implications of these results for the evolution of chromosome rearrangements.
AU - Piálek, Jaroslav
AU - Nicholas Barton
ID - 4286
IS - 2
JF - Genetics
TI - The spread of an advantageous allele across a barrier: the effects of random drift and selection against heterozygotes
VL - 145
ER -
TY - GEN
AB - We evaluate Sewall Wright's three-phase 'shifting balance' theory of evolution, examining both the theoretical issues and the relevant data from nature and the laboratory. We conclude that while phases I and II of Wright's theory (the movement of populations from one 'adaptive peak' to another via drift and selection) can occur under some conditions, genetic drift is often unnecessary for movement between peaks. Phase III of the shifting balance, in which adaptations spread from particular populations to the entire species, faces two major theoretical obstacles: (1) unlike adaptations favored by simple directional selection, adaptations whose fixation requires some genetic drift are often prevented from spreading by barriers to gene flow; and (2) it is difficult to assemble complex adaptations whose constituent parts arise via peak shifts in different demes. Our review of the data from nature shows that although there is some evidence for individual phases of the shifting balance process, there are few empirical observations explained better by Wright's three-phase mechanism than by simple mass selection. Similarly, artificial selection experiments fail to show that selection in subdivided populations produces greater response than does mass selection in large populations. The complexity of the shifting balance process and the difficulty of establishing that adaptive valleys have been crossed by genetic drift make it impossible to test Wright's claim that adaptations commonly originate by this process. In view of these problems, it seems unreasonable to consider the shifting balance process as an important explanation for the evolution of adaptations.
AU - Coyne, Jerry A
AU - Nicholas Barton
AU - Turelli, Michael
ID - 4287
IS - 3
T2 - Evolution; International Journal of Organic Evolution
TI - Perspective: A critique of Sewall Wright's shifting balance theory of evolutionight's shifting balance theory of evolution
VL - 51
ER -
TY - JOUR
AB - We measured the heterozygous effects on net fitness of a sample of 12 wild-type third chromosomes in D. melanogaster. Effects on fitness were assessed by competing the wild-type chromosomes against balancer chromosomes, to prevent the production of recombinants. The measurements were carried out in the population cage environment in which the life history had been evolving, in an undisturbed population with overlapping generations, and replicated measurements were made on each chromosome to control for confounding effects such as mutation accumulation. We found significant variation among the wild type chromosomes in their additive genetic effect on net fitness. The system provides an opportunity to obtain an accurate estimate of the distribution of heterozygous effects on net fitness, the contribution of different fitness components including male mating success, and the role of intra-chromosomal epistasis in fitness variation.
AU - Fowler, Kevin
AU - Semple, Colin
AU - Nicholas Barton
AU - Partridge, Linda
ID - 4288
IS - 1379
JF - Proceedings of the Royal Society of London Series B Biological Sciences
TI - Genetic variation for total fitness in Drosophila melanogaster
VL - 264
ER -
TY - GEN
AB - A worldwide survey of polymorphic molecular markers shows that the human population is genetically homogeneous, in close agreement with evidence from quite different genes and traits.
AU - Nicholas Barton
ID - 4289
IS - 12
T2 - Current Biology
TI - Population genetics: A new apportionment of human diversity
VL - 7
ER -
TY - GEN
AU - Nicholas Barton
ID - 4290
IS - 2
T2 - Genetical Research
TI - Natural hybridization and evolution
VL - 70
ER -
TY - GEN
AU - Nicholas Barton
ID - 4291
IS - 2
T2 - Genetical Research
TI - The ccological detective: Confronting models with data
VL - 70
ER -
TY - CHAP
AB - Natural populations differ from the simplest models in ways which can significantly affect their evolution. Real populations are rarely all of the same size; the rates of migration into and out of populations vary in space and time; some populations go extinct, and new ones are established, while all populations fluctuate in size. Furthermore, the genetic properties of real species are not like those assumed in simple models. Alleles are exposed to a wide variety of selection mutation rarely creates novel genotypes with each mutation event, generations overlap, and environments vary from place to place. Evolution in a metapopulation can be substantially different from the predictions of single-population models and, indeed, very different from the simplest models of subdivided species.
AU - Nicholas Barton
AU - Whitlock, Michael
ID - 4293
T2 - Metapopulation Biology
TI - The evolution of metapopulations
ER -