@article{205,
author = {Timothy Browning},
journal = {Acta Arithmetica},
number = {3},
pages = {275 -- 295},
publisher = {Instytut Matematyczny},
title = {{Counting rational points on cubic and quartic surfaces}},
doi = {10.4064/aa108-3-7},
volume = {108},
year = {2003},
}
@article{206,
abstract = {Let T ⊂ ℙ 4 be a non-singular threefold of degree at least four. Then we show that the number of points in T(ℚ), with height at most B, is o(B 3) or B → ∞.},
author = {Timothy Browning},
journal = {Quarterly Journal of Mathematics},
number = {1},
pages = {33 -- 39},
publisher = {Unknown},
title = {{A note on the distribution of rational points on threefolds}},
doi = {10.1093/qjmath/54.1.33},
volume = {54},
year = {2003},
}
@article{207,
author = {Browning, Timothy D},
journal = {Mathematical Proceedings of the Cambridge Philosophical Society},
number = {3},
pages = {385 -- 395},
publisher = {Cambridge University Press},
title = {{Sums of four biquadrates}},
doi = {10.1017/S0305004102006382},
volume = {134},
year = {2003},
}
@article{208,
abstract = {For any ε > 0 and any diagonal quadratic form Q ∈ ℤ[x 1, x 2, x 3, x 4] with a square-free discriminant of modulus Δ Q ≠ 0, we establish the uniform estimate ≪ε B 3/2+ε + B 2+ε/Δ Q 1/6 for the number of rational points of height at most B lying in the projective surface Q = 0.},
author = {Timothy Browning},
journal = {Quarterly Journal of Mathematics},
number = {1},
pages = {11 -- 31},
publisher = {Oxford University Press},
title = {{Counting rational points on diagonal quadratic surfaces}},
doi = {10.1093/qjmath/54.1.11},
volume = {54},
year = {2003},
}
@inproceedings{2337,
author = {Lieb, Élliott H and Robert Seiringer},
editor = {Karpeshina, Yulia and Weikard, Rudi and Zeng, Yanni},
pages = {239 -- 250},
publisher = {American Mathematical Society},
title = {{Bose-Einstein condensation of dilute gases in traps }},
doi = {10.1090/conm/327/05818},
volume = {327},
year = {2003},
}
@article{2354,
abstract = {We investigate the ground state properties of a gas of interacting particles confined in an external potential in three dimensions and subject to rotation around an axis of symmetry. We consider the Gross-Pitaevskii (GP) limit of a dilute gas. Analysing both the absolute and the bosonic ground states of the system, we show, in particular, their different behaviour for a certain range of parameters. This parameter range is determined by the question whether the rotational symmetry in the minimizer of the GP functional is broken or not. For the absolute ground state, we prove that in the GP limit a modified GP functional depending on density matrices correctly describes the energy and reduced density matrices, independent of symmetry breaking. For the bosonic ground state this holds true if and only if the symmetry is unbroken.},
author = {Robert Seiringer},
journal = {Journal of Physics A: Mathematical and Theoretical},
number = {37},
pages = {9755 -- 9778},
publisher = {IOP Publishing Ltd.},
title = {{Ground state asymptotics of a dilute, rotating gas}},
doi = {10.1088/0305-4470/36/37/312},
volume = {36},
year = {2003},
}
@article{2357,
abstract = {The classic Poincaré inequality bounds the L q-norm of a function f in a bounded domain Ω ⊂ ℝ n in terms of some L p-norm of its gradient in Ω. We generalize this in two ways: In the first generalization we remove a set Τ from Ω and concentrate our attention on Λ = Ω \ Τ. This new domain might not even be connected and hence no Poincaré inequality can generally hold for it, or if it does hold it might have a very bad constant. This is so even if the volume of Τ is arbitrarily small. A Poincaré inequality does hold, however, if one makes the additional assumption that f has a finite L p gradient norm on the whole of Ω, not just on Λ. The important point is that the Poincaré inequality thus obtained bounds the L q-norm of f in terms of the L p gradient norm on Λ (not Ω) plus an additional term that goes to zero as the volume of Τ goes to zero. This error term depends on Τ only through its volume. Apart from this additive error term, the constant in the inequality remains that of the 'nice' domain Ω. In the second generalization we are given a vector field A and replace ∇ by ∇ + iA(x) (geometrically, a connection on a U(1) bundle). Unlike the A = 0 case, the infimum of ∥(∇ + iA)f∥ p over all f with a given ∥f∥ q is in general not zero. This permits an improvement of the inequality by the addition of a term whose sharp value we derive. We describe some open problems that arise from these generalizations.},
author = {Lieb, Élliott H and Robert Seiringer and Yngvason, Jakob},
journal = {Annals of Mathematics},
number = {3},
pages = {1067 -- 1080},
publisher = {Princeton University Press},
title = {{Poincaré inequalities in punctured domains}},
doi = {10.4007/annals.2003.158.1067 },
volume = {158},
year = {2003},
}
@article{2358,
abstract = {A study was conducted on the one-dimensional (1D) bosons in three-dimensional (3D) traps. A rigorous analysis was carried out on the parameter regions in which various types of 1D or 3D behavior occurred in the ground state. The four parameter regions include density, transverse, longitudinal dimensions and scattering length.},
author = {Lieb, Élliott H and Robert Seiringer and Yngvason, Jakob},
journal = {Physical Review Letters},
number = {15},
pages = {1504011 -- 1504014},
publisher = {American Physical Society},
title = {{One-dimensional Bosons in three-dimensional traps}},
doi = {10.1103/PhysRevLett.91.150401},
volume = {91},
year = {2003},
}
@phdthesis{2414,
author = {Uli Wagner},
publisher = {ETH Zurich},
title = {{On k-Sets and Their Applications}},
doi = {10.3929/ethz-a-004708408},
year = {2003},
}
@inproceedings{2422,
abstract = {We prove a lower bound of 0.3288(4 n) for the rectilinear crossing number cr̄(Kn) of a complete graph on n vertices, or in other words, for the minimum number of convex quadrilaterals in any set of n points in general position in the Euclidean plane. As we see it, the main contribution of this paper is not so much the concrete numerical improvement over earlier bounds, as the novel method of proof, which is not based on bounding cr̄(Kn) for some small n.},
author = {Uli Wagner},
pages = {583 -- 588},
publisher = {SIAM},
title = {{On the rectilinear crossing number of complete graphs}},
year = {2003},
}
@inproceedings{2423,
abstract = {A finite set N ⊃ Rd is a weak ε-net for an n-point set X ⊃ Rd (with respect to convex sets) if N intersects every convex set K with |K ∩ X| ≥ εn. We give an alternative, and arguably simpler, proof of the fact, first shown by Chazelle et al. [7], that every point set X in Rd admits a weak ε-net of cardinality O(ε-d polylog(1/ε)). Moreover, for a number of special point sets (e.g., for points on the moment curve), our method gives substantially better bounds. The construction yields an algorithm to construct such weak ε-nets in time O(n ln(1/ε)). We also prove, by a different method, a near-linear upper bound for points uniformly distributed on the (d - 1)-dimensional sphere.},
author = {Matoušek, Jiří and Uli Wagner},
pages = {129 -- 135},
publisher = {ACM},
title = {{New constructions of weak epsilon-nets}},
doi = {10.1145/777792.777813},
year = {2003},
}
@inproceedings{2424,
abstract = {We introduce the adaptive neighborhood graph as a data structure for modeling a smooth manifold M embedded in some (potentially very high-dimensional) Euclidean space ℝd. We assume that M is known to us only through a finite sample P ⊂ M, as it is often the case in applications. The adaptive neighborhood graph is a geometric graph on P. Its complexity is at most min{2O(k)(n, n2}, where n = |P| and k = dim M, as opposed to the n⌈d/2⌉ complexity of the Delaunay triangulation, which is often used to model manifolds. We show that we can provably correctly infer the connectivity of M and the dimension of M from the adaptive neighborhood graph provided a certain standard sampling condition is fulfilled. The running time of the dimension detection algorithm is d2O(k7 log k) for each connected component of M. If the dimension is considered constant, this is a constant-time operation, and the adaptive neighborhood graph is of linear size. Moreover, the exponential dependence of the constants is only on the intrinsic dimension k, not on the ambient dimension d. This is of particular interest if the co-dimension is high, i.e., if k is much smaller than d, as is the case in many applications. The adaptive neighborhood graph also allows us to approximate the geodesic distances between the points in P.},
author = {Giesen, Joachim and Uli Wagner},
pages = {329 -- 337},
publisher = {ACM},
title = {{Shape dimension and intrinsic metric from samples of manifolds with high co-dimension}},
doi = {10.1145/777792.777841},
year = {2003},
}
@article{3917,
abstract = {Male dimorphism is not genetically determined, but is induced by environmental conditions particularly decreasing temperature and density.},
author = {Cremer, Sylvia and Heinze, Jürgen},
journal = {Blick in die Wissenschaft},
number = {15},
pages = {32 -- 36},
publisher = {Schnell und Steiner},
title = {{Zwischen Hochzeitsflug und Brudermord: reproduktive Taktiken bei Ameisenmännchen}},
volume = {12},
year = {2003},
}
@article{3921,
abstract = {Unlike most social insects, many Cardiocondyla ant species have two male morphs: wingless (ergatoid) males, who remain in the natal nest, and winged males who disperse but, strangely, before leaving may also mate within the nest. Whereas ergatoid males are highly intolerant of each other and fight among themselves, they tend to tolerate their winged counterparts. This is despite the fact that these winged males, like ergatoid males, represent mating competition. Why should ergatoid males tolerate their winged rivals? We developed a mathematical model to address this question. Our model focuses on a number of factors likely toinfluence whether ergatoid males are tolerant of winged males: ergatoid male–winged male relatedness, number of virgin queens, number of winged males, and the number of ejaculates a winged male has (winged males are sperm limited, whereas ergatoid males have lifelong spermatogenesis). Surprisingly, we found that increasing the number of virgin queens favors a kill strategy, whereas an increase in the other factors favors a let-live strategy; these predictions appear true for C. obscurior and for a number of other Cardiocondyla species. Two further aspects, unequal insemination success and multiple mating in queens, were also incorporated into the model and predictions made about their effects on toleration of winged males. The model is applicable more generally in species that have dimorphic males, such as some other ants, bees, and fig wasps.},
author = {Anderson, Carl and Cremer, Sylvia and Heinze, Jürgen},
journal = {Behavioral Ecology},
number = {1},
pages = {54 -- 62},
publisher = {Oxford University Press},
title = {{Live and let die: Why fighter males of the ant Cardiocondyla kill each other but tolerate their winged rivals}},
doi = {10.1093/beheco/14.1.54},
volume = {14},
year = {2003},
}
@article{3922,
abstract = {Dispersal is advantageous, but, at the same time, it implies high costs and risks. Due to these counteracting selection pressures, many species evolved dispersal polymorphisms, which, in ants, are typically restricted to the female sex (queens). Male polymorphism is presently only known from a few genera, such as Cardiocondyla, in which winged dispersing males coexist with wingless fighter males that mate exclusively inside their maternal nests. We studied the developmental mechanisms underlying these alternative male morphs and found that, first, male dimorphism is not genetically determined, but is induced by environmental conditions (decreasing temperature and density). Second, male morph is not yet fixed at the egg stage, but it differentiates during larval development. This flexible developmental pattern of male morphs allows Cardiocondyla ant colonies to react quickly to changes in their environment. Under good conditions, they invest exclusively in philopatric wingless males. But, when environmental conditions turn bad, colonies start to produce winged dispersal males, even though these males require a many times higher investment by the colony than their much smaller wingless counterparts. Cardiocondyla ants share this potential of optimal resource allocation with other colonial animals and some seed dimorphic plants.},
author = {Cremer, Sylvia and Heinze, Jürgen},
journal = {Current Biology},
number = {3},
pages = {219 -- 223},
publisher = {Cell Press},
title = {{Stress grows wings: Environmental induction of winged dispersal males in Cardiocondyla ants}},
doi = {10.1016/S0960-9822(03)00012-5},
volume = {13},
year = {2003},
}
@inbook{3991,
abstract = {We give analytic inclusion-exclusion formulas for the area and perimeter derivatives of a union of finitely many disks in the plane.},
author = {Cheng, Ho-Lun and Herbert Edelsbrunner},
booktitle = {Computer Science in Perspective: Essays Dedicated to Thomas Ottmann},
pages = {88 -- 97},
publisher = {Springer},
title = {{Area and perimeter derivatives of a union of disks}},
doi = {10.1007/3-540-36477-3_7},
volume = {2598},
year = {2003},
}
@article{3992,
abstract = {Computing the volume occupied by individual atoms in macromolecular structures has been the subject of research for several decades. This interest has grown in the recent years, because weighted volumes are widely used in implicit solvent models. Applications of the latter in molecular mechanics simulations require that the derivatives of these weighted volumes be known. In this article, we give a formula for the volume derivative of a molecule modeled as a space-filling diagram made up of balls in motion. The formula is given in terms of the weights, radii, and distances between the centers as well as the sizes of the facets of the power diagram restricted to the space-filling diagram. Special attention is given to the detection and treatment of singularities as well as discontinuities of the derivative.},
author = {Herbert Edelsbrunner and Koehl, Patrice},
journal = {PNAS},
number = {5},
pages = {2203 -- 2208},
publisher = {National Academy of Sciences},
title = {{The weighted-volume derivative of a space-filling diagram}},
doi = {10.1073/pnas.0537830100},
volume = {100},
year = {2003},
}
@article{3993,
abstract = {We present algorithms for constructing a hierarchy of increasingly coarse Morse-Smale complexes that decompose a piecewise linear 2-manifold. While these complexes are defined only in the smooth category, we extend the construction to the piecewise linearcategory by ensuring structural integrity and simulating differentiability. We then simplify Morse-Smale complexes by canceling pairs of critical points in order of increasing persistence.},
author = {Herbert Edelsbrunner and Harer, John and Zomorodian, Afra},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {87 -- 107},
publisher = {Springer},
title = {{Hierarchical Morse-Smale complexes for piecewise linear 2-manifolds}},
doi = {10.1007/s00454-003-2926-5},
volume = {30},
year = {2003},
}
@article{3994,
abstract = {The body defined by a finite collection of disks is a subset of the plane bounded by a tangent continuous curve, which we call the skin. We give analytic formulas for the area, the perimeter, the area derivative, and the perimeter derivative of the body. Given the filtrations of the Delaunay triangulation and the Voronoi diagram of the disks, all formulas can be evaluated in time proportional to the number of disks.},
author = {Cheng, Ho-Lun and Herbert Edelsbrunner},
journal = {Computational Geometry: Theory and Applications},
number = {2},
pages = {173 -- 192},
publisher = {Elsevier},
title = {{Area, perimeter and derivatives of a skin curve}},
doi = {10.1016/S0925-7721(02)00124-4},
volume = {26},
year = {2003},
}
@inproceedings{3997,
abstract = {We combine topological and geometric methods to construct a multi-resolution data structure for functions over two-dimensional domains. Starting with the Morse-Smale complex, we construct a topological hierarchy by progressively canceling critical points in pairs. Concurrently, we create a geometric hierarchy by adapting the geometry to the changes in topology. The data structure supports mesh traversal operations similarly to traditional multi-resolution representations.},
author = {Bremer, Peer-Timo and Herbert Edelsbrunner and Hamann, Bernd and Pascucci, Valerio},
pages = {139 -- 146},
publisher = {IEEE},
title = {{A multi-resolution data structure for two-dimensional Morse-Smale functions}},
doi = {10.1109/VISUAL.2003.1250365},
year = {2003},
}
@inproceedings{3999,
abstract = {We introduce relaxed scheduling as a paradigm for mesh maintenance and demonstrate its applicability to triangulating a skin surface in R-3.},
author = {Herbert Edelsbrunner and Üngör, Alper},
pages = {135 -- 151},
publisher = {Springer},
title = {{Relaxed scheduling in dynamic skin triangulation}},
doi = {10.1007/978-3-540-44400-8_14},
volume = {2866},
year = {2003},
}
@article{4254,
abstract = {Chromosomal rearrangements can promote reproductive isolation by reducing recombination along a large section of the genome. We model the effects of the genetic barrier to gene flow caused by a chromosomal rearrangement on the rate of accumulation of postzygotic isolation genes in parapatry. We find that, if reproductive isolation is produced by the accumulation in parapatry of sets of alleles compatible within but incompatible across species, chromosomal rearrangements are far more likely to favor it than classical genetic barriers without chromosomal changes. New evidence of the role of chromosomal rearrangements in parapatric speciation suggests that postzygotic isolation is often due to the accumulation of such incompatibilities. The model makes testable qualitative predictions about the genetic signature of speciation.},
author = {Navarro, Arcadio and Nicholas Barton},
journal = {Evolution; International Journal of Organic Evolution},
number = {3},
pages = {447 -- 459},
publisher = {Wiley-Blackwell},
title = {{Accumulating postzygotic isolation genes in parapatry: a new twist on chromosomal speciation}},
doi = {10.1111/j.0014-3820.2003.tb01537.x},
volume = {57},
year = {2003},
}
@article{4255,
abstract = {Humans and their closest evolutionary relatives, the chimpanzees, differ in ∼1.24% of their genomic DNA sequences. The fraction of these changes accumulated during the speciation processes that have separated the two lineages may be of special relevance in understanding the basis of their differences. We analyzed human and chimpanzee sequence data to search for the patterns of divergence and polymorphism predicted by a theoretical model of speciation. According to the model, positively selected changes should accumulate in chromosomes that present fixed structural differences, such as inversions, between the two species. Protein evolution was more than 2.2 times faster in chromosomes that had undergone structural rearrangements compared with colinear chromosomes. Also, nucleotide variability is slightly lower in rearranged chromosomes. These patterns of divergence and polymorphism may be, at least in part, the molecular footprint of speciation events in the human and chimpanzee lineages. },
author = {Navarro, Arcadio and Nicholas Barton},
journal = {Science},
number = {5617},
pages = {321 -- 324},
publisher = {American Association for the Advancement of Science},
title = {{Chromosomal speciation and molecular divergence -- Accelerated evolution in rearranged chromosomes}},
doi = {10.1126/science.1080600 },
volume = {300},
year = {2003},
}
@misc{4256,
abstract = {Artificial Life models may shed new light on the long-standing challenge for evolutionary biology of explaining the origins of complex organs. Real progress on this issue, however, requires Artificial Life researchers to take seriously the tools and insights from population genetics.},
author = {Nicholas Barton and Zuidema, Willem H},
booktitle = {Current Biology},
number = {16},
pages = {R649 -- R651},
publisher = {Cell Press},
title = {{The erratic path towards complexity}},
doi = {10.1016/S0960-9822(03)00573-6},
volume = {13},
year = {2003},
}
@article{4257,
abstract = {Variation within a species may be structured both geographically and by genetic background. We review the effects of such structuring on neutral variants, using a framework based on the coalescent process. Short-term effects of sex differences and age structure can be averaged out using fast timescale approximations, allowing a simple general treatment of effective population size and migration. We consider the effects of geographic structure on variation within and between local populations, first in general terms, and then for specific migration models. We discuss the close parallels between geographic structure and stable types of genetic structure caused by selection, including balancing selection and background selection. The effects of departures from stability, such as selective sweeps and population bottlenecks, are also described. Methods for distinguishing population history from the effects of ongoing gene flow are discussed. We relate the theoretical results to observed patterns of variation in natural populations.},
author = {Charlesworth, Brian and Charlesworth, Deborah and Nicholas Barton},
journal = {Annual Review of Ecology and Systematics},
pages = {99 -- 125},
publisher = {Annual Reviews},
title = {{The effects of genetic and geographic structure on neutral variation}},
doi = {10.1146/annurev.ecolsys.34.011802.132359},
volume = {34},
year = {2003},
}
@article{4338,
abstract = {Mosaic hybrid zones arise when ecologically differentiated taxa hybridize across a network of habitat patches. Frequent interbreeding across a small-scale patchwork can erode species differences that might have been preserved in a clinal hybrid zone. In particular, the rapid breakdown of neutral divergence sets an upper limit to the time for which differences at marker loci can persist. We present here a case study of a mosaic hybrid zone between the fire-bellied toads Bombina bombina and B. variegata (Anura: Discoglossidae) near Apahida in Romania. In our 20 × 20 km study area, we detected no evidence of a clinal transition but found a strong association between aquatic habitat and mean allele frequencies at four molecular markers. In particular, pure populations of B. bombina in ponds appear to cause massive introgression into the surrounding B. variegata gene pool found in temporary aquatic sites. Nevertheless, the genetic structure of these hybrid populations was remarkably similar to those of a previously studied transect near Pescenica (Croatia), which had both clinal and mosaic features: estimates of heterozygote deficit and linkage disequilibrium in each country are similar. In Apahida, the observed strong linkage disequilibria should stem from an imperfect habitat preference that guides most (but not all) adults into the habitats to which they are adapted. In the absence of a clinal structure, the inferred migration rate between habitats implies that associations between selected loci and neutral markers should break down rapidly. Although plausible selection strengths can maintain differentiation at those loci adapting the toads to either permanent or temporary breeding sites, the divergence at neutral markers must be transient. The hybrid zone may be approaching a state in which the gene pools are homogenized at all but the selected loci, not dissimilar from an early stage of sympatric divergence.},
author = {Vines, Timothy H and Kohler, S C and Thiel, M and Ghira, Ioan and Sands, T R and MacCallum, Catriona J and Nicholas Barton and Nürnberger, Beate},
journal = {Evolution; International Journal of Organic Evolution},
number = {8},
pages = {1876 -- 1888},
publisher = {Wiley-Blackwell},
title = {{On the maintenance of reproductive isolation in a mosaic hybrid zone between the toads Bombina bombina and B. variegata}},
doi = {10.1111/j.0014-3820.2003.tb00595.x},
volume = {57},
year = {2003},
}
@article{4348,
abstract = {Many questions in evolutionary biology are best addressed by comparing traits in different species. Often such studies involve mapping characters on phylogenetic trees. Mapping characters on trees allows the nature, number, and timing of the transformations to be identified. The parsimony method is the only method available for mapping morphological characters on phylogenies. Although the parsimony method often makes reasonable reconstructions of the history of a character, it has a number of limitations. These limitations include the inability to consider more than a single change along a branch on a tree and the uncoupling of evolutionary time from amount of character change. We extended a method described by Nielsen (2002, Syst. Biol. 51:729-739) to the mapping of morphological characters under continuous-time Markov models and demonstrate here the utility of the method for mapping characters on trees and for identifying character correlation.},
author = {Huelsenbeck, John P and Nielsen, Rasmus and Jonathan Bollback},
journal = {Systematic Biology},
number = {2},
pages = {131 -- 58},
publisher = {Oxford University Press},
title = {{Stochastic mapping of morphological characters}},
doi = {10.1080/10635150390192780},
volume = {52},
year = {2003},
}
@article{4350,
abstract = {The phylogeny of Crocodylia offers an unusual twist on the usual molecules versus morphology story. The true gharial (Gavialis gangeticus) and the false gharial (Tomistoma schlegelii), as their common names imply, have appeared in all cladistic morphological analyses as distantly related species, convergent upon a similar morphology. In contrast, all previous molecular studies have shown them to be sister taxa. We present the first phylogenetic study of Crocodylia using a nuclear gene. We cloned and sequenced the c-myc proto-oncogene from Alligator mississippiensis to facilitate primer design and then sequenced an 1,100-base pair fragment that includes both coding and noncoding regions and informative indels for one species in each extant crocodylian genus and six avian outgroups. Phylogenetic analyses using parsimony, maximum likelihood, and Bayesian inference all strongly agreed on the same tree, which is identical to the tree found in previous molecular analyses: Gavialis and Tomistoma are sister taxa and together are the sister group of Crocodylidae. Kishino-Hasegawa tests rejected the morphological tree in favor of the molecular tree. We excluded long-branch attraction and variation in base composition among taxa as explanations for this topology. To explore the causes of discrepancy between molecular and morphological estimates of crocodylian phylogeny, we examined puzzling features of the morphological data using a priori partitions of the data based on anatomical regions and investigated the effects of different coding schemes for two obvious morphological similarities of the two gharials.},
author = {Harshman, John and Huddleston, Christopher J and Jonathan Bollback and Parsons, Thomas J and Braun, Michael J},
journal = {Systematic Biology},
number = {3},
pages = {386 -- 402},
publisher = {Oxford University Press},
title = {{True and false gharials: A nuclear gene phylogeny of crocodylia}},
doi = {10.1080/10635150390197028},
volume = {52},
year = {2003},
}
@article{4460,
abstract = {Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating expressions that represent state sets. Traditionally, symbolic model-checking tools are based on back- ward state traversal; their basic operation is the function pre, which, given a set of states, returns the set of all predecessor states. This is because specifiers usually employ formalisms with future-time modalities, which are naturally evaluated by iterating applications of pre. It has been shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which, given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only parts of the state space that are reachable from an initial state and relevant for the satisfaction or violation of the specification are explored; that is, errors can be detected as soon as possible.
In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two μ-calculi. The pre-μ calculus is based on the pre operation, and the post-μ calculus is based on the post operation. These two μ-calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all ω-regular (linear-time) specifications can be expressed as post-μ queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.},
author = {Thomas Henzinger and Kupferman, Orna and Qadeer,Shaz},
journal = {Formal Methods in System Design},
number = {3},
pages = {303 -- 327},
publisher = {Springer},
title = {{From pre-historic to post-modern symbolic model checking}},
doi = {10.1023/A:1026228213080},
volume = {23},
year = {2003},
}
@inproceedings{4462,
abstract = {A major hurdle in the algorithmic verification and control of systems is the need to find suitable abstract models, which omit enough details to overcome the state-explosion problem, but retain enough details to exhibit satisfaction or controllability with respect to the specification. The paradigm of counterexample-guided abstraction refinement suggests a fully automatic way of finding suitable abstract models: one starts with a coarse abstraction, attempts to verify or control the abstract model, and if this attempt fails and the abstract counterexample does not correspond to a concrete counterexample, then one uses the spurious counterexample to guide the refinement of the abstract model. We present a counterexample-guided refinement algorithm for solving ω-regular control objectives. The main difficulty is that in control, unlike in verification, counterexamples are strategies in a game between system and controller. In the case that the controller has no choices, our scheme subsumes known counterexample-guided refinement algorithms for the verification of ω-regular specifications. Our algorithm is useful in all situations where ω-regular games need to be solved, such as supervisory control, sequential and program synthesis, and modular verification. The algorithm is fully symbolic, and therefore applicable also to infinite-state systems.},
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {886 -- 902},
publisher = {Springer},
title = {{Counterexample-guided control}},
doi = {10.1007/3-540-45061-0_69},
volume = {2719},
year = {2003},
}
@inproceedings{4463,
abstract = {We present an algorithm called TAR (“Thread-modular Abstraction Refinement”) for model checking safety properties of concurrent software. The TAR algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that TAR explores the state space of one thread at a time, making assumptions about how the environment can interfere. The TAR algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool BLAST we have implemented a fully automatic race checker for multithreaded C programs which is based on the TAR algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as ERASER or WARLOCK.},
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S and Qadeer,Shaz},
pages = {262 -- 274},
publisher = {Springer},
title = {{Thread-modular abstraction refinement}},
doi = {10.1007/978-3-540-45069-6_27},
volume = {2725},
year = {2003},
}
@inproceedings{4464,
abstract = {We introduce the paradigm of schedule-carrying code (SCC). A hard real-time program can be executed on a given platform only if there exists a feasible schedule for the real-time tasks of the program. Traditionally, a scheduler determines the existence of a feasible schedule according to some scheduling strategy. With SCC, a compiler proves the existence of a feasible schedule by generating executable code that is attached to the program and represents its schedule. An SCC executable is a real-time program that carries its schedule as code, which is produced once and can be revalidated and executed with each use. We evaluate SCC both in theory and practice. In theory, we give two scenarios, of nonpreemptive and distributed scheduling for Giotto programs, where the generation of a feasible schedule is hard, while the validation of scheduling instructions that are attached to the programs is easy. In practice, we implement SCC and show that explicit scheduling instructions can reduce the scheduling overhead up to 35% and can provide an efficient, flexible, and verifiable means for compiling Giotto programs on complex architectures, such as the TTA.},
author = {Thomas Henzinger and Kirsch, Christoph M and Matic, Slobodan},
pages = {241 -- 256},
publisher = {ACM},
title = {{Schedule-carrying code}},
doi = {10.1007/978-3-540-45212-6_16},
volume = {2855},
year = {2003},
}
@inbook{4465,
abstract = {Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots.},
author = {Thomas Henzinger and Horowitz, Benjamin and Kirsch, Christoph M},
booktitle = {Software-Enabled Control: Information Technology for Dynamical Systems},
pages = {123 -- 146},
publisher = {Wiley-Blackwell},
title = {{Embedded control systems development with Giotto}},
doi = {10.1002/047172288X.ch8},
year = {2003},
}
@inproceedings{4466,
abstract = {One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternationfree fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.},
author = {Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S},
pages = {49 -- 64},
publisher = {Springer},
title = {{On the universal and existential fragments of the mu-calculus}},
doi = {10.1007/3-540-36577-X_5},
volume = {2619},
year = {2003},
}
@inproceedings{4467,
abstract = {BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification system for checking safety properties of C programs using automatic property-driven construction and model checking of software abstractions. Blast implements an abstract-model check-refine loop to check for reachability of a specified label in the program. The abstract model is built on the fly using predicate abstraction. This model is then checked for reachability. If there is no (abstract) path to the specified error label, Blast reports that the system is safe and produces a succinct proof. Otherwise, it checks if the path is feasible using symbolic execution of the program. If the path is feasible, Blast outputs the path as an error trace, otherwise, it uses the infeasibility of the path to refine the abstract model. Blast short-circuits the loop from abstraction to verification to refinement, integrating the three steps tightly through “lazy abstraction” [5]. This integration can offer significant advantages in performance by avoiding the repetition of work from one iteration of the loop to the next. },
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S and Sutre, Grégoire},
pages = {235 -- 239},
publisher = {Springer},
title = {{Software verification with BLAST}},
doi = {10.1007/3-540-44829-2_17},
volume = {2648},
year = {2003},
}
@article{4468,
abstract = {Giotto is a high-level programming language for time-triggered control applications. The authors begin with a conceptual overview of its methodology, discuss the Giotto helicopter project, and summarize available Giotto implementations.},
author = {Thomas Henzinger and Kirsch, Christoph M and Sanvido, Marco A and Pree, Wolfgang},
journal = {IEEE Control Systems Magazine},
number = {1},
pages = {50 -- 64},
publisher = {IEEE},
title = {{From control models to real-time code using Giotto}},
doi = {10.1109/MCS.2003.1172829},
volume = {23},
year = {2003},
}
@article{4469,
abstract = {Giotto provides an abstract programmer's model for the implementation of embedded control systems with hard real-time constraints. A typical control application consists of periodic software tasks together with a mode-switching logic for enabling and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations, actuator updates, and mode switches independent of any implementation platform. Giotto can be annotated with platform constraints such as task-to-host mappings, and task and communication schedules. The annotations are directives for the Giotto compiler, but they do not alter the functionality and timing of a Giotto program. By separating the platform-independent from the platform-dependent concerns, Giotto enables a great deal of flexibility in choosing control platforms as well as a great deal of automation in the validation and synthesis of control software. The time-triggered nature of Giotto achieves timing predictability, which makes Giotto particularly suitable for safety-critical applications.},
author = {Thomas Henzinger and Horowitz, Benjamin and Kirsch, Christoph M},
journal = {Proceedings of the IEEE},
number = {1},
pages = {84 -- 99},
publisher = {IEEE},
title = {{Giotto: A time-triggered language for embedded programming}},
doi = {10.1109/JPROC.2002.805825},
volume = {91},
year = {2003},
}
@inproceedings{4561,
abstract = {We present a formalism for specifying component interfaces that expose component requirements on limited resources. The formalism permits an algorithmic check if two or more components, when put together, exceed the available resources. Moreover, the formalism can be used to compute the quantity of resources necessary for satisfying the requirements of a collection of components. The formalism can be instantiated in several ways. For example, several components may draw power from the same source. Then, the formalism supports compatibility checks such as: can two components, when put together, achieve their tasks without ever exceeding the available amount of peak power? or, can they achieve their tasks by using no more than the initially available amount of energy (i.e., power accumulated over time)? The corresponding quantitative questions that our algorithms answer are the following: what is the amount of peak power needed for two components to be put together? what is the corresponding amount of initial energy? To solve these questions, we model interfaces with resource requirements as games with quantitative objectives. The games are played on state spaces where each state is labeled by a number (representing, e.g., power consumption), and a play produces an infinite path of labels. The objective may be, for example, to minimize the largest label that occurs during a play. We illustrate our approach by modeling compatibility questions for the components of robot control software, and of wireless sensor networks.},
author = {Chakrabarti, Arindam and de Alfaro, Luca and Thomas Henzinger and Stoelinga, Mariëlle},
pages = {117 -- 133},
publisher = {ACM},
title = {{Resource interfaces}},
doi = {10.1007/978-3-540-45212-6_9},
volume = {2855},
year = {2003},
}
@inproceedings{4628,
abstract = {Discounting the future means that the value, today, of a unit payoffis 1 if the payoffo ccurs today, a if it occurs tomorrow, a 2 if it occurs the day after tomorrow, and so on, for some real-valued discount factor 0 < a < 1. Discounting (or inflation) is a key paradigm in economics and has been studied in Markov decision processes as well as game theory. We submit that discounting also has a natural place in systems engineering: for nonterminating systems, a potential bug in the far-away future is less troubling than a potential bug today. We therefore develop a systems theory with discounting. Our theory includes several basic elements: discounted versions of system properties that correspond to the ω-regular properties, fixpoint-based algorithms for checking discounted properties, and a quantitative notion of bisimilarity for capturing the difference between two states with respect to discounted properties. We present the theory in a general form that applies to probabilistic systems as well as multicomponent systems (games), but it readily specializes to classical transition systems. We show that discounting, besides its natural practical appeal, has also several mathematical benefits. First, the resulting theory is robust, in that small perturbations of a system can cause only small changes in the properties of the system. Second, the theory is computational, in that the values of discounted properties, as well as the discounted bisimilarity distance between states, can be computed to any desired degree of precision.},
author = {de Alfaro, Luca and Thomas Henzinger and Majumdar, Ritankar S},
pages = {1022 -- 1037},
publisher = {Springer},
title = {{Discounting the future in systems theory}},
doi = {10.1007/3-540-45061-0_79},
volume = {2719},
year = {2003},
}
@inproceedings{4630,
abstract = {We consider concurrent two-person games played in real time, in which the players decide both which action to play, and when to play it. Such timed games differ from untimed games in two essential ways. First, players can take each other by surprise, because actions are played with delays that cannot be anticipated by the opponent. Second, a player should not be able to win the game by preventing time from diverging. We present a model of timed games that preserves the element of surprise and accounts for time divergence in a way that treats both players symmetrically and applies to all ω-regular winning conditions. We prove that the ability to take each other by surprise adds extra power to the players. For the case that the games are specified in the style of timed automata, we provide symbolic algorithms for their solution with respect to all ω-regular winning conditions. We also show that for these timed games, memory strategies are more powerful than memoryless strategies already in the case of reachability objectives.},
author = {de Alfaro, Luca and Faella, Marco and Thomas Henzinger and Majumdar, Ritankar S and Stoelinga, Mariëlle},
pages = {144 -- 158},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The element of surprise in timed games}},
doi = {10.1007/978-3-540-45187-7_9},
volume = {2761},
year = {2003},
}
@article{576,
abstract = {We study the free expansion of a pancake-shaped Bose-condensed gas, which is initially trapped under harmonic confinement and containing a vortex at its centre. In the case of a radial expansion holding the axial confinement fixed we consider various models for the interactions, depending on the thickness of the condensate relative to the value of the scattering length. We are thus able to evaluate different scattering regimes ranging from quasi-three-dimensional (Q3D) to strictly two-dimensional (2D). We find that as the system goes from Q3D to 2D the expansion rate of the condensate increases whereas that of the vortex core decreases. In the Q3D scattering regime we also examine a fully free expansion in 3D and find oscillatory behaviour for the vortex core radius: an initial fast expansion of the vortex core is followed by a slowing down. Such a nonuniform expansion rate of the vortex core implies that the timing of its observation should be chosen appropriately.},
author = {Onur Hosten and Vignolo, Patrizia and Minguzzi, Anna and Tanatar, Bilal and Tosi, Mario P},
journal = {Journal of Physics B: Atomic, Molecular and Optical Physics},
number = {12},
pages = {2455 -- 2463},
publisher = {IOP Publishing Ltd.},
title = {{Free expansion of two-dimensional condensates with a vortex}},
doi = {10.1088/0953-4075/36/12/306},
volume = {36},
year = {2003},
}
@article{6156,
abstract = {Social and solitary feeding in natural Caenorhabditis elegans isolates are associated with two alleles of the orphan G-protein-coupled receptor (GPCR) NPR-1: social feeders contain NPR-1 215F, whereas solitary feeders contain NPR-1 215V. Here we identify FMRFamide-related neuropeptides (FaRPs) encoded by the flp-18 and flp-21 genes as NPR-1 ligands and show that these peptides can differentially activate the NPR-1 215F and NPR-1 215V receptors. Multicopy overexpression of flp-21 transformed wild social animals into solitary feeders. Conversely, a flp-21 deletion partially phenocopied the npr-1(null) phenotype, which is consistent with NPR-1 activation by FLP-21 in vivo but also implicates other ligands for NPR-1. Phylogenetic studies indicate that the dominant npr-1 215V allele likely arose from an ancestral npr-1 215F gene in C. elegans. Our data suggest a model in which solitary feeding evolved in an ancestral social strain of C. elegans by a gain-of-function mutation that modified the response of NPR-1 to FLP-18 and FLP-21 ligands.},
author = {Rogers, Candida and Reale, Vincenzina and Kim, Kyuhyung and Chatwin, Heather and Li, Chris and Evans, Peter and de Bono, Mario},
issn = {1097-6256},
journal = {Nature Neuroscience},
number = {11},
pages = {1178--1185},
publisher = {Springer Nature},
title = {{Inhibition of Caenorhabditis elegans social feeding by FMRFamide-related peptide activation of NPR-1}},
doi = {10.1038/nn1140},
volume = {6},
year = {2003},
}
@article{6157,
abstract = {In many animal species individuals aggregate to live in groups. A range of experimental approaches in different animals, including studies of social feeding in nematodes, maternal behavior in rats and sheep, and pair-bonding in voles, are providing insights into the neural bases for these behaviors. These studies are delineating multiple neural circuits and gene networks in the brain that interact in ways that are as yet poorly understood to coordinate social behavior.},
author = {de Bono, Mario},
issn = {0022-3034},
journal = {Journal of Neurobiology},
number = {1},
pages = {78--92},
publisher = {Wiley},
title = {{Molecular approaches to aggregation behavior and social attachment}},
doi = {10.1002/neu.10162},
volume = {54},
year = {2003},
}
@article{2623,
abstract = {Patients with Hodgkin's disease can develop paraneoplastic cerebellar ataxia because of the generation of autoantibodies against mGluR1 (mGluR1-Abs). Yet, the pathophysiological mechanisms underlying their motor coordination deficits remain to be elucidated. Here, we show that application of IgG purified from the patients' serum to cerebellar slices of mice acutely reduces the basal activity of Purkinje cells, whereas application to the flocculus of mice in vivo evokes acute disturbances in the performance of their compensatory eye movements. In addition, the mGluR1-Abs block induction of long-term depression in cultured mouse Purkinje cells, whereas the cerebellar motor learning behavior of the patients is affected in that they show impaired adaptation of their saccadic eye movements. Finally, postmortem analysis of the cerebellum of a paraneoplastic cerebellar ataxia patient showed that the number of Purkinje cells was significantly reduced by approximately two thirds compared with three controls. We conclude that autoantibodies against mGluR1 can cause cerebellar motor coordination deficits caused by a combination of rapid effects on both acute and plastic responses of Purkinje cells and chronic degenerative effects.},
author = {Coesmans, Michiel P and Sillevis-Smitt, Peter A and Linden, David J and Ryuichi Shigemoto and Hirano, Tomoo and Yamakawa, Yoshinori and Van Alphen, Adriaan M and Luo, Chongde and Van Der Geest, Jos N and Kros, Johan M and Gaillard, Carlo A and Frens, Maarten A and De Zeeuw, Chris I},
journal = {Annals of Neurology},
number = {3},
pages = {325 -- 336},
publisher = {Wiley-Blackwell},
title = {{Mechanisms underlying cerebellar motor deficits due to mGluR1-autoantibodies}},
doi = {10.1002/ana.10451},
volume = {53},
year = {2003},
}
@article{2625,
abstract = {Metabotropic glutamate receptor 1 (mGluR1) plays a crucial role in synaptic plasticity and motor learning in the cerebellum. We have studied activity-dependent changes in mGluR1 function in mouse cultured Purkinje neurons. Depolarizing stimulation potentiated Ca2+ and current responses to an mGluR1 agonist for several hours in the cultured Purkinje neurons. It also blocked internalization of mGluR1 and increased the number of mGluR1s on the cell membrane. We found that depolarization simultaneously increased transcription of Homer1a in Purkinje neurons. Homer1a inhibited internalization and increased cell-surface expression of mGluR1 when coexpressed in human embryonic kidney (HEK)-293 cells. Depolarization-induced Homer1a expression in Purkinje neurons was blocked by a mitogen-activated protein kinase (MAPK) inhibitor. Changes in internalization and mGluR1-mediated Ca2+ response were also blocked by inhibition of MAPK activity, suggesting that localization and activity of mGluR1 were regulated in the same signalling pathway as Homer1a expression. It is thus suggested that depolarization of the Purkinje neuron leads to the increment in mGluR1 responsiveness through MAPK activity and induction of Homer1a expression, which increases active mGluR1 on the cell surface by blocking internalization of mGluR1.},
author = {Minami, Itsunari and Kengaku, Mineko and Smitt, Sillevis P and Ryuichi Shigemoto and Hirano, Tomoo},
journal = {European Journal of Neuroscience},
number = {5},
pages = {1023 -- 1032},
publisher = {Wiley-Blackwell},
title = {{Long-term potentiation of mGluR1 activity by depolarization-induced Homer1a in mouse cerebellar Purkinje neurons}},
doi = {10.1046/j.1460-9568.2003.02499.x},
volume = {17},
year = {2003},
}
@article{2626,
abstract = {The expression pattern of metabotropic glutamate receptor Iα (mGluR1α) was immunohistochemically investigated in substantia nigra dopaminergic neurons of the macaque monkey. In normal monkeys, mGluR1α immunoreactivity was weakly observed in the dorsal tier of the substantia nigra pars compacta (SNc-d) where calbindin-D28k-containing dopaminergic neurons invulnerable to parkinsonian degeneration are specifically located. On the other hand, mGluR1α was strongly expressed in the ventral tier of the substantia nigra pars cornpacta (SNc-v). In monkeys treated with the parkinsonism-inducing drug, I-methyl-4-phenyl-1,2,3,6-tetrahydropyridine (MPTP), mGluR1α expression was decreased in dopaminergic neurons in the SNc-v that were spared its toxic action. These results suggest that mGluR1α expression may be involved at least partly in the vulnerability of dopaminergic neurons to parkinsonian insults.},
author = {Kaneda, Katsuyuki and Imanishi, Michiko and Nambu, Atsushi and Ryuichi Shigemoto and Takada, Masahiko},
journal = {Neuroreport},
number = {7},
pages = {947 -- 950},
publisher = {Lippincott, Williams & Wilkins},
title = {{Differential expression patterns of mGluR1α in monkey nigral dopamine neurons}},
doi = {10.1097/01.wnr.0000074344.81633.e4},
volume = {14},
year = {2003},
}
@article{2627,
abstract = {Despite its implications for higher order functions of the brain, little is currently known about the molecular basis of left-right asymmetry of the brain. Here we report that synaptic distribution of N-methyl-D-aspartate (NMDA) receptor GluRε2 (NR2B) subunits in the adult mouse hippocampus is asymmetrical between the left and right and between the apical and basal dendrites of single neurons. These asymmetrical allocations of ε2 subunits differentiate the properties of NMDA receptors and synaptic plasticity between the left and right hippocampus. These results provide a molecular basis for the structural and functional asymmetry of the mature brain.},
author = {Kawakami, Ryosuke and Shinohara, Yoshiaki and Kato, Yuichiro and Sugiyama, Hiroyuki and Ryuichi Shigemoto and Ito, Isao},
journal = {Science},
number = {5621},
pages = {990 -- 994},
publisher = {American Association for the Advancement of Science},
title = {{Asymmetrical allocation of NMDA receptor ε2 subunits in hippocampal circuitry}},
doi = {10.1126/science.1082609},
volume = {300},
year = {2003},
}
@article{2628,
abstract = {We aimed to estimate the number of AMPA receptors (AMPARs) bound by the quantal transmitter packet, their single-channel conductance and their density in the postsynaptic membrane at cerebellar Purkinje cell synapses. The synaptic and extrasynaptic AMPARs were examined in Purkinje cells in 2- to 4-day-old rats, when they receive synaptic inputs solely from climbing fibres (CFs). Evoked CF EPSCs and whole-cell AMPA currents displayed roughly linear current-voltage relationships, consistent with the presence of GluR2 subunits in synaptic and extrasynaptic AMPARs. The mean quantal size, estimated from the miniature EPSCs (MEPSCs), was ∼300 pS. Peak-scaled non-stationary fluctuation analysis of spontaneous EPSCs and MEPSCs gave a weighted-mean synaptic channel conductance of ∼5 pS (∼7 pS when corrected for filtering). By applying non-stationary fluctuation analysis to extrasynaptic currents activated by brief glutamate pulses (5 mM), we also obtained a small single-channel conductance estimate for extrasynaptic AMPARs (∼11 pS). This approach allowed us to obtain a maximum open probability (Po,max) value for the extrasynaptic receptors (Po,max = 0.72). Directly resolved extrasynaptic channel openings in the continued presence of glutamate exhibited clear multiple-conductance levels. The mean area of the postsynaptic density (PSD) of these synapses was 0.074 μm2, measured by reconstructing electron-microscopic (EM) serial sections. Postembedding immunogold labelling by anti-GluR2/3 antibody revealed that AMPARs are localised in PSDs. From these data and by simulating error factors, we estimate that at least 66 AMPARs are bound by a quantal transmitter packet at CF-Purkinje cell synapses, and the receptors are packed at a minimum density of ∼900 μm-2 in the postsynaptic membrane.},
author = {Momiyama, Akiko and Silver, Rachel A and Häusser, Michael A and Notomi, Takuya and Wu, Yue and Ryuichi Shigemoto and Cull-Candy, Stuart G},
journal = {Journal of Physiology},
number = {1},
pages = {75 -- 92},
publisher = {Wiley-Blackwell},
title = {{The density of AMPA receptors activated by a transmitter quantum at the climbing fibre - Purkinje cell synapse in immature rats}},
doi = {10.1113/jphysiol.2002.033472},
volume = {549},
year = {2003},
}
@article{2629,
abstract = {The release of neurotransmitters is modulated by presynaptic metabotropic glutamate receptors (mGluRs), which show a highly selective expression and subcellular location in glutamatergic terminals in the hippocampus. Using immunocytochemistry, we investigated whether one of the receptors, mGluR7, whose level of expression is governed by the postsynaptic target, was present in GABAergic terminals and whether such terminals targeted particular cells. A total of 165 interneuron dendritic profiles receiving 466 synapses (82% mGluR7a-positive) were analysed. The presynaptic active zones of most GAD-(77%) or GABA-positive (94%) synaptic boutons on interneurons innervated by mGluR7a-enriched glutamatergic terminals (mGluR7a-decorated) were immunopositive for mGluR7a. GABAergic terminals on pyramidal cells and most other interneurons in str. oriens were mGluR7a-immunonegative. The mGluR7a-decorated cells were mostly somatostatin- and mGluR1α-immunopositive neurons in str. oriens and the alveus. Their GABAergic input mainly originated from VIP-positive terminals, 90% of which expressed high levels of mGluR7a in the presynaptic active zone. Parvalbumin-positive synaptic terminals were rare on mGluR7a-decorated cells, but on these neurons 73% of them were mGluR7a-immunopositive. Some type II synapses innervating interneurons were immunopositive for mGluR7b, as were some type I synapses. Because not all target cells of VIP-positive neurons are known it has not been possible to determine whether mGluR7 is expressed in a target-cell-specific manner in the terminals of single GABAergic cells. The activation of mGluR7 may decrease GABA release to mGluR7-decorated cells at times of high pyramidal cell activity, which elevates extracellular glutamate levels. Alternatively, the presynaptic receptor may be activated by as yet unidentified endogenous ligands released by the GABAergic terminals or the postsynaptic dendrites.},
author = {Somogyi, Péter and Dalezios, Yannis and Luján, Rafael and Roberts, John D and Watanabe, Masahiko and Ryuichi Shigemoto},
journal = {European Journal of Neuroscience},
number = {12},
pages = {2503 -- 2520},
publisher = {Wiley-Blackwell},
title = {{High level of mGluR7 in the presynaptic active zones of select populations of GABAergic terminals innervating interneurons in the rat hippocampus}},
doi = {10.1046/j.1460-9568.2003.02697.x},
volume = {17},
year = {2003},
}
@article{2630,
abstract = {Taste-metabotropic glutamate receptor 4 (taste-mGluR4) and the heteromers of T1R1 and T1R3 are candidate receptors involved in the sense of umami (monosodium glutamate) taste. Although the expression of group III mGluRs (taste-mGluR4) has been demonstrated in taste tissues, no mention has been made of the expression of group I mGluRs (mGluR1 and mGluR5) in taste tissues. We examined the expression of mGluR1 and mGluR5 in rat gustatory tissues by using reverse transcription-polymerase chain reaction (RT-PCR), in situ hybridization, immunohistochemistry and immunoelectron microscopy. RT-PCR assay showed that mGluR1α and mGluR1β mRNAs were expressed in circumvallate papillae, but mGluR5 mRNA was not expressed. The positive signals of mGluR1 mRNA were detected only in circumvallate taste buds by in situ hybridization analysis. In cryosections of fungiform, foliate and circumvallate papillae, the antibody against mGluRla gave intense labeling on the taste hairs in all taste pores examined. In the developing taste buds, the positive signals of mGluR1α in taste hairs gradually increased with the increase in number of taste bud cells. These results show that, in addition to taste-mGluR4 and the heteromer of T1R1 and T1R3, mGluR1α may function as a receptor for glutamate (umami) taste sensation.},
author = {Toyono, Takashi and Seta, Yuji and Kataoka, Shinji and Kawano, Shintaro and Ryuichi Shigemoto and Toyoshima, Kuniaki},
journal = {Cell and Tissue Research},
number = {1},
pages = {29 -- 35},
publisher = {Springer},
title = {{Expression of metabotropic glutamate receptor group I in rat gustatory papillae}},
doi = {10.1007/s00441-003-0740-2},
volume = {313},
year = {2003},
}