@article{2602,
abstract = {Although presynaptic localization of mGluR7 is well established, the mechanism by which the receptor may control Ca2+ channels in neurons is still unknown. We show here that cultured cerebellar granule cells express native metabotropic glutamate receptor type 7 (mGluR7) in neuritic processes, whereas transfected mGluR7 was also expressed in cell bodies. This allowed us to study the effect of the transfected receptor on somatic Ca2+ channels. In transfected neurons, mGuR7 selectively inhibited P/Q-type Ca2+ channels. The effect was mimicked by GTPγS and blocked by pertussis toxin (PTX) or a selective antibody raised against the G-protein αo subunit, indicating the involvement of a G(o)-like protein. The mGuR7 effect did not display the characteristics of a direct interaction between G-protein βγ subunits and the α1A Ca2+ channel subunit, but was abolished by quenching βγ subunits with specific intracellular peptides. Intracellular dialysis of G-protein βγ subunits did not mimic the action of mGluR7, suggesting that both G-protein βγ and αo subunits were required to mediate the effect. Inhibition of phospholipase C (PLC) blocked the inhibitory action of mGluR7, suggesting that a coincident activation of PLC by the G-protein βγ with αo subunits was required. The Ca2+ chelator BAPTA, as well as inhibition of either the inositol trisphosphate (IP3) receptor or protein kinase C (PKC) abolished the mGluR7 effect. Moreover, activation of native mGluR7 induced a PTX-dependent IP3 formation. These results indicated that IP3-mediated intracellular Ca2+ release was required for PKC-dependent inhibition of the Ca2+ channels. Possible control of synaptic transmission by the present mechanisms is discussed.},
author = {Perroy, Julie and Prezèau, Laurent and De Waard, Michel and Ryuichi Shigemoto and Bockaërt, Joël L and Fagni, Laurent},
journal = {Journal of Neuroscience},
number = {21},
pages = {7896 -- 7904},
publisher = {Society for Neuroscience},
title = {{Selective blockade of P/Q-type calcium channels by the metabotropic glutamate receptor type 7 involves a phospholipase C pathway in neurons}},
volume = {20},
year = {2000},
}
@article{2603,
abstract = {Aggregation of neurotransmitter receptors at pre- and postsynaptic structures is crucial for efficient neuronal communication. In contrast to the wealth of information about postsynaptic specializations, little is known about the molecular organization of presynaptic membrane proteins. We show here that the metabotropic glutamate receptor mGluR7a, which localizes specifically to presynaptic active zones, interacts in vitro and in vivo with PICK1. Coexpression in heterologous systems induces coclustering dependent upon the extreme C terminus of mGluR7a and the PDZ domain of PICK1. mGluR7a and PICK1 localize to excitatory synapses in hippocampal neurons. Furthermore, whereas transfected mGluR7a clusters at presynaptic sites, mGluR7aΔ3 lacking the PICK1 binding site targets to axons but does not cluster. These results suggest that PICK1 is a component of the presynaptic machinery involved in mGlUR7a aggregation and in modulation of glutamate neurotransmission.},
author = {Boudin, Hélène and Doan, Andrew and Xia, Jun and Ryuichi Shigemoto and Huganir, Richard L and Worley, Paul F and Craig, Ann M},
journal = {Neuron},
number = {2},
pages = {485 -- 497},
publisher = {Elsevier},
title = {{Presynaptic clustering of mGluR7a requires the PICK1 PDZ domain binding site}},
doi = {10.1016/S0896-6273(00)00127-6},
volume = {28},
year = {2000},
}
@inproceedings{2710,
author = {László Erdös},
pages = {111 -- 119},
publisher = {American Mathematical Society},
title = {{The kernel of Dirac operators on S3 and R3}},
volume = {16},
year = {2000},
}
@article{2731,
abstract = {We study the time evolution of a quantum particle in a Gaussian random environment. We show that in the weak coupling limit the Wigner distribution of the wave function converges to a solution of a linear Boltzmann equation globally in time. The Boltzmann collision kernel is given by the Born approximation of the quantum differential scattering cross section.},
author = {László Erdös and Yau, Horng-Tzer},
journal = {Communications on Pure and Applied Mathematics},
number = {6},
pages = {667 -- 735},
publisher = {Wiley-Blackwell},
title = {{Linear Boltzmann equation as the weak coupling limit of a random Schrödinger equation}},
doi = {10.1002/(SICI)1097-0312(200006)53:6<667::AID-CPA1>3.0.CO;2-5},
volume = {53},
year = {2000},
}
@article{2732,
abstract = {We consider a quantum particle moving in a harmonic exterior potential and linearly coupled to a heat bath of quantum oscillators. Caldeira and Leggett derived the Fokker Planck equation with friction for the Wigner distribution of the particle in the large-temperature limit: however, their (nonrigorous) derivation was not free of criticism, especially since the limiting equation is not of Lindblad form. In this paper we recover the correct form of their result in a rigorous way. We also point out that the source of the diffusion is physically restrictive under this scaling. We investigate the model at a fixed temperature and in the large-time limit, where the origin of the diffusion is a cumulative effect of many resonant collisions. We obtain a heat equation with a friction term for the radial process in phase space and we prove the Einstein relation in this case.},
author = {Castella, François and László Erdös and Frommlet, Florian and Markowich, Peter A},
journal = {Journal of Statistical Physics},
number = {3-4},
pages = {543 -- 601},
publisher = {Springer},
title = {{Fokker-Planck equations as scaling limits of reversible quantum systems}},
doi = {10.1023/A:1018667323830},
volume = {100},
year = {2000},
}
@article{2733,
abstract = {The Li-Yau semiclassical lower bound for the sum of the first N eigenvalues of the Dirichlet–Laplacian is extended to Dirichlet–Laplacians with constant magnetic fields. Our method involves a new diamagnetic inequality for constant magnetic fields.},
author = {László Erdös and Loss, Michael and Vougalter, Vitali},
journal = {Annales de l'Institut Fourier},
number = {3},
pages = {891 -- 907},
publisher = {Association des Annales de l'Institut Fourier},
title = {{Diamagnetic behavior of sums Dirichlet eigenvalues}},
doi = {10.5802/aif.1777},
volume = {50},
year = {2000},
}
@article{842,
author = {Wolf, Yuri I and Fyodor Kondrashov and Koonin, Eugene V},
journal = {Trends in Genetics},
number = {8},
pages = {333 -- 334},
publisher = {Elsevier},
title = {{No footprints of primordial introns in a eukaryotic genome}},
doi = {10.1016/S0168-9525(00)02059-X},
volume = {16},
year = {2000},
}
@article{8525,
abstract = {Let M be a smooth compact manifold of dimension at least 2 and Diffr(M) be the space of C r smooth diffeomorphisms of M. Associate to each diffeomorphism f;isin; Diffr(M) the sequence P n (f) of the number of isolated periodic points for f of period n. In this paper we exhibit an open set N in the space of diffeomorphisms Diffr(M) such for a Baire generic diffeomorphism f∈N the number of periodic points P n f grows with a period n faster than any following sequence of numbers {a n } n ∈ Z + along a subsequence, i.e. P n (f)>a ni for some n i →∞ with i→∞. In the cases of surface diffeomorphisms, i.e. dim M≡2, an open set N with a supergrowth of the number of periodic points is a Newhouse domain. A proof of the man result is based on the Gontchenko–Shilnikov–Turaev Theorem [GST]. A complete proof of that theorem is also presented.},
author = {Kaloshin, Vadim},
issn = {0010-3616},
journal = {Communications in Mathematical Physics},
keywords = {Mathematical Physics, Statistical and Nonlinear Physics},
pages = {253--271},
publisher = {Springer Nature},
title = {{Generic diffeomorphisms with superexponential growth of number of periodic orbits}},
doi = {10.1007/s002200050811},
volume = {211},
year = {2000},
}
@inproceedings{1736,
abstract = {A coding scheme called diode is compared with duobinary signalling and with normal binary transmission. It is shown that the diode coding suppresses the FWM products of a three channel DWDM system and this reduction against that achieved with duobinary coding is presented. The results presented show how the average level of the FWM products relative to the average levels of the three optical carriers vary over the channel spacing range. The suppression observed is about / dB more than that achieved with duobinary modulation and is greater for narrow channel spacing.},
author = {Georgios Katsaros and Lane, Phil M and Murphy, Michelle M},
pages = {27 -- 28},
publisher = {IEEE},
title = {{Comparison of the impact of FWM on binary, duobinary and dicode modulation in DWDM systems}},
doi = {10.1109/LEOS.2000.890656},
volume = {1},
year = {2000},
}
@article{1957,
abstract = {NADH:ubiquinone oxidoreductase (complex I) is the first and largest enzyme of the mitochondrial respiratory chain. The low-resolution structure of the complex is known from electron microscopy studies. The general shape of the complex is in the form of an L, with one arm in the membrane and the other peripheral. We have purified complex I from beef heart mitochondria and reconstituted the enzyme into lipid bilayers. Under different conditions, several two-dimensional crystal forms were obtained. Crystals belonging to space groups p2221 and c12 (unit cell 488 Å x 79 Å) were obtained at 22°C and contained only the membrane fragment of complex I similar to hydrophobic subcomplex Iβ but lacking the ND5 subunit. A crystal form with larger unit cell (534 Å x 81 Å, space group c12) produced at 4°C contained both the peripheral and membrane arms of the enzyme, except that ND5 was missing. Projection maps from frozen hydrated samples were calculated for all crystal forms. By comparing two different c12 crystal forms, extra electron density in the projection map of large crystal form was assigned to the peripheral arm of the enzyme. One of the features of the map is a deep, channel-like, cleft next to peripheral arm. Comparison with available structures of the intact enzyme indicates that large hydrophobic subunit ND5 is situated at the distal end of the membrane domain. Possible locations of sub-unit ND4 and of other subunits in the membrane domain are proposed. Implications of our findings for the mechanism of proton pumping by complex I are discussed. (C) 2000 Academic Press.},
author = {Leonid Sazanov and Walker, John E},
journal = {Journal of Molecular Biology},
number = {2},
pages = {455 -- 464},
publisher = {Elsevier},
title = {{Cryo-electron crystallography of two sub-complexes of bovine complex I reveals the relationship between the membrane and peripheral arms}},
doi = {10.1006/jmbi.2000.4079},
volume = {302},
year = {2000},
}
@article{1958,
abstract = {
Complex I (NADH:ubiquinone oxidoreductase) purified from bovine heart mitochondria was treated with the detergent N,N-dimethyldodecylamine N-oxide (LDAO). The enzyme dissociated into two known subcomplexes, Iα and Iβ, containing mostly hydrophilic and hydrophobic subunits, and a previously undetected fragment referred to as Iγ. Subcomplex Iγ contains the hydrophobic subunits ND1, ND2, ND3, and ND4L which are encoded in the mitochondrial genome, and the nuclear-encoded subunit KFYL. During size- exclusion chromatography in the presence of LDAO, subcomplex Iα lost several subunits and formed another characterized subcomplex known as Iλ. Similarly, subcomplex Iβ dissociated into two smaller subcomplexes, one of which contains the hydrophobic subunits ND4 and ND5; subcomplex Iγ released a fragment containing ND1 and ND2. These results suggest that in the intact complex subunits ND1 and ND2 are likely to be in a different region of the membrane domain than subunits ND4 and ND5. The compositions of the various subcomplexes and fragments of complex I provide an organization of the subunits of the enzyme in the framework of the known low resolution structure of the enzyme.},
author = {Leonid Sazanov and Peak-Chew, Sew Y and Fearnley, Ian M and Walker, John E},
journal = {Biochemistry},
number = {24},
pages = {7229 -- 7235},
publisher = {ACS},
title = {{Resolution of the membrane domain of bovine complex I into subcomplexes: implications for the structural organization of the enzyme}},
doi = {10.1021/bi000335t},
volume = {39},
year = {2000},
}
@inproceedings{4627,
abstract = {We consider two-player games, which are played on a finite state space for an infinite number of rounds. The games are concurrent, that is, in each round, the two players choose their moves independently and simultaneously; the current state and the two moves determine a successor state. We consider omega-regular winning conditions on the resulting infinite state sequence. To model the independent choice of moves, both players are allowed to use randomization for selecting their moves. This gives rise to the following qualitative modes of winning, which can be studied without numerical considerations concerning probabilities: sure-win (player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure winning with probability 1), limit-win (player 1 can ensure winning with probability arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability bounded away from 0), positive-win (player 1 can ensure winning with positive probability), and exist-win (player 1 can ensure that at least one possible outcome of the game satisfies the winning condition).We provide algorithms for computing the sets of winning states for each of these winning modes. In particular, we solve concurrent Rabin-chain games in n0 (m) time, where n is the size of the game structure and m is the number of pairs in the Rabin-chain condition. While this complexity is in line with traditional turn-based games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games are. This is because concurrent games violate two of the most fundamental properties of turn-based games. First, concurrent games are not determined, but rather exhibit a more general duality property, which involves multiple modes of winning. Second, winning strategies for concurrent games may require infinite memory.},
author = {de Alfaro, Luca and Thomas Henzinger},
pages = {141 -- 154},
publisher = {IEEE},
title = {{Concurrent omega-regular games}},
doi = {10.1109/LICS.2000.855763},
year = {2000},
}
@inproceedings{4637,
abstract = {In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their effects on the control problem.
A static type enforces fixed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process and control objective, there may be a controller of a static type, or only a controller of a syntactically compatible dynamic type, or only a controller of a semantically compatible dynamic type. We show this to be a strict hierarchy of possibilities, and we present algorithms and determine the complexity of the corresponding control problems.
Furthermore, we consider versions of the control problem in which the type of the controller (static or dynamic) is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions},
author = {de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {458 -- 473},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The control of synchronous systems}},
doi = {10.1007/3-540-44618-4_33},
volume = {1877},
year = {2000},
}
@inproceedings{4638,
abstract = {Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs; for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated.
The key observation is that “unpreventability” is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of “unpreventability,” including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol.},
author = {de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {186 -- 201},
publisher = {Springer},
title = {{Detecting errors before reaching them}},
doi = {10.1007/10722167_17},
volume = {1855},
year = {2000},
}
@article{1455,
abstract = {First, a special case of Knaster's problem is proved implying that each symmetric convex body in ℝ3 admits an inscribed cube. It is deduced from a theorem in equivariant topology, which says that there is no S4 - equivariant map from SO(3) to S2, where S4 acts on SO(3) on the right as the rotation group of the cube, and on S2 on the right as the symmetry group of the regular tetrahedron. Some generalizations are also given. Second, it is shown how the above non-existence theorem yields Makeev's conjecture in ℝ3 that each set in ℝ3 of diameter 1 can be covered by a rhombic dodecahedron, which has distance 1 between its opposite faces. This reveals an unexpected connection between inscribing cubes into symmetric bodies and covering sets by rhombic dodecahedra. Finally, a possible application of our second theorem to the Borsuk problem in ℝ3 is pointed out.},
author = {Tamas Hausel and Makai, Endre and Szücs, András},
journal = {Mathematika},
number = {1-2},
pages = {371 -- 397},
publisher = {University College London},
title = {{Inscribing cubes and covering by rhombic dodecahedra via equivariant topology}},
doi = {10.1112/S0025579300015965},
volume = {47},
year = {2000},
}
@article{3798,
abstract = {Glutamate is the main excitatory transmitter in the mammalian CNS, mediating fast synaptic transmission primarily by activation of AMPA-type glutamate receptor channels. Both synaptic structure and a cell-specific molecular switch in the AMPA receptor subunit expression are involved in the regulation of the synaptic signaling time course.},
author = {Peter Jonas},
journal = {Physiology},
number = {2},
pages = {83 -- 89},
publisher = {American Physiological Society},
title = {{The time course of signaling at central glutamatergic synapses}},
volume = {15},
year = {2000},
}
@article{3923,
author = {Cremer, Sylvia},
journal = {B.I.F. Futura},
number = {1},
pages = {68 -- 71},
publisher = {Hippokrates},
title = {{Paternity analysis with AFLPs in Cardiocondyla ants}},
volume = {15},
year = {2000},
}
@article{4004,
abstract = {In this paper we introduce the abacus model of a simplex and use it to subdivide a d-simplex into k(d) d-simplices all of the same volume and shape characteristics. The construction is an extension of the subdivision method of Freudenthal [3] and has been used by Goodman and Peters [4] to design smooth manifolds.},
author = {Herbert Edelsbrunner and Grayson, Daniel R},
journal = {Discrete & Computational Geometry},
number = {4},
pages = {707 -- 719},
publisher = {Springer},
title = {{Edgewise subdivision of a simplex}},
doi = {10.1007/s004540010063},
volume = {24},
year = {2000},
}
@inproceedings{4008,
abstract = {We formalize a notion of topological simplification within the framework of a filtration, which is the history of a growing complex. We classify a topological change that happens during growth as either a feature or noise depending on its life-time or persistence within the filtration. We give fast algorithms for computing persistence and experimental evidence for their speed and utility.},
author = {Herbert Edelsbrunner and Letscher, David and Zomorodian, Afra},
pages = {454 -- 463},
publisher = {IEEE},
title = {{Topological persistance and simplification}},
doi = {10.1109/SFCS.2000.892133},
year = {2000},
}
@article{4009,
abstract = {We study the maintenance of a simplicial grid or complex under changing density requirements. The proposed method works in any fixed dimension and generates grids by projecting cross-sections of a monotone simplicial complex that lives in one dimension higher than the grid. The density of the grid is adapted by locally moving the cross-section up or down along the extra dimension.},
author = {Herbert Edelsbrunner and Waupotitsch, Roman},
journal = {International Journal of Computational Geometry and Applications},
number = {3},
pages = {267 -- 284},
publisher = {World Scientific Publishing},
title = {{Adaptive simplicial grids from cross-sections of monotone complexes}},
doi = {10.1142/S0218195900000164},
volume = {10},
year = {2000},
}
@article{4010,
abstract = {A sliver is a tetrahedron whose four vertices lie close to a plane and whose orthogonal projection to that plane is a convex quadrilateral with no short edge. Slivers are notoriously common in 3-dimensional Delaunay triangulations even for well-spaced point sets. We show that, if the Delaunay triangulation has the ratio property introduced in Miller et al. [1995], then there is an assignment of weights so the weighted Delaunay triangulation contains no slivers. We also give an algorithm to compute such a weight assignment.},
author = {Cheng, Siu Wing and Dey, Tamal K and Herbert Edelsbrunner and Facello, Michael A and Teng, Shang Hua},
journal = {Journal of the ACM},
number = {5},
pages = {883 -- 904},
publisher = {ACM},
title = {{Sliver exudation}},
doi = {10.1145/355483.355487},
volume = {47},
year = {2000},
}
@article{4147,
abstract = {We have developed a protocol to perform a genetic screen for zygotic mutations affecting embryogenesis on the protochordate Ciona intestinalis. The choice of this taxon, whose phylogenetic position places it at the basis of the chordates as one the most primitive vertebrate relatives, could allow to address several evolutionary questions. The protochordates share many morphological features with the vertebrates, in primis the presence of a notochord. Ciona intestinalis shows several ideal features for a mutational analysis, such as external development and larvae made of a limited number of cells and cell types. Detailed cell lineage studies are available. The haploid genome size is comparable to the size of the Drosophila haploid genome. We have optimised conditions for chemical mutagenesis studying the efficiency at which different concentration of N-ethyl-N-nitrosourea (ENU) can induce mutations. Because the adult Ciona are hermaphrodites, we are performing a one-generation screen. The induced mutations are identified by visual inspection of developmental stages. We report the preliminary results from our screen including examples of the different classes of mutant phenotypes found so far.},
author = {Sordino, Paolo and Heisenberg, Carl-Philipp J and Cirino, Paola and Toscano, Alfonso and Giuliano, Paola and Marino, Rita and Pinto, Maria and De Santis, Rosaria},
journal = {Sarsia},
number = {2},
pages = {173 -- 176},
publisher = {Taylor & Francis},
title = {{A mutational approach to the study of development of the protochordate Ciona intestinalis (Tunicata, Chordata)}},
volume = {85},
year = {2000},
}
@article{4197,
abstract = {Vertebrate gastrulation involves the specification and coordinated movement of large populations of cells that give rise to the ectodermal, mesodermal and endodermal germ layers. Although many of the genes involved in the specification of cell identity during this process have been identified, little is known of the genes that coordinate cell movement. Here we show that the zebrafish silberblick (slb) locus(1) encodes Wnt11 and that Slb/Wnt11 activity is required for cells to undergo correct convergent extension movements during gastrulation. In the absence of Slb/Wnt11 function, abnormal extension of axial tissue results in cyclopia and other midline defects in the head(2). The requirement for Slb/Wnt11 is cell non-autonomous, and our results indicate that the correct extension of axial tissue is at least partly dependent on medio-lateral cell intercalation in paraxial tissue. We also show that the slb phenotype is rescued by a truncated form of Dishevelled that does not signal through the canonical Wnt pathway(3), suggesting that, as in flies(4), Wnt signalling might mediate morphogenetic events through a divergent signal transduction cascade. Our results provide genetic and experimental evidence that Wnt activity in lateral tissues has a crucial role in driving the convergent extension movements underlying vertebrate gastrulation.},
author = {Heisenberg, Carl-Philipp J and Tada, Masazumi and Rauch, Gerd and Saúde, Leonor and Concha, Miguel and Geisler, Robert and Stemple, Derek and Smith, James and Wilson, Stephen},
journal = {Nature},
number = {6782},
pages = {76 -- 81},
publisher = {Nature Publishing Group},
title = {{Silberblick/Wnt11 mediates convergent extension movements during zebrafish gastrulation}},
doi = {10.1038/35011068},
volume = {405},
year = {2000},
}
@misc{4268,
abstract = {In yeast, a modified protein known as a prion generates variation in growth rate across diverse environments. Is this an example of an agent that has evolved in order to promote its possessor's adaptability?},
author = {Partridge, Linda and Nicholas Barton},
booktitle = {Nature},
number = {6803},
pages = {457 -- 458},
publisher = {Nature Publishing Group},
title = {{Evolving evolvability}},
doi = {10.1038/35035173},
volume = {407},
year = {2000},
}
@article{4269,
author = {Coyne, Jerry A and Nicholas Barton and Turelli, Michael},
journal = {Evolution; International Journal of Organic Evolution},
number = {1},
pages = {306 -- 317},
publisher = {Wiley-Blackwell},
title = {{Is Wright’s shifting balance process important in evolution?}},
doi = {310.1111/j.0014-3820.2000.tb00033.x},
volume = {54},
year = {2000},
}
@article{4270,
abstract = {A coalescence-based maximum-likelihood method is presented that aims to (i) detect diversity-reducing events in the recent history of a population and (ii) distinguish between demographic (e.g., bottlenecks) and selective causes (selective sweep) of a recent reduction of genetic variability. The former goal is achieved by taking account of the distortion in the shape of gene genealogies generated by diversity-reducing events: gene trees tend to be more star-like than under the standard coalescent. The latter issue is addressed by comparing patterns between loci: demographic events apply to the whole genome whereas selective events affect distinct regions of the genome to a varying extent. The maximum-likelihood approach allows one to estimate the time and strength of diversity-reducing events and to choose among competing hypotheses. An application to sequence data from an African population of Drosophila melanogaster shows that the bottleneck hypothesis is unlikely and that one or several selective sweeps probably occurred in the recent history of this population.},
author = {Galtier, Nicolas and Depaulis, Frantz and Nicholas Barton},
journal = {Genetics},
number = {2},
pages = {981 -- 987},
publisher = {Genetics Society of America},
title = {{Detecting bottlenecks and selective sweeps from DNA sequence polymorphism}},
volume = {155},
year = {2000},
}
@article{4271,
abstract = {Within hybrid zones that are maintained by a balance between selection and dispersal, linkage disequilibrium is generated by the mixing of divergent populations. This linkage disequilibrium causes selection on each locus to act on all other loci, thereby steepening dines, and generating a barrier to gene flow. Diffusion models predict simple relations between the strength of linkage disequilibrium and the dispersal rate, σ, and between the barrier to gene flow, B, and the reduction in mean fitness, W̄. The aim of this paper is to test the accuracy of these predictions by comparison with an exact deterministic model of unlinked loci (r = 0.5). Disruptive selection acts on the proportion of alleles from the parental populations (p, q): W = exp[-S(4pq)(β)], such that the least fit genotype has fitness e(-S). Where β << 1, fitness is reduced for a wide range of intermediate genotypes; where β >> 1, fitness is only reduced for those genotypes close to p = 0.5. Even with strong epistasis, linkage disequilibria are close to σ2p'(i)p'(j)/r(ij), where p'(i), p'(j) are the gradients in allele frequency at loci i, j. The barrier to gene flow, which is reflected in the steepening of neutral dines, is given by B = ∫(-∞)(∞) (W̄(1/r̄)-1) dx, where r̄, the harmonic mean recombination rate between the neural and selected loci, is here 0.5. This is a close approximation for weak selection, but underestimates B for strong selection. The barrier is stronger for small β, because hybrid fitness is then reduced over a wider range of p. The widths of the selected dines are harder to predict: though simple approximations are accurate for β = 1, they become inaccurate for extreme β because, then, fitness changes sharply with p. Estimates of gene number, made from neutral dines on the assumption that selection acts against heterozygotes, are accurate for weak selection when β = 1; however, for strong selection, gene number is overestimated. For β > 1, gene number is systematically overestimated and, conversely, when β < 1, it is underestimated.
},
author = {Nicholas Barton and Shpak, Max},
journal = {Genetical Research},
number = {2},
pages = {179 -- 198},
publisher = {Cambridge University Press},
title = {{The effects of epistasis on the structure of hybrid zones}},
doi = {10.1017/S0016672399004334},
volume = {75},
year = {2000},
}
@article{4272,
abstract = {Analysis of multilocus evolution is usually intractable for more than n ~ 10 genes, because the frequencies of very large numbers of genotypes must be followed. An exact analysis of up to n ~ 100 loci is feasible for a symmetrical model, in which a set of unlinked loci segregate for two alleles (labeled '0' and '1') with interchangeable effects on fitness. All haploid genotypes with the same number of 1 alleles can then remain equally frequent. However, such a symmetrical solution may be unstable: for example, under stabilizing selection, populations tend to fix any one genotype which approaches the optimum. Here, we show how the 2' x 2' stability matrix can be decomposed into a set of matrices, each no larger than n x n. This allows the stability of symmetrical solutions to be determined. We apply the method to stabilizing and disruptive selection in a single deme and to selection against heterozygotes in a linear cline. (C) 2000 Academic Press.},
author = {Nicholas Barton and Shpak, Max},
journal = {Theoretical Population Biology},
number = {3},
pages = {249 -- 263},
publisher = {Academic Press},
title = {{The stability of symmetrical solutions to polygenic models}},
doi = {10.1006/tpbi.2000.1455},
volume = {57},
year = {2000},
}
@article{4273,
abstract = {We review the various factors that limit adaptation by natural selection. Recent discussion of constraints on selection and, conversely, of the factors that enhance 'evolvability', have concentrated on the kinds of variation that can be produced. Here, we emphasise that adaptation depends on how the various evolutionary processes shape variation in populations. We survey the limits that population genetics places on adaptive evolution, and discuss the relationship between disparate literatures. BioEssays 22:1075-1084, 2000. (C) 2000 John Wiley and Sons, Inc.},
author = {Nicholas Barton and Partridge, Linda},
journal = {Bioessays : News and Reviews in Molecular, Cellular and Developmental Biology},
number = {12},
pages = {1075 -- 1084},
publisher = {Wiley-Blackwell},
title = {{Limits to natural selection}},
doi = {10.1002/1521-1878(200012)22:12<1075::AID-BIES5>3.0.CO;2-M},
volume = {22},
year = {2000},
}
@article{4274,
abstract = {Selection on one or more genes inevitably perturbs other genes, even when those genes have no direct effect on fitness. This article reviews the theory of such genetic hitchhiking, concentrating on effects on neutral loci. Maynard Smith and Haigh introduced the classical case where the perturbation is due to a single favourable mutation. This is contrasted with the apparently distinct effects of inherited variation in fitness due to loosely linked loci. A model of fluctuating selection is analysed which bridges these alternative treatments. When alleles sweep between extreme frequencies at a rate λ, the rate of drift is increased by a factor (1 + E[1/pq]λ/(2(2λ + r))), where the recombination rate r is much smaller than the strength of selection. In spatially structured populations, the effects of any one substitution are weaker, and only cause a local increase in the frequency of a neutral allele. This increase depends primarily on the rate of recombination relative to selection (r/s), and more weakly, on the neighbourhood size, Nb = 4πρσ2. Spatial subdivision may allow local selective sweeps to occur more frequently than is indicated by the overall rate of molecular evolution. However, it seems unlikely that such sweeps can be sufficiently frequent to increase significantly the drift of neutral alleles.},
author = {Nicholas Barton},
journal = {Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences},
number = {1403},
pages = {1553 -- 1562},
publisher = {Royal Society, The},
title = {{Genetic hitchhiking}},
doi = {10.1098/rstb.2000.0716},
volume = {355},
year = {2000},
}
@inbook{4275,
author = {Nicholas Barton},
booktitle = {Encyclopedia of Biodiversity},
pages = {85 -- 94},
publisher = {Academic Press},
title = {{Differentiation}},
doi = {10.1016/B0-12-226865-2/00070-5},
year = {2000},
}
@misc{4276,
author = {Nicholas Barton},
booktitle = {Genetical Research},
number = {3},
pages = {371 -- 373},
publisher = {Cambridge University Press},
title = {{Population genetics of multiple loci}},
volume = {75},
year = {2000},
}
@inproceedings{4433,
abstract = {Bisimulations enjoy numerous applications in the analysis of labeled transition systems. Many of these applications are based on two central observations: first, bisimilar systems satisfy the same branching-time properties; second, bisimilarity can be checked efficiently for finite-state systems. The local character of bisimulation, however, makes it difficult to address liveness concerns. Indeed, the definitions of fair bisimulation that have been proposed in the literature sacrifice locality, and with it, also efficient checkability. We put forward a new definition of fair bisimulation which does not suffer from this drawback.
The bisimilarity of two systems can be viewed in terms of a game played between a protagonist and an adversary. In each step of the infinite bisimulation game, the adversary chooses one system, makes a move, and the protagonist matches it with a move of the other system. Consistent with this game-based view, we call two fair transition systems bisimilar if in the bisimulation game, the infinite path produced in the first system is fair iff the infinite path produced in the second system is fair.
We show that this notion of fair bisimulation enjoys the following properties. First, fairly bisimilar systems satisfy the same formulas of the logics Fair-AFMC (the fair alternation-free μ-calculus) and Fair-CTL*. Therefore, fair bisimulations can serve as property-preserving abstractions for these logics and weaker ones, such as Fair-CTL and LTL. Indeed, Fair-AFMC provides an exact logical characterization of fair bisimilarity. Second, it can be checked in time polynomial in the number of states if two systems are fairly bisimilar. This is in stark contrast to all trace-based equivalences, which are traditionally used for addressing liveness but require exponential time for checking.},
author = {Thomas Henzinger and Rajamani, Sriram K},
pages = {299 -- 314},
publisher = {Springer},
title = {{Fair bisimulation}},
doi = {10.1007/3-540-46419-0_21},
volume = {1785},
year = {2000},
}
@inproceedings{4434,
abstract = {The algorithmic approach to the analysis of timed and hybrid systems is fundamentally limited by undecidability, of universality in the timed case (where all continuous variables are clocks), and of emptiness in the rectangular case (which includes drifting clocks). Traditional proofs of undecidability encode a single Turing computation by a single timed trajectory. These proofs have nurtured the hope that the introduction of “fuzziness” into timed and hybrid models (in the sense that a system cannot distinguish between trajectories that are sufficiently similar) may lead to decidability. We show that this is not the case, by sharpening both fundamental undecidability results. Besides the obvious blow our results deal to the algorithmic method, they also prove that the standard model of timed and hybrid systems, while not “robust” in its definition of trajectory acceptance (which is affected by tiny perturbations in the timing of events), is quite robust in its mathematical properties: the undecidability barriers are not affected by reasonable perturbations of the model.},
author = {Thomas Henzinger and Raskin, Jean-François},
pages = {145 -- 159},
publisher = {Springer},
title = {{Robust undecidability of timed and hybrid systems}},
doi = {10.1007/3-540-46430-1_15},
volume = {1790},
year = {2000},
}
@inproceedings{4435,
abstract = {An important case of hybrid systems are the rectangular automata. First, rectangular dynamics can naturally and arbitrarily closely approximate more general, nonlinear dynamics. Second, rectangular automata are the most general type of hybrid systems for which model checking -in particular, Ltl model checking- is decidable. However, on one hand, the original proofs of decidability did not suggest practical algorithms and, on the other hand, practical symbolic model-checking procedures -such as those implemented in HyTech- were not known to terminate on rectangular automata. We remedy this unsatisfactory situation: we present a symbolic method for Ltl model checking which can be performed by HyTech and is guaranteed to terminate on all rectangular automata. We do so by proving that our method for symbolic Ltl model checking terminates on an infinite-state transition system if the trace-equivalence relation of the system has finite index, which is the case for all rectangular automata.},
author = {Thomas Henzinger and Majumdar, Ritankar S},
pages = {142 -- 156},
publisher = {Springer},
title = {{Symbolic model checking for rectangular hybrid systems}},
doi = {10.1007/3-540-46419-0_11},
volume = {1785},
year = {2000},
}
@inproceedings{4439,
abstract = {We define five increasingly comprehensive classes of infinite-state systems, called STS1–5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.
STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by (1) iterating the predecessor and boolean operations starting from a finite set of observable state sets, and (2) terminating when no new state sets are generated. This enables model checking of the μ-calculus.
STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus.
STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive boolean operations (intersection is restricted to intersection with observables). This enables model checking of linear temporal logic.
STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus.
STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered. This enables model checking of reachability properties.},
author = {Thomas Henzinger and Majumdar, Ritankar S},
pages = {13 -- 34},
publisher = {Springer},
title = {{A classification of symbolic transition systems}},
doi = {10.1007/3-540-46541-3_2},
volume = {1770},
year = {2000},
}
@inproceedings{4481,
abstract = {Since hybrid embedded systems are pervasive and often safety-critical, guarantees about their correct performance are desirable. The hybrid systems model checker HyTech provides such guarantees and has successfully verified some systems. However, HyTech severely restricts the continuous dynamics of the system being analyzed and, therefore, often forces the use of prohibitively expensive discrete and polyhedral abstractions. We have designed a new algorithm, which is capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear differential equations. The new algorithm conservatively overapproximates the reachable states of a hybrid automaton by using interval numerical methods. Interval numerical methods return sets of points that enclose the true result of numerical computation and, thus, avoid distortions due to the accumulation of round-off errors. We have implemented the new algorithm in a successor tool to HyTech called HyperTech. We consider three examples: a thermostat with delay, a two-tank water system, and an air-traffic collision avoidance protocol. HyperTech enables the direct, fully automatic analysis of these systems, which is also more accurate than the use of polyhedral abstractions.},
author = {Thomas Henzinger and Horowitz, Benjamin and Majumdar, Ritankar S and Wong-Toi, Howard},
pages = {130 -- 144},
publisher = {Springer},
title = {{Beyond HyTech: Hybrid systems analysis using interval numerical methods}},
doi = {10.1007/3-540-46430-1_14},
volume = {1790},
year = {2000},
}
@inproceedings{4482,
abstract = {We apply the theory of abstract interpretation to the verification of game properties for reactive systems. Unlike properties expressed in standard temporal logics, game properties can distinguish adversarial from collaborative relationships between the processes of a concurrent program, or the components of a parallel system. We consider two-player concurrent games –say, component vs. environment– and specify properties of such games –say, the component has a winning strategy to obtain a resource, no matter how the environment behaves– in the alternating-time μ-calculus (Aμ ). A sound abstraction of such a game must at the same time restrict the behaviors of the component and increase the behaviors of the environment: if a less powerful component can win against a more powerful environment, then surely the original component can win against the original environment.
We formalize the concrete semantics of a concurrent game in terms of controllable and uncontrollable predecessor predicates, which suffice for model checking all Aμ properties by applying boolean operations and iteration. We then define the abstract semantics of a concurrent game in terms of abstractions for the controllable and uncontrollable predecessor predicates. This allows us to give general characterizations for the soundness and completeness of abstract games with respect to Aμ properties. We also present a simple programming language for multi-process programs, and show how approximations of the maximal abstraction (w.r.t. Aμ properties) can be obtained from the program text. We apply the theory to two practical verification examples, a communication protocol developed at the Berkeley Wireless Research Center, and a protocol converter. In the wireless protocol, both the use of a game property for specification and the use of abstraction for automatic verification were instrumental to uncover a subtle bug.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Mang, Freddy Y and Raskin, Jean-François},
pages = {220 -- 239},
publisher = {Springer},
title = {{Abstract interpretation of game properties}},
doi = {10.1007/978-3-540-45099-3_12},
volume = {1824},
year = {2000},
}
@inproceedings{4483,
abstract = {Model-checking algorithms can be used to verify, formally and automatically, if a low-level description of a design conforms with a high-level description. However, for designs with very large state spaces, prior to the application of an algorithm, the refinement-checking task needs to be decomposed into subtasks of manageable complexity. It is natural to decompose the task following the component structure of the design. However, an individual component often does not satisfy its requirements unless the component is put into the right context, which constrains the inputs to the component. Thus, in order to verify each component individually, we need to make assumptions about its inputs, which are provided by the other components of the design. This reasoning is circular: component A is verified under the assumption that context B behaves correctly, and symmetrically, B is verified assuming the correctness of A. The assume-guarantee paradigm provides a systematic theory and methodology for ensuring the soundness of the circular style of postulating and discharging assumptions in component-based reasoning.We give a tutorial introduction to the assume-guarantee paradigm for decomposing refinement-checking tasks. To illustrate the method, we step in detail through the formal verification of a processor pipeline against an instruction set architecture. In this example, the verification of a three-stage pipeline is broken up into three subtasks, one for each stage of the pipeline.},
author = {Thomas Henzinger and Qadeer,Shaz and Rajamani, Sriram K},
pages = {245 -- 252},
publisher = {IEEE},
title = {{Decomposing refinement proofs using assume-guarantee reasoning}},
doi = {10.1109/ICCAD.2000.896481},
year = {2000},
}
@inproceedings{4512,
abstract = {Masaccio is a formal model for hybrid dynamical systems which are built from atomic discrete components (difference equations) and atomic continuous components (differential equations) by parallel and serial composition, arbitrarily nested. Each system component consists of an interface, which determines the possible ways of using the component, and a set of executions, which define the possible behaviors of the component in real time.
Version 1.0 (May 2000).
},
author = {Thomas Henzinger},
pages = {549 -- 563},
publisher = {Springer},
title = {{Masaccio: A formal model for embedded components}},
doi = {10.1007/3-540-44929-9_38},
volume = {1872},
year = {2000},
}
@inbook{4513,
author = {Thomas Henzinger},
booktitle = {Verification of Digital and Hybrid Systems},
editor = {Inan, M. Kemal and Kurshan, Robert P.},
pages = {265 -- 292},
publisher = {Springer},
title = {{The theory of hybrid automata}},
volume = {170},
year = {2000},
}
@article{4598,
abstract = {A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analyzed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas.},
author = {Alur, Rajeev and Thomas Henzinger and Lafferriere, Gerardo and Pappas, George J.},
journal = {Proceedings of the IEEE},
number = {7},
pages = {971 -- 984},
publisher = {IEEE},
title = {{Discrete abstractions of hybrid systems}},
doi = {10.1109/5.871304 },
volume = {88},
year = {2000},
}
@article{3149,
abstract = {The prohormone convertases (PCs) are an evolutionarily ancient group of proteases required for the maturation of neuropeptide and peptide hormone precursors. In Drosophila melanogaster, the homolog of prohormone convertase 2, dPC2 (amontillado), is required for normal hatching behavior, and immunoblotting data indicate that flies express 80- and 75-kDa forms of this protein. Because mouse PC2 (mPC2) requires 7B2, a helper protein for productive maturation, we searched the fly data base for the 7B2 signature motif PPNPCP and identified an expressed sequence tag clone encoding the entire open reading frame for this protein. dPC2 and d7B2 cDNAs were subcloned into expression vectors for transfection into HEK-293 cells; mPC2 and rat 7B2 were used as controls. Although active mPC2 was detected in medium in the presence of either d7B2 or r7B2, dPC2 showed no proteolytic activity upon coexpression of either d7B2 or r7B2. Labeling experiments showed that dPC2 was synthesized but not secreted from HEK-293 cells. However, when dPC2 and either d7B2 or r7B2 were coexpressed in Drosophila S2 cells, abundant immunoreactive dPC2 was secreted into the medium, coincident with the appearance of PC2 activity. Expression and secretion of dPC2 enzyme activity thus appears to require insect cell-specific posttranslational processing events. The significant differences in the cell biology of the insect and mammalian enzymes, with 7B2 absolutely required for secretion of dPC2 and zymogen conversion occurring intracellularly in the case of dPC2 but not mPC2, support the idea that the Drosophila enzyme has specific requirements for maturation and secretion that can be met only in insect cells.},
author = {Hwang, Jae R and Daria Siekhaus and Fuller, Robert S and Taghert, Paul H and Lindberg, Iris},
journal = {Journal of Biological Chemistry},
number = {23},
pages = {17886 -- 17893},
publisher = {American Society for Biochemistry and Molecular Biology},
title = {{Interaction of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect cell specific processing and secretion}},
doi = {10.1074/jbc.M000032200 },
volume = {275},
year = {2000},
}
@article{3489,
abstract = {We have examined factors that determine the strength and dynamics of GABAergic synapses between interneurons [dentate gyrus basket cells (BCs)] and principal neurons [dentate gyrus granule cells (GCs)] using paired recordings in rat hippocampal slices at 34°C. Unitary IPSCs recorded from BC–GC pairs in high intracellular Cl− concentration showed a fast rise and a biexponential decay, with mean time constants of 2 and 9 msec. The mean quantal conductance change, determined directly at reduced extracellular Ca2+/Mg2+concentration ratios, was 1.7 nS. Quantal release at the BC–GC synapse occurred with short delay and was highly synchronized. Analysis of IPSC peak amplitudes and numbers of failures by multiple probability compound binomial analysis indicated that synaptic transmission at the BC–GC synapse involves three to seven release sites, each of which releases transmitter with high probability (∼0.5 in 2 mMCa2+/1 mM Mg2+). Unitary BC–GC IPSCs showed paired-pulse depression (PPD); maximal depression, measured for 10 msec intervals, was 37%, and recovery from depression occurred with a time constant of 2 sec. Paired-pulse depression was mainly presynaptic in origin but appeared to be independent of previous release. Synaptic transmission at the BC–GC synapse showed frequency-dependent depression, with half-maximal decrease at 5 Hz after a series of 1000 presynaptic action potentials. The relative stability of transmission at the BC–GC synapse is consistent with a model in which an activity-dependent gating mechanism reduces release probability and thereby prevents depletion of the releasable pool of synaptic vesicles. Thus several mechanisms converge on the generation of powerful and sustained transmission at interneuron–principal neuron synapses in hippocampal circuits.},
author = {Kraushaar, Udo and Peter Jonas},
journal = {Journal of Neuroscience},
number = {15},
pages = {5594 -- 5607},
publisher = {Society for Neuroscience},
title = {{Efficacy and stability of quantal GABA release at a hippocampal interneuron-principal neuron synapse}},
volume = {20},
year = {2000},
}
@article{3490,
abstract = {Long-term depression (LTD) is a form of synaptic plasticity that can be induced either by low-frequency stimulation of presynaptic fibers or in an associative manner by asynchronous pairing of presynaptic and postsynaptic activity. We investigated the induction mechanisms of associative LTD in CA1 pyramidal neurons of the hippocampus using whole-cell patch-clamp recordings and Ca2+ imaging in acute brain slices. Asynchronous pairing of postsynaptic action potentials with EPSPs evoked with a delay of 20 msec induced a robust, long-lasting depression of the EPSP amplitude to 43%. Unlike LTD induced by low-frequency stimulation, associative LTD was resistant to the application of D-AP-5, indicating that it is independent of NMDA receptors. In contrast, associative LTD was inhibited by (S)-α-methyl-4-carboxyphenyl-glycine, indicating the involvement of metabotropic glutamate receptors. Furthermore, associative LTD is dependent on the activation of voltage-gated Ca2+ channels by postsynaptic action potentials. Both nifedipine, an L-type Ca2+ channel antagonist, and ω-conotoxin GVIA, a selective N-type channel blocker, abolished the induction of associative LTD. 8-hydroxy-2-dipropylaminotetralin (OH-DPAT), a 5-HT(1A) receptor agonist, inhibited postsynaptic Ca2+ influx through N-type Ca2+ channels, without affecting presynaptic transmitter release. OH-DPAT also inhibited the induction of associative LTD, suggesting that the involvement of N-type channels makes synaptic plasticity accessible to modulation by neurotransmitters. Thus, the modulation of N-type Ca2+ channels provides a gain control for synaptic depression in hippocampal pyramidal neurons.},
author = {Normann, Claus and Peckys, Diana and Schulze, Christian H and Walden, Jörg and Peter Jonas and Bischofberger, Joseph},
journal = {Journal of Neuroscience},
number = {22},
pages = {8290 -- 8297},
publisher = {Society for Neuroscience},
title = {{Associative long-term depression in the hippocampus is dependent on postsynaptic N-type Ca(2+) channels}},
volume = {20},
year = {2000},
}
@article{3491,
abstract = {Fast and reliable activation of inhibitory interneurons is critical for the stability of cortical neuronal networks. Active conductances in dendrites may facilitate interneuron activation, but direct experimental evidence was unavailable. Patch-clamp recordings from dendrites of hippocampal oriens- alveus interneurons revealed high densities of voltage-gated sodium and potassium ion channels. Simultaneous recordings from dendrites and somata suggested that action potential initiation occurs preferentially in the axon with long threshold stimuli, but can be shifted to somatodendritic sites when brief stimuli are applied. After initiation, action potentials propagate over the somatodendritic domain with constant amplitude, high velocity, and reliability, even during high-frequency trains.},
author = {Martina, Marco and Vida, Imre and Peter Jonas},
journal = {Science},
number = {5451},
pages = {295 -- 300},
publisher = {American Association for the Advancement of Science},
title = {{Distal initiation and active propagation of action potentials in interneuron dendrites}},
doi = {10.1126/science.287.5451.295},
volume = {287},
year = {2000},
}
@article{3492,
abstract = {Analysis of presynaptic determinants of synaptic strength has been difficult at cortical synapses, mainly due to the lack of direct access to presynaptic elements. Here we report patch-clamp recordings from mossy fiber boutons (MFBs) in rat hippocampal slices. The presynaptic action potential is very short during low-frequency stimulation but is prolonged up to 3-fold during high-frequency stimulation. Voltage-gated K+ channels in MFBs inactivate rapidly but recover from inactivation very slowly, suggesting that cumulative K+ channel inactivation mediates activity-dependent spike broadening. Prolongation of the presynaptic voltage waveform leads to an increase in the number of Ca2+ ions entering the terminal per action potential and to a consecutive potentiation of evoked excitatory postsynaptic currents at MFB-CA3 pyramidal cell synapses. Thus, inactivation of presynaptic K+ channels contributes to the control of efficacy of a glutamatergic synapse in the cortex.},
author = {Geiger, Jörg R and Peter Jonas},
journal = {Neuron},
number = {3},
pages = {927 -- 939},
publisher = {Elsevier},
title = {{Dynamic control of presynaptic Ca(2+) inflow by fast-inactivating K+ channels in hippocampal mossy fiber boutons}},
doi = {10.1016/S0896-6273(00)00164-1},
volume = {28},
year = {2000},
}
@article{3532,
abstract = {Multichannel tetrode array recording in awake behaving animals provides a powerful method to record the activity of large numbers of neurons. The power of this method could be extended if further information concerning the intracellular state of the neurons could be extracted from the extracellularly recorded signals. Toward this end, we have simultaneously recorded intracellular and extracellular signals from hippocampal CA1 pyramidal cells and interneurons in the anesthetized rat. We found that several intracellular parameters can be deduced from extracellular spike waveforms. The width of the intracellular action potential is defined precisely by distinct points on the extracellular spike. Amplitude changes of the intracellular action potential are reflected by changes in the amplitude of the initial negative phase of the extracellular spike, and these amplitude changes are dependent on the state of the network. In addition, intracellular recordings from dendrites with simultaneous extracellular recordings from the soma indicate that, on average, action potentials are initiated in the perisomatic region and propagate to the dendrites at 1.68 m/s. Finally we determined that a tetrode in hippocampal area CA1 theoretically should be able to record electrical signals from similar to 1,000 neurons. Of these, 60-100 neurons should generate spikes of sufficient amplitude to be detectable from the noise and to allow for their separation using current spatial clustering methods. This theoretical maximum is in contrast to the approximately six units that are usually detected per tetrode. From this, we conclude that a large percentage of hippocampal CA1 pyramidal cells are silent in any given behavioral condition.},
author = {Henze, Darrell A and Borhegyi, Zsolt and Jozsef Csicsvari and Mamiya, Akira and Harris, Kenneth D and Buzsáki, György},
journal = {Journal of Neurophysiology},
number = {1},
pages = {390 -- 400},
publisher = {American Physiological Society},
title = {{Intracellular features predicted by extracellular recordings in the hippocampus in vivo}},
volume = {84},
year = {2000},
}
@article{3542,
abstract = {Transfer of neuronal patterns from the CA3 to CA1 region was studied by simultaneous recording of neuronal ensembles in the behaving rat. A nonlinear interaction among pyramidal neurons was observed during sharp wave (SPW)-related population bursts, with stronger synchrony associated with more widespread spatial coherence. SPW bursts emerged in the CA3a-b subregions and spread to CA3c before invading the CA1 area. Synchronous discharge of >10% of the CA3 within a 100 ms window was required to exert a detectable influence on CA1 pyramidal cells. Activity of some CA3 pyramidal neurons differentially predicted the ripple-related discharge of circumscribed groups of CA1 pyramidal cells. We suggest that, in SPW behavioral state, the coherent discharge of a small group of CA3 cells is the primary cause of spiking activity in CA1 pyramidal neurons.},
author = {Jozsef Csicsvari and Hirase, Hajima and Mamiya, Akira and Buzsáki, György},
journal = {Neuron},
number = {2},
pages = {585 -- 594},
publisher = {Elsevier},
title = {{Ensemble patterns of hippocampal CA3-CA1 neurons during sharp wave-associated population events}},
doi = {10.1016/S0896-6273(00)00135-5},
volume = {28},
year = {2000},
}
@article{3548,
abstract = {Simultaneous recording from large numbers of neurons is a prerequisite for understanding their cooperative behavior. Various recording techniques and spike separation methods are being used toward this goal. However, the error rates involved in spike separation have not yet been quantified. We studied the separation reliability of “tetrode” (4-wire electrode) recorded spikes by monitoring simultaneously from the same cell intracellularly with a glass pipette and extracellularly with a tetrode. With manual spike sorting, we found a trade-off between Type I and Type II errors, with errors typically ranging from 0 to 30% depending on the amplitude and firing pattern of the cell, the similarity of the waveshapes of neighboring neurons, and the experience of the operator. Performance using only a single wire was markedly lower, indicating the advantages of multiple-site monitoring techniques over single-wire recordings. For tetrode recordings, error rates were increased by burst activity and during periods of cellular synchrony. The lowest possible separation error rates were estimated by a search for the best ellipsoidal cluster shape. Human operator performance was significantly below the estimated optimum. Investigation of error distributions indicated that suboptimal performance was caused by inability of the operators to mark cluster boundaries accurately in a high-dimensional feature space. We therefore hypothesized that automatic spike-sorting algorithms have the potential to significantly lower error rates. Implementation of a semi-automatic classification system confirms this suggestion, reducing errors close to the estimated optimum, in the range 0-8%.},
author = {Harris, Kenneth D and Henze, Darrell A and Jozsef Csicsvari and Hirase, Hajima and Buzsáki, György},
journal = {Journal of Neurophysiology},
number = {1},
pages = {401 -- 414},
publisher = {American Physiological Society},
title = {{Accuracy of tetrode spike separation as determined by simultaneous intracellular and extracellular measurements}},
volume = {84},
year = {2000},
}
@inproceedings{3555,
abstract = {A sliver is a tetrahedron whose four vertices lie close to a plane and whose perpendicular projection to that plane is a convex quadrilateral with no short edge. Slivers are both undesirable and ubiquitous in 3-dimensional Delaunay triangulations. Even when the point-set is well-spaced, slivers may result. This paper shows that such a point set permits a small perturbation whose Delaunay triangulation contains no slivers. It also gives deterministic algorithms that compute the perturbation of n points in time O(n log n) with one processor and in time O(log n) with O(n) processors.},
author = {Herbert Edelsbrunner and Xiang Li and Miller, Gary and Stathopoulos, Andreas and Talmor, Dafna and Teng, Shang Hua and Üngör, Alper and Walkington, Noel},
pages = {273 -- 277},
publisher = {ACM},
title = {{Smoothing and cleaning up slivers}},
doi = {10.1145/335305.335338},
year = {2000},
}
@inbook{3572,
abstract = {Allzulange wurde die spielhafte Beschäftigung als Gegensatz zu ernsthafter Arbeit gesehen. Dieser Artikel propagiert die spielerische Untersuchung von Kreis- und Kugelmengen. Gleichzeitig belegt er die nutzbare Anwendung
von elementaren Einsichten in der Molekularbiologie und allgemeiner
in der Beschreibung von Form und Verformung.},
author = {Herbert Edelsbrunner},
booktitle = {Zur Kunst des formalen Denkens},
pages = {153 -- 171},
publisher = {Passagen Verlag},
title = {{Spielereien mit Kreisen und Kugeln. Zum Thema Form und Verformung}},
year = {2000},
}
@article{3583,
abstract = {The Delaunay triangulation of a finite point set is a central theme in computational geometry. It finds its major application in the generation of meshes used in the simulation of physical processes. This paper connects the predominantly combinatorial work in classical computational geometry with the numerical interest in mesh generation. It focuses on the two- and three-dimensional case and covers results obtained during the twentieth century.},
author = {Herbert Edelsbrunner},
journal = {Acta Numerica},
pages = {133 -- 213},
publisher = {Cambridge University Press},
title = {{Triangulations and meshes in computational geometry}},
volume = {9},
year = {2000},
}
@article{3623,
abstract = {We present the theoretical background to a new method for measuring genetic variation for total fitness in Drosophila. The method allows heterozygous effects on total fitness of whole wild-type chromosomes to be measured under normal demography with overlapping generations. The wild-type chromosomes are competed against two balancer chromosomes (B1, B2, say), providing a standard genotype B1/B2 against which variation in the fitness effects of the wild-type chromosomes can be assessed. Fitness can be assessed in two ways: (i) at equilibrium of all three chromosomes under heterozygote advantage, and (ii) during displacement of one balancer by the other. Equilibrium with all three chromosomes present will be achieved only if the wild-type homozygote is not too fit, and if the fitnesses of the three heterozygotes are not too unequal. These conditions were not satisfied for any of a sample of 12 lethal-bearing chromosomes isolated from a random-bred laboratory population of Drosophila. At equilibrium, genotypic frequencies show low sensitivity to changes in genotypic fitness. Furthermore, where all four genotypes are viable and fertile, supplementary information from cages with only two chromosomes present and from direct measurements of pre-adult viability are required to estimate fitnesses from frequencies. The invasion method has the advantages of a greater sensitivity and of not requiring further data to estimate fitnesses if the wild-type homozygote is fertile. However, it requires that multiple samples be taken as the invasion progresses. In a discrete generation model, generation time influences fitness estimates from this method and is difficult to estimate accurately from the data. A full age-structured model can also be applied to the data from both types of experiment. For the invasion method, this gives fitness estimates close to those from the discrete generation model.},
author = {Nicholas Barton and Patridge, Linda},
journal = {Genetical Research},
number = {3},
pages = {297 -- 314},
publisher = {Cambridge University Press},
title = {{Measuring fitness by means of balancer chromosomes}},
doi = {10.1017/S0016672399004346},
volume = {75},
year = {2000},
}
@article{3624,
abstract = {The state of a diploid population segregating for two alleles at each of n loci is described by 22(n) genotype frequencies, or equivalently, by allele frequencies and by multilocus moments or cumulants of various orders. These measures of linkage disequilibrium cannot usually be determined, both because one cannot tell whether a gene came from the maternal or paternal gamete, and because such a large number of parameters cannot be estimated even from large samples. Simplifying assumptions must therefore be made. This paper sets out methods for estimating multilocus genotype frequencies which are appropriate for unlinked neutral loci, and for populations that are ultimately derived by mixing of two source populations. In such a hybrid population, all multilocus associations depend primarily on the number of loci involved that derive from the maternal genome, and the number derived from the paternal genome Allele frequencies may differ across loci, and the contribution of each locus to multilocus associations may be scaled by the difference in allele frequency between source populations for that locus (δp ≤ 1). For example, the cumulant describing the association between genes i, j, k from the maternal genome, and genes i, l from the paternal genome is K(tJ,k,iλ*), = δp(i)/2 δp(J) δp(k) δp(l) κ3,2. The state of the population is described by n allele frequencies; n divergences, δp; and by a symmetric matrix of cumulants, κ(J,K) (J = 0 ,..., n, K = 0 ,..., n). Expressions for these cumulants under short- and long-range migration are given. Two methods for estimating the cumulants are described: a simple method based on multivariate moments, and a maximum likelihood procedure, which uses the Metropolis algorithm. Both methods perform well when tested against simulations with two or four loci.},
author = {Nicholas Barton},
journal = {Heredity},
number = {3},
pages = {373 -- 389},
publisher = {Nature Publishing Group},
title = {{Estimating multilocus linkage disequilibria}},
doi = {10.1046/j.1365-2540.2000.00683.x},
volume = {84},
year = {2000},
}
@article{2591,
abstract = {The occurrence and distribution of the preferred receptor for the neuropeptide, substance P (SP), the neurokinin-1 receptor (NK1R) was investigated in the vascular supply of the rat sciatic nerve. Messenger RNA for NK1R was demonstrated by RT-PCR in the epineurial layer where the majority of small arteries and arterioles feeding the endoneurial vasculature are located. Immunoreactivity to NK1R-protein was localized on the smooth muscle cells of these arterial vessels by means of immunofluorescence using a polyclonal NK1R antiserum. This muscular localization of NK1R explains the previously reported [Zochodne, D.W. and Ho, L.T., J. Physiol. 444 (1991) 615- 630] moderate vasoconstrictor rather than vasodilator effects of SP in this vascular bed.},
author = {Kummer, Wolfgang and Ryuichi Shigemoto and Haberberger, Rainer V},
journal = {Neuroscience Letters},
number = {2},
pages = {119 -- 122},
publisher = {Elsevier},
title = {{Smooth muscle cells are the site of neurokinin-1 receptor localization in the arterial supply of the rat sciatic nerve}},
doi = {10.1016/S0304-3940(98)00926-4},
volume = {259},
year = {1999},
}
@article{2592,
abstract = {Metabotropic glutamate receptors (mGluRs) consist of eight different subtypes and exert their effects or second messengers and ion channels via G- proteins. The function of individual mGluR subtypes in the CNS, however, largely remains to be clarified. We examined the fear response of freezing after electric shock in wild-type and mGluR7(-/-) knockout littermates. Wild- type mice displayed freezing immediately after and 1 d after footshock. In comparison, mGluR7(-/-) knockout mice showed significantly reduced levels in both immediate postshock and delayed freezing responses. However, the knockout mice exhibited no abnormalities in pain sensitivity and locomotor activity. To further examine amygdala-dependent behavior, we performed conditioned taste aversion (CTA) experiments. In wild-type mice, the administration of saccharin followed by intraperitoneal injection of the malaise-inducing agent LiCl resulted in an association between saccharin and LiCl. This association caused strong CTA toward saccharin n contrast, mGluR7(-/-) knockout mice failed to associate between the taste and the negative reinforcer in CTA experiments. Again, the knockout mice showed no abnormalities in taste preference and in the sensitivity to LiCl toxicity. These results indicate that mGluR7 deficiency causes an impairment of two distinct amygdala-dependent behavioral paradigms. Immunohistochemical and immunoelectron-microscopic analyses showed that mGluR7 is highly expressed in amygdala and preferentially localized at the presynaptic axon terminals of glutamatergic neurons. Together, these findings strongly suggest that mGluR7 is involved in neural processes subserving amygdala-dependent averse responses.},
author = {Masugi, Miwako and Yokoi, Mineto and Ryuichi Shigemoto and Muguruma, Keiko and Watanabe, Yasuyoshi and Sansig, Gilles and Van Der Putten, Herman V and Nakanishi, Shigetada},
journal = {Journal of Neuroscience},
number = {3},
pages = {955 -- 963},
publisher = {Society for Neuroscience},
title = {{Metabotropic glutamate receptor subtype 7 ablation causes deficit in fear response and conditioned taste aversion}},
volume = {19},
year = {1999},
}
@article{2593,
abstract = {In cat and monkey, lamina I cells can be classified into three basic morphological types (fusiform, pyramidal, and multipolar), and recent intracellular labeling evidence in the cat indicates that fusiform and multipolar lamina I cells are two different types of nociceptive cells, whereas pyramidal cells are innocuous thermoreceptive-specific. Because earlier observations indicated that only nociceptive dorsal horn neurons respond to substance P (SP), we examined which morphological types of lamina I neurons express receptors for SP (NK-1r). We categorized NK-1r- immunoreactive (IR) lamina I neurons in serial horizontal sections from the cervical and lumbar enlargements of four monkeys. Consistent results were obtained by two independent teams of observers. Nearly all NK-1r-IR cells were fusiform (42%) or multipolar (43%), but only 6% were pyramidal (with 9% unclassified). We obtained similar findings in three monkeys in which we used double-labeling immunocytochemistry to identify NK-1r-IR and spinothalamic lamina I neurons retrogradely labeled with cholera toxin subunit b from the thalamus; most NK-1r-IR lamina I spinothalamic neurons were fusiform (48%) or multipolar (33%), and only 10% were pyramidal. In contrast, most (~75%) pyramidal and some (~25%) fusiform and multipolar lamina I spinothalamic neurons did not display NK-1r immunoreactivity. These data indicate that most fusiform and multipolar lamina I neurons in the monkey can express NK-1r, consistent with the idea that both types are nociceptive, whereas only a small proportion of lamina I pyramidal cells express this receptor, consistent with the previous finding that they are nonnociceptive. However, these findings also indicate that not all nociceptive lamina I neurons express receptors for SP.},
author = {Yu, Xiao-Hong and Zhang, En T and Craig, Arthur D and Ryuichi Shigemoto and Ribeiro-da-Silva, Alfredo and De Koninck, Yves},
journal = {Journal of Neuroscience},
number = {9},
pages = {3545 -- 3555},
publisher = {Society for Neuroscience},
title = {{NK-1 receptor immunoreactivity in distinct morphological types of lamina I neurons of the primate spinal cord}},
volume = {19},
year = {1999},
}
@article{2594,
abstract = {Substance P receptor (i.e. NK1)-like immunoreactive (SPR-LI) neurons were observed in the newborn and adult human spinal cord. Substance P receptor-like immunoreactive neuronal cell bodies were seen most frequently in lamina I, and were scattered throughout the remaining laminae of the dorsal horn and the area around the central canal. Some neurons in the intermediolateral nucleus also showed weak immunoreactivity. The pattern of distribution of SPR-LI neurons in the adult spinal cord was essentially the same as that in the newborn spinal cord. However, SPR-LI neurons cell bodies were seen much more frequently in the newborn than in the adult dorsal horn, especially in lamina II.},
author = {Ding, Yu-Qiang and Zheng, Heng-Xing and Wang, Dian-Shi and Xu, Jun-Qing and Gong, Liang-Wei and Lü, Yan and Qin, Bing-Zhi and Shi, Juan and Li, Hua L and Li, Ji-Shuo and Ryuichi Shigemoto and Kaneko, Takeshi and Mizuno, Noboru},
journal = {Neuroscience Letters},
number = {2},
pages = {133 -- 136},
publisher = {Elsevier},
title = {{The distribution of substance P receptor (NK1)-like immunoreactive neurons in the newborn and adult human spinal cord}},
doi = {10.1016/S0304-3940(99)00283-9},
volume = {266},
year = {1999},
}
@article{2595,
abstract = {Presynaptic metabotropic glutamate receptors (mGluRs) of group III constitute possible targets for putative neuroprotective drugs acting against glutamate excitotoxic insults. Indeed, in glutamatergic cerebellar granule neurones in culture, high concentrations of L-2-amino-4-phosphonobutyrate (L-AP4, above 0.3 mM, thus activating mGluR7) inhibit NMDA-induced cell death. In contrast, in striatal cultures which are enriched in GABAergic neurones, we show that high concentrations of L-AP4 increased neuronal death in control as well as in NMDA-stimulated cultures. Moreover, similar results were obtained with the GABA(B)R agonist, baclofen. Both the neuroprotective effects in cerebellar granule cells and the neurotoxic effects in striatal neurones were mediated via Gi-Go-coupled mGluRs, suggesting that these effects were probably mediated by mGluR7a or b and GABA(B)R expressed in these neurones. In striatal neurones, we found that L-AP4 and baclofen inhibited both basal and NMDA-stimulated GABA release. These inhibitions of GABA release may be responsible for the increase in basal and NMDA-stimulated neuronal death. Indeed, blockade of GABA(A) receptors with bicuculline increased neuronal death of control and NMDA-treated striatal cultures. Taken together, these results suggest that L-AP4 and baclofen, via mGluR7 and GABA(B)R, reduced the neuroprotective effect of GABA present in striatal cultures acting via GABA(A) receptors. Although caution must be taken when extrapolating from in vitro to in vivo situations, the present experiments and the recent observations that mGluR7 and GABA(B)R are expressed in heterologous synapses, should be taken into consideration when evaluating the neuroprotective action of future mGluR7 specific agonists or GABA(B)R specific antagonists.},
author = {Lafon-Cazal, Mireille and Viennois, Gaëlle and Kühn, Rainer and Malitschek, Barbara and Pin, Jean-Philippe and Ryuichi Shigemoto and Bockaërt, Joël L},
journal = {Neuropharmacology},
number = {10},
pages = {1631 -- 1640},
publisher = {Elsevier},
title = {{mGluR7-like receptor and GABA(B) receptor activation enhance neurotoxic effects of N-methyl-D-aspartate in cultured mouse striatal GABAergic neurones}},
doi = {10.1016/S0028-3908(99)00124-0},
volume = {38},
year = {1999},
}
@article{2596,
abstract = {A γ-aminobutyric acid (GABA)(B) receptor (named GABA(B)R1) has been recently cloned in the rat and human brain and two variants generated by alternative RNA splicing were identified. In the present study, we addressed the question as to whether these variants contribute to the diversity of GABA(B) receptor-mediated physiological responses and constitute real receptor subtypes with distinct functions. To this aim, we have mapped the GABA(B)R1 (R1a) and GABA(B)R1b (R1b) transcript distribution in the rat brain using in situ hybridization. We have compared the mRNA distribution with the distribution of [ 3H]CGP54626-labeled binding GABA(B)R1 receptor sites as assessed in adjacent cryosections by quantitative autoradiography. We found that GABA(B) receptor transcripts and binding sites are expressed in the brain in almost all neuronal cell populations. Expression in glial cells, if any, is marginal. We observed a good parallelism between GABA(B)R1 mRNA transcripts and binding sites in broad neuroanatomical entities with highest densities in hippocampus, thalamic nuclei, and cerebellum. By contrast, R1a and R1b transcripts exhibit marked differences in their regional and cellular distribution pattern. A typical example is the cerebellum with an almost exclusive expression of R1b in the Purkinje cells and of R1a in the granule, stellate, and basket cells. Data pointing at a pre- versus postsynaptic localization for R1a and R1b, respectively, at some neuronal sites are presented.
},
author = {Bischoff, Serge F and Leonhard, Sabine and Reymann, Nicole C and Schuler, Valérie and Ryuichi Shigemoto and Kaupmann, Klemens and Bettler, Bernhard},
journal = {Journal of Comparative Neurology},
number = {1},
pages = {1 -- 16},
publisher = {Wiley-Blackwell},
title = {{Spatial distribution of GABA(B)R1 receptor mRNA and binding sites in the rat brain^}},
doi = {10.1002/(SICI)1096-9861(19990913)412:1<1::AID-CNE1>3.0.CO;2-D},
volume = {412},
year = {1999},
}
@article{2597,
abstract = {Metabotropic glutamate receptors (mGlus) are known to modulate synaptic transmission in various pathways of the central nervous system, but the exact mechanisms by which this modulation occurs remain unclear. Here we utilise electrophysiological and immunocytochemical techniques on cultured autaptic hippocampal neurones to investigate the mechanism of action and distribution of mGlus. Agonists at all three groups of mGlus depressed glutamatergic transmission, whereas only agonists at group I mGlus depressed GABAergic transmission. Agonists at all mGlus failed to modulate Ca2+ and K+ channels in glutamatergic autapses whereas an agonist at group III mGlus did depress the frequency of miniature excitatory postsynaptic currents (mEPSCs). Agonists failed to modulate Ca2+ or K+ channels and miniature inhibitory postsynaptic currents (mIPSCs) in GABAergic autapses. Distribution studies using selective antibodies revealed punctate staining for group III mGlus that co-localised with the synaptic marker, synaptophysin. Staining for the remaining mGlus was more diffuse throughout the soma and processes with little co-localisation with synaptophysin. The distribution of the group III receptors is consistent with the direct 'downstream' modulation of mEPSCs, although the exact mechanism of action for the remaining receptors remains unclear.},
author = {Bushell, Trevor J and Lee, Chong C and Ryuichi Shigemoto and Miller, Richard J},
journal = {Neuropharmacology},
number = {10},
pages = {1553 -- 1567},
publisher = {Elsevier},
title = {{Modulation of synaptic transmission and differential localisation of mGlus in cultured hippocampal autapses}},
doi = {10.1016/S0028-3908(99)00103-3},
volume = {38},
year = {1999},
}
@inproceedings{2711,
abstract = {We study the long time evolution of a quantum particle in a Gaussian random environment. We show that in the weak coupling limit the Wigner distribution of the wave function converges to the solution of a linear Boltzmann equation globally in time. The Boltzmann collision kernel is given by the Born approximation of the quantum scattering cross section.},
author = {László Erdös},
pages = {233 -- 242},
publisher = {World Scientific Publishing},
title = {{Linear Boltzmann equation as the weak coupling limit of the random Schrödinger equation}},
doi = {10.1007/978-3-0348-8745-8_20},
volume = {108},
year = {1999},
}
@article{2730,
author = {László Erdös and Solovej, Jan P},
journal = {Duke Mathematical Journal},
number = {1},
pages = {127 -- 173},
publisher = {Duke University Press},
title = {{Semiclassical eigenvalue estimates for the Pauli operator with strong nonhomogeneous magnetic fields, I: Nonasymptotic Lieb-Thirring-type estimate}},
doi = {10.1215/S0012-7094-99-09604-7},
volume = {96},
year = {1999},
}
@article{2783,
abstract = {Pattern formation in a layer of fluid heated from below is an example of macroscopic ordering in continuous media. Here we show that in a relatively compact experimental version of the problem, a rich and diverse set of stable flows can be found. These flows, many of which are novel, can be categorized and understood in terms of their symmetry properties. This approach shows promise for providing insight into the more complicated fluid motion that occurs as the lateral dimension of the layer is increased.},
author = {Björn Hof and Lucas, Peter G and Mullin, Tom P},
journal = {Physics of Fluids},
number = {10},
pages = {2815 -- 2817},
publisher = {American Institute of Physics},
title = {{Flow state multiplicity in convection}},
doi = {10.1063/1.870178 },
volume = {11},
year = {1999},
}
@article{2864,
abstract = {Using an electrospray tandem mass spectrometer as a concentration-sensitive detector, a method has been developed to quantify femtomole amounts of plant growth regulators (i.e. isoprenoid type cytokinins, zeatin, dihydrozeatin, isopentenyladenine and their respective riboside and glucoside analogues) and the second messenger adenosine 3':5'-cyclic monophosphate (3':5'-cAMP). Miniaturisation of the chromatographic setup using capillary high performance liquid chromatographic (HPLC) ion spray mass spectrometry increased the sensitivity to the low femtomole region. Application of automated capillary column switching allowed the introduction of large injection volumes into the HPLC system. Aliquots (25 μL) were injected into one dimension of the HPLC set-up and stacked onto a micro pre-column. By means of mobile phase switching the pre-column was back-flushed to introduce the analytes onto the analytical column. For cytokinin analysis positive electrospray ionisation was used and resulted in 2.5-25 fmol detection limits. Cyclic nucleotides were separated under ion-pair conditions using tetrabutyl ammonium bromide as ion-pair reagent and were detected under negative electrospray ionisation conditions. Here a 25 fmol detection limit was determined. Following this approach, cytokinins and 3':5'-cAMP extracted from only mg amounts of apical shoot meristem and chloroplasts obtained from Nicotiana tabacum cv. Petit Havana SR1 were identified and quantified.},
author = {Witters, Erwin and Vanhoutte, Koen and Dewitte, Walter and Macháčková, Ivana and Eva Benková and Van Dongen, Walter and Esmans, Eddy L and Van Onckelen, Henri A},
journal = {Phytochemical Analysis},
number = {3},
pages = {143 -- 151},
publisher = {Wiley-Blackwell},
title = {{Analysis of cyclic nucleotides and cytokinins in minute plant samples using phase system switching capillary electrospray liquid chromatography tandem mass spectrometry}},
doi = {10.1002/(SICI)1099-1565(199905/06)10:3<143::AID-PCA441>3.0.CO;2-G},
volume = {10},
year = {1999},
}
@article{2865,
abstract = {Although cytokinins (CKs) affect a number of processes connected with chloroplasts, it has never been rigorously proven that chloroplasts contain CKs. We isolated intact chloroplasts from tobacco (Nicotiana tabacum L. cv SR1) and wheat (Triticum aestivum L. cv Ritmo) leaves and determined their CKs by liquid chromatography/tandem mass spectroscopy. Chloroplasts from both species contained a whole spectrum of CKs, including free bases (zeatin and isopentenyladenine), ribosides (zeatin riboside, and isopentenyladenosine), ribotides (isopentenyladenosine-5′-monophosphate, zeatin riboside-5′-monophosphate, and dihydrozeatin riboside-5′-monophosphate), and N-glucosides (zeatin-N 9-glucoside, dihydrozeatin-N 9-glucoside, zeatin-N 7-glucoside, and isopentenyladenine-N-glucosides). In chloroplasts there was a moderately higher relative amount of bases, ribosides, and ribotides than in leaves, and a significantly increased level ofN 9-glucosides of zeatin and dihydrozeatin. Tobacco and wheat chloroplasts were prepared from leaves at the end of either a dark or light period. After a dark period, chloroplasts accumulated more CKs than after a light period. The differences were moderate for free bases and ribosides, but highly significant for glucosides. Tobacco chloroplasts from dark-treated leaves contained zeatin riboside-O-glucoside and dihydrozeatin riboside-O-glucoside, as well as a relatively high CK oxidase activity. These data show that chloroplasts contain a whole spectrum of CKs and the enzymatic activity necessary for their metabolism. },
author = {Eva Benková and Witters, Erwin and Van Dongen, Walter and Kolář, Jan and Motyka, Václav and Brzobohatý, Břetislav and Van Onckelen, Henri A and Macháčková, Ivana},
journal = {Plant Physiology},
number = {1},
pages = {245 -- 251},
publisher = {American Society of Plant Biologists},
title = {{Cytokinins in tobacco and wheat chloroplasts. Occurrence and changes due to light/dark treatment}},
doi = {10.1104/pp.121.1.245},
volume = {121},
year = {1999},
}
@article{8526,
author = {Kaloshin, Vadim},
issn = {0003-486X},
journal = {The Annals of Mathematics},
keywords = {Statistics, Probability and Uncertainty, Statistics and Probability},
number = {2},
pages = {729--741},
publisher = {JSTOR},
title = {{An extension of the Artin-Mazur theorem}},
doi = {10.2307/121093},
volume = {150},
year = {1999},
}
@article{883,
abstract = {Sympatric speciation, the origin of two or more species from a single local population, has almost certainly been involved in formation of several species flocks, and may be fairly common in nature. The most straightforward scenario for sympatric speciation requires disruptive selection favouring two substantially different phenotypes, and consists of the evolution of reproductive isolation between them followed by the elimination of all intermediate phenotypes. Here we use the hypergeometric phenotypic model to show that sympatric speciation is possible even when fitness and mate choice depend on different quantitative traits, so that speciation must involve formation of covariance between these traits. The increase in the number of variable loci affecting fitness facilitates sympatric speciation, whereas the increase in the number of variable loci affecting mate choice has the opposite effect. These predictions may enable more cases of sympatric speciation to be identified.},
author = {Kondrashov, Alexey S and Fyodor Kondrashov},
journal = {Nature},
number = {6742},
pages = {351 -- 354},
publisher = {Nature Publishing Group},
title = {{Interactions among quantitative traits in the course of sympatric speciation}},
doi = {10.1038/22514},
volume = {400},
year = {1999},
}
@inproceedings{4601,
abstract = {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.
Depending on whether we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL. We interpret the formulas of ATL and ATL over alternating transition systems. While in ordinary transition systems, each transition corresponds to a possible step of the system, in alternating transition systems, each transition corresponds to a possible move in the game between the system and the environment. Fair alternating transition systems can capture both synchronous and asynchronous compositions of open systems. For synchronous systems, the expressive power of ATL beyond CTL comes at no cost: the model-checking complexity of synchronous ATL is linear in the size of the system and the length of the formula. The symbolic model-checking algorithm for CTL extends with few modifications to synchronous ATL, and with some work, also to asynchronous ATL, whose model-checking complexity is quadratic. This makes ATL an obvious candidate for the automatic verification of open systems. In the case of ATL, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time for both synchronous and asynchronous systems.
A preliminary version of this paper appeared in the Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (FOCS 1997), pp. 100–109.},
author = {Alur, Rajeev and Thomas Henzinger and Kupferman, Orna},
pages = {23 -- 60},
publisher = {Springer},
title = {{Alternating-time temporal logic}},
doi = {10.1007/3-540-49213-5_2},
volume = {1536},
year = {1999},
}
@inproceedings{4602,
abstract = {Modular techniques for automatic verification attempt to overcome the state-explosion problem by exploiting the modular structure naturally present in many system designs. Unlike other tasks in the verification of finite-state systems, current modular techniques rely heavily on user guidance. In particular, the user is typically required to construct module abstractions that are neither too detailed as to render insufficient benefits in state exploration, nor too coarse as to invalidate the desired systemproperties. In this paper, we construct abstractmodules automatically, using reachability and controllability information about the concrete modules. This allows us to leverage automatic verification techniques by applying them in layers: first we compute on the state spaces of system components, then we use the results for constructing abstractions, and finally we compute on the abstract state space of the system. Our experimental results indicate that if reachability and controllability information is used in the construction of abstractions, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification.},
author = {Alur, Rajeev and de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {82 -- 97},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Automating modular verification}},
doi = {10.1007/3-540-48320-9_8},
volume = {1664},
year = {1999},
}
@article{4014,
abstract = {A new paradigm for designing smooth surfaces is described. A finite set of points with weights specifies a closed surface in space referred to as skin. It consists of one or more components, each tangent continuous and free of self-intersections and intersections with other components. The skin varies continuously with the weights and locations of the points, and the variation includes the possibility of a topology change facilitated by the violation of tangent continuity at a single point in space and time. Applications of the skin to molecular modeling and to geometric deformation are discussed.},
author = {Herbert Edelsbrunner},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {87 -- 115},
publisher = {Springer},
title = {{Deformable smooth surface design}},
doi = {10.1007/PL00009412},
volume = {21},
year = {1999},
}
@article{4204,
abstract = {During the development of the zebrafish nervous system both noi, a zebrafish pax2 homolog, and ace, a zebrafish fgf8 homolog, are required for development of the midbrain and cerebellum. Here we describe a dominant mutation, aussicht (aus), in which the expression of noi and ace is upregulated, In aus mutant embryos, ace is upregulated at many sites in the embryo, while Itoi expression is only upregulated in regions of the forebrain and midbrain which also express ace. Subsequent to the alterations in noi and ace expression, aus mutants exhibit defects in the differentiation of the forebrain, midbrain and eyes. Within the forebrain, the formation of the anterior and postoptic commissures is delayed and the expression of markers within the pretectal area is reduced. Within the midbrain, En and wnt1 expression is expanded. In heterozygous aus embryos, there is ectopic outgrowth of neural retina in the temporal half of the eyes, whereas in putative homozygous aus embryos, the ventral retina is reduced and the pigmented retinal epithelium is expanded towards the midline, The observation that ans mutant embryos exhibit widespread upregulation of ace raised the possibility that aus might represent an allele of the ace gene itself. However, by crossing carriers for both aus and ace, we were able to generate homozygous ace mutant embryos that also exhibited the aus phenotype, This indicated that aus is not tightly linked to ace and is unlikely to be a mutation directly affecting the ace locus. However, increased Ace activity may underly many aspects of the aus phenotype and we show that the upregulation of noi in the forebrain of aus mutants is partially dependent upon functional Ace activity. Conversely, increased ace expression in the forebrain of arcs mutants is not dependent upon functional Noi activity. We conclude that aus represents a mutation involving a locus normally required for the regulation of ace expression during embryogenesis.},
author = {Heisenberg, Carl-Philipp J and Brennan, Caroline and Wilson, Stephen},
journal = {Development},
number = {10},
pages = {2129 -- 2140},
publisher = {Company of Biologists},
title = {{Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development}},
volume = {126},
year = {1999},
}
@article{4277,
abstract = {Reproductive isolation between two taxa may be due to endogenous selection, which is generated by incompatibilities between the respective genomes, to exogenous selection, which is generated by differential adaptations to alternative environments, or to both. The continuing debate over the relative importance of either mode of selection has highlighted the need for unambiguous data on the fitness of hybrid genotypes. The hybrid zone between the fire-bellied toad (Bombina bombina) and the yellow-bellied toad (B. variegata) in central Europe involves adaptation to different environments, but evidence of hybrid dysfunction is equivocal. In this study, we followed the development under laboratory conditions of naturally laid eggs collected from a transect across the Bombina hybrid zone in Croatia. Fitness was significantly reduced in hybrid populations: Egg batches from the center of the hybrid zone showed significantly higher embryonic and larval mortality and higher frequencies of morphological abnormalities relative to either parental type. Overall mortality from day of egg collection to three weeks after hatching reached 20% in central hybrid populations, compared to 2% in pure populations. There was no significant difference in fitness between two parental types. Within hybrid populations, there was considerable variation in fitness, with some genotypes showing no evidence of reduced viability. We discuss the implications of these findings for our understanding of barriers to gene flow between species.},
author = {Kruuk, Loeske E and Gilchrist, Jason S and Nicholas Barton},
journal = {Evolution; International Journal of Organic Evolution},
number = {5},
pages = {1611 -- 1616},
publisher = {Wiley-Blackwell},
title = {{Hybrid dysfunction in fire-bellied toads (Bombina)}},
doi = {10.2307/2640907},
volume = {53},
year = {1999},
}
@article{4279,
abstract = {In this article we describe the structure of a hybrid zone in Argyll, Scotland, between native red deer (Cervus elaphus) and introduced Japanese sika deer (Cervus nippon), on the basis of a genetic analysis using 11 microsatellite markers and mitochondrial DNA. In contrast to the findings of a previous study of the same population, we conclude that the deer fall into two distinct genetic classes, corresponding to either a sika-like or red- like phenotype. Introgression is rare at any one locus, but where the taxa overlap up to 40% of deer carry apparently introgressed alleles. While most putative hybrids are heterozygous at only one locus, there are rare multiple heterozygotes, reflecting significant linkage disequilibrium within both sika- and red-like populations. The rate of backcrossing into the sika population is estimated as H = 0.002 per generation and into red, H = 0.001 per generation. On the basis of historical evidence that red deer entered Kintyre only recently, a diffusion model evaluated by maximum likelihood shows that sika have increased at ~9.2% yr-1 from low frequency and disperse at a rate of ~3.7 km yr-1. Introgression into the red-like population is greater in the south, while introgression into sika varies little along the transect. For both sika- and red-like populations, the degree of introgression is 30-40% of that predicted from the rates of current hybridization inferred from linkage disequilibria; however, in neither case is this statistically significant evidence for selection against introgression.},
author = {Goodman, Simon J and Nicholas Barton and Swanson, Graeme M and Abernethy, Kate and Pemberton, Josephine M},
journal = {Genetics},
number = {1},
pages = {355 -- 371},
publisher = {Genetics Society of America},
title = {{Introgression through rare hybridisation: A genetic study of a hybrid zone between red and sika deer (genus Cervus), in Argyll, Scotland}},
volume = {152},
year = {1999},
}
@phdthesis{4411,
abstract = {Model checking algorithms for the verification of reactive systems proceed by a systematic and exhaustive exploration of the system state space. They do not scale to large designs because of the state explosion problem --the number of states grows exponentially with the number of components in the design. Consequently, the model checking problem is PSPACE-hard in the size of the design description. This dissertation proposes three novel techniques to combat the state explosion problem.
One of the most important advances in model checking in recent years has been the discovery of symbolic methods, which use a calculus of expressions, such as binary decision diagrams, to represent the state sets encountered during state space exploration. Symbolic model checking has proved to be effective for verifying hardware designs. Traditionally, symbolic checking of temporal logic specifications is performed by backward fixpoint reasoning with the operator Pre. Backward reasoning can be wasteful since unreachable states are explored. We suggest the use of forward fixpoint reasoning based on the operator Post. We show how all linear temporal logic specifications can be model checked symbolically by forward reasoning. In contrast to backward reasoning, forward reasoning performs computations only on the reachable states.
Heuristics that improve algorithms for application domains, such as symbolic methods for hardware designs, are useful but not enough to make model checking feasible on industrial designs. Currently, exhaustive state exploration is possible only on designs with about 50-100 boolean state variables. Assume-guarantee verification attempts to combat the state explosion problem by using the principle of "divide and conquer," where the components of the implementation are analyzed one at a time. Typically, an implementation component refines its specification only when its inputs are suitably constrained by other components in the implementation. The assume-guarantee principle states that instead of constraining the inputs by implementation components, it is sound to constrain them by the corresponding specification components, which can be significantly smaller. We extend the assume-guarantee proof rule to deal with the case where the specification operates at a coarser time scale than the implementation. Using our model checker Mocha, which implements this methodology, we verify VGI, a parallel DSP processor chip with 64 compute processors each containing approximately 800 state variables and 30K gates.
Our third contribution is a systematic model checking methodology for verifying the abstract shared-memory interface of sequential consistency on multiprocessor systems with three parameters --number of processors, number of memory locations, and number of data values. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at different processors be a trace of serial memory. Therefore, it suffices to construct a non-interfering serializer that watches and reorders read/write events so that a trace of serial memory is obtained. While in general such a serializer must be unbounded even for fixed values of the parameters --checking sequential consistency is undecidable!-- we show that the paradigmatic class of snoopy cache coherence protocols has finite-state serializers. In order to reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop a novel framework for induction over the number of processors and use the notion of a serializer to reduce the problem of verifying sequential consistency to that of checking language inclusion between finite state machines.},
author = {Qadeer, Shaz},
pages = {1 -- 150},
publisher = {University of California, Berkeley},
title = {{Algorithms and Methodology for Scalable Model Checking}},
year = {1999},
}
@article{4442,
abstract = {Rectangular hybrid automata model digital control programs of analog plant environments. We study rectangular hybrid automata where the plant state evolves continuously in real-numbered time, and the controller samples the plant state and changes the control state discretely, only at the integer points in time. We prove that rectangular hybrid automata have finite bisimilarity quotients when all control transitions happen at integer times, even if the constraints on the derivatives of the variables vary between control states. This is in contrast with the conventional model where control transitions may happen at any real time, and already the reachability problem is undecidable. Based on the finite bisimilarity quotients, we give an exponential algorithm for the symbolic sampling-controller synthesis of rectangular automata. We show our algorithm to be optimal by proving the problem to be EXPTIME-hard. We also show that rectangular automata form a maximal class of systems for which the sampling-controller synthesis problem can be solved algorithmically.},
author = {Thomas Henzinger and Kopke, Peter W},
journal = {Theoretical Computer Science},
number = {1-2},
pages = {369 -- 392},
publisher = {Elsevier},
title = {{Discrete-time control for rectangular hybrid automata}},
doi = {10.1016/S0304-3975(99)00038-9},
volume = {221},
year = {1999},
}
@inproceedings{4480,
abstract = {We describe the formal specification and verification of the VGI parallel DSP chip [1], which contains 64 compute processors with ~30K gates in each processor. Our effort coincided in time with the “informal” verification stage of the chip. By interacting with the designers, we produced an abstract but executable specification of the design which embodies the programmer's view of the system. Given the size of the design, an automatic check that even one of the 64 processors satisfies its specification is well beyond the scope of current verification tools. However, the check can be decomposed using assume-guarantee reasoning. For VGI, the implementation and specification operate at different time scales: several steps of the implementation correspond to a single step in the specification. We generalized both the assume-guarantee method and our model checker MOCHA to allow compositional verification for such applications. We used our proof rule to decompose the verification problem of the VGI chip into smaller proof obligations that were discharged automatically by MOCHA. Using our formal approach, we uncovered and fixed subtle bugs that were unknown to the designers.},
author = {Thomas Henzinger and Liu, Xiaojun and Qadeer,Shaz and Rajamani, Sriram K},
pages = {494 -- 499},
publisher = {IEEE},
title = {{Formal specification and verification of a dataflow processor array}},
year = {1999},
}
@inproceedings{4484,
abstract = {In shared-memory multiprocessors sequential consistency offers a natural tradeoff between the flexibility afforded to the implementor and the complexity of the programmer’s view of the memory. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at different processors be a trace of serial memory. We develop a systematic methodology for proving sequential consistency for memory systems with three parameters —number of processors, number of memory locations, and number of data values. From the definition of sequential consistency it suffices to construct a non-interfering observer that watches and reorders read/write events so that a trace of serial memory is obtained. While in general such an observer must be unbounded even for fixed values of the parameters —checking sequential consistency is undecidable!— we show that for two paradigmatic protocol classes—lazy caching and snoopy cache coherence—there exist finite-state observers. In these cases, sequential consistency for fixed parameter values can thus be checked by language inclusion between finite automata.
In order to reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop a novel framework for induction over the number of processors. Classical induction schemas, which are based on process invariants that are inductive with respect to an implementation preorder that preserves the temporal sequence of events, are inadequate for our purposes, because proving sequential consistency requires the reordering of events. Hence we introduce merge invariants, which permit certain reorderings of read/write events. We show that under certain reasonable assumptions about the memory system, it is possible to conclude sequential consistency for any number of processors, memory locations, and data values by model checking two finite-state lemmas about process and merge invariants: they involve two processors each accessing a maximum of three locations, where each location stores at most two data values. For both lazy caching and snoopy cache coherence we are able to discharge the two lemmas using the model checker MOCHA.},
author = {Thomas Henzinger and Qadeer,Shaz and Rajamani, Sriram K},
pages = {301 -- 315},
publisher = {Springer},
title = {{Verifying sequential consistency on shared-memory multiprocessor systems}},
doi = {10.1007/3-540-48683-6_27},
volume = {1633},
year = {1999},
}
@inproceedings{4485,
abstract = {In order to study control problems for hybrid systems, we generalize hybrid automata to hybrid games —say, controller vs. plant. If we specify the continuous dynamics by constant lower and upper bounds, we obtain rectangular games. We show that for rectangular games with objectives expressed in Ltl (linear temporal logic), the winning states for each player can be computed, and winning strategies can be synthesized. Our result is sharp, as already reachability is undecidable for generalizations of rectangular systems, and optimal —singly exponential in the size of the game structure and doubly exponential in the size of the Ltl objective. Our proof systematically generalizes the theory of hybrid systems from automata (single-player structures) [9] to games (multi-player structures): we show that the successively more general infinite-state classes of timed, 2D rectangular, and rectangular games induce successively weaker, but still finite, quotient structures called game bisimilarity, game similarity, and game trace equivalence. These quotients can be used, in particular, to solve the Ltl control problem.},
author = {Thomas Henzinger and Horowitz, Benjamin and Majumdar, Ritankar S},
pages = {320 -- 335},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Rectangular hybrid games}},
doi = {10.1007/3-540-48320-9_23},
volume = {1664},
year = {1999},
}
@inproceedings{4487,
abstract = {Refinement checking is used to verify implementations against more abstract specifications. Assume-guarantee reasoning is used to decompose refinement proofs in order to avoid state-space explosion. In previous approaches, specifications are forced to operate on the same time scale as the implementation. This may lead to unnatural specifications and inefficiencies in verification. We introduce a novel methodology for decomposing refinement proofs of temporally abstract specifications, which specify implementation requirements only at certain sampling instances in time. Our new assume-guarantee rule allows separate refinement maps for specifying functionality and timing.We present the theory for the correctness of our methodology, and illustrate it using a simple example. Support for sampling and the generalized assume-guarantee rule have been implemented in the model checker Mocha and successfully applied to verify the VGI multiprocessor dataflow chip with 6 million transistors.},
author = {Thomas Henzinger and Qadeer,Shaz and Rajamani, Sriram K},
pages = {208 -- 221},
publisher = {Springer},
title = {{Assume-guarantee refinement between different time scales}},
doi = {10.1007/3-540-48683-6_20},
volume = {1633},
year = {1999},
}
@article{4582,
abstract = {We present a formal model for concurrent systems. The model represents synchronous and asynchronous components in a uniform framework that supports compositional (assume-guarantee) and hierarchical (stepwise-refinement) design and verification. While synchronous models are based on a notion of atomic computation step, and asynchronous models remove that notion by introducing stuttering, our model is based on a flexible notion of what constitutes a computation step: by applying an abstraction operator to a system, arbitrarily many consecutive steps can be collapsed into a single step. The abstraction operator, which may turn an asynchronous system into a synchronous one, allows us to describe systems at various levels of temporal detail. For describing systems at various levels of spatial detail, we use a hiding operator that may turn a synchronous system into an asynchronous one. We illustrate the model with diverse examples from synchronous circuits, asynchronous shared-memory programs, and synchronous message-passing protocols.
},
author = {Alur, Rajeev and Thomas Henzinger},
journal = {Formal Methods in System Design},
number = {1},
pages = {7 -- 48},
publisher = {Springer},
title = {{Reactive modules}},
doi = {10.1023/A:1008739929481},
volume = {15},
year = {1999},
}
@book{3137,
abstract = {This volume provides an overview of glutamate receptors and their role in excitatory neurotransmission. It focusses on three aspects. First, it describes the functional, molecular, and pharmacological properties of glutamate receptors (AMPA, NMDA, and kainate receptors). Second, it gives a survey how these receptors are involved in synaptic transmission at different glutamatergic synapses in the mammalian CNS. Finally, it adresses how overactivation of glutamate receptors can lead to excitotoxic cell death, and emphasizes the importance of glutamate receptors as potential therapeutical targets. The chapters, written by leading scientists, give accurate summaries of facets that have emerged recently in this field. The book demonstrates the strength of a multidisciplinary approach involving physiology, pharmacology, and molecular biology. It will be useful for other scientists in and outside the field, lecturers and students at different educational levels.},
editor = {Peter Jonas and Monyer, Hannah},
publisher = {Springer},
title = {{Ionotropic Glutamate Receptors in the CNS}},
volume = {141},
year = {1999},
}
@article{3148,
abstract = {Accurate proteolytic processing of neuropeptide and peptide hormone precursors by members of the kexin/furin family of proteases is key to determining both the identities and activities of signaling peptides. Here we identify amontillado (amon), the Drosophila melanogaster homolog of the mammalian neuropeptide processing protease PC2, and show that in contrast to vertebrate PC2, amontillado expression undergoes extensive regulation in the nervous system during development. In situ hybridization reveals that expression of amontillado is restricted to the final stages of embryogenesis when it is found in anterior sensory structures and in only 168 cells in the brain and ventral nerve cord. After larvae hatch from their egg shells, the sensory structures and most cells in the CNS turn off or substantially reduce amontillado expression, suggesting that amontillado plays a specific role late in embryogenesis. Larvae lacking the chromosomal region containing amontillado show no gross anatomical defects and respond to touch. However, such larvae show a greatly reduced frequency of a hatching behavior of wild- type Drosophila in which larvae swing their heads, scraping through the eggshell with their mouth hooks. Ubiquitous expression of amontillado can restore near wild-type levels of this behavior, whereas expression of amontillado with an alanine substitution for the catalytic histidine cannot. These results suggest that amontillado expression is regulated as part of a programmed modulation of neural signaling that controls hatching behavior by producing specific neuropeptides in particular neurons at an appropriate developmental time.},
author = {Daria Siekhaus and Fuller, Robert S},
journal = {Journal of Neuroscience},
number = {16},
pages = {6942 -- 6954},
publisher = {Society for Neuroscience},
title = {{A role for amontillado the Drosophila homolog of the neuropeptide precursor processing protease PC2 in triggering hatching behavior}},
volume = {19},
year = {1999},
}
@article{3444,
abstract = {This study examined intermittent, high-frequency (100-200 Hz) oscillatory patterns in the CA1 region of the hippocampus in the absence of theta activity, i.e., during and in between sharp wave (SPW) bursts. Pyramidal and interneuronal activity was phase-locked not only to large amplitude (>7 SD from baseline) oscillatory events, which are present mainly during SPWs, but to smaller amplitude (<4 SD) patterns, as well. Large-amplitude events were in the 140-200 Hz, "ripple" frequency range. Lower-amplitude events, however, contained slower, 100-130 Hz ("slow") oscillatory patterns. Fast ripple waves reversed just below the CA1 pyramidal layer, whereas slow oscillatory potentials reversed in the stratum radiatum and/or in the stratum oriens. Parallel CA1-CA3 recordings revealed correlated CA3 field and unit activity to the slow CA1 waves but not to fast ripple waves. These findings suggest that fast ripples emerge in the CA1 region, whereas slow (100-130 Hz) oscillatory patterns are generated in the CA3 region and transferred to the CA1 field.},
author = {Jozsef Csicsvari and Hirase, Hajima and Czurkó, András and Mamiya, Akira and Buzsáki, György},
journal = {Journal of Neuroscience},
number = {16},
publisher = {Society for Neuroscience},
title = {{Fast network oscillations in the hippocampal CA1 region of the behaving rat}},
volume = {19},
year = {1999},
}
@article{3445,
abstract = {The medial septal region and the hippocampus are connected reciprocally via GABAergic neurons, but the physiological role of this loop is still not well understood. In an attempt to reveal the physiological effects of the hippocamposeptal GABAergic projection, we cross-correlated hippocampal sharp wave (SPW) ripples or theta activity and extracellular units recorded in the medial septum and diagonal band of Broca (MSDB) in freely moving rats. The majority of single MSDB cells (60%) were significantly suppressed during SPWs. Most cells inhibited during SPW (80%) fired rhythmically and phase-locked to the negative peak of the CA1 pyramidal layer theta waves. Because both SPW and the negative peak of local theta waves correspond to the maximum discharge probability of CA1 pyramidal cells and interneuron classes, the findings indicate that the activity of medial septal neurons can be negatively (during SPW) or positively (during theta waves) correlated with the activity of hippocampal interneurons. We hypothesize that the functional coupling between medial septal neurons and hippocampal interneurons varies in a state-dependent manner.},
author = {Dragoi, George and Carpi, Daniel and Recce, Michael and Jozsef Csicsvari and Buzsáki, György},
journal = {Journal of Neuroscience},
number = {14},
pages = {6191 -- 6199},
publisher = {Society for Neuroscience},
title = {{Hippocampomedial septal interactions during sharp waves and theta oscillation in the behaving rat}},
volume = {19},
year = {1999},
}
@inbook{3456,
author = {Monyer, Hannah and Peter Jonas and Rossier, Jean},
booktitle = {Ionotropic Glutamate Receptors in the CNS},
editor = {Peter Jonas and Monyer, Hannah},
pages = {309 -- 339},
publisher = {Springer},
title = {{Molecular determinants controlling functional properties of AMPARs and NMDARs in the mammalian CNS}},
doi = {10.1007/978-3-662-08022-1_9},
volume = {141},
year = {1999},
}
@inbook{3457,
author = {Geiger, Jörg R and Roth, Arnd and Taskin, Birol and Peter Jonas},
booktitle = {Ionotropic Glutamate Receptors in the CNS},
editor = {Monyer, Hannah and Peter Jonas},
pages = {363 -- 398},
publisher = {Springer},
title = {{Glutamate-mediated synaptic excitation of cortical interneurons}},
doi = {10.1007/978-3-662-08022-1_11},
volume = {141},
year = {1999},
}
@article{3515,
abstract = {Oscillations in neuronal networks are assumed to serve various physiological functions, from coordination of motor patterns to perceptual binding of sensory information. Here, we describe an ultra-slow oscillation (0.025 Hz) in the hippocampus. Extracellular and intracellular activity was recorded from the CA1 and subicular regions in rats of the Wistar and Sprague-Dawley strains. anesthetized with urethane. in a subgroup of Wistar rats (23%), spontaneous afterdischarges (4.7 +/- 1.6 s) occurred regularly at 40.8 +/- 15.7 s. The afterdischarge was initiated by a fast increase of population synchrony (100-250 Hz oscillation; “tonic” phase), followed by large-amplitude rhythmic waves and associated action potentials at gamma and beta frequency (15-50 Hz; “clonic” phase). The afterdischarges were bilaterally synchronous and terminated relatively abruptly without post-ictal depression. Single-pulse stimulation of the commissural input could trigger afterdischarges, but only at times when they were about to occur. Commissural stimulation evoked inhibitory postsynaptic potentials in pyramidal cells. However, when the stimulus triggered an afterdischarge, the inhibitory postsynaptic potential was absent and the cells remained depolarized during most of the afterdischarge. Afterdischarges were not observed in the Sprague-Dawley rats. Long-term analysis of interneuronal activity in intact, drug-free rats also revealed periodic excitability changes in the hippocampal network at 0.025 Hz. These findings indicate the presence of an ultra-slow oscillation in the hippocampal formation. The ultra-slow clock induced afterdischarges in susceptible animals. We hypothesize that a transient failure of GABAergic inhibition in a subset of Wistar rats is responsible for the emergence of epileptiform patterns. (C) 1999 IBRO. Published by Elsevier Science Ltd.},
author = {Penttonen, Markku and Nurminen, Nina and Miettinen, Riitta A. and Sirviö, Jouni and Henze, Darrell A and Jozsef Csicsvari and Buzsáki, György},
journal = {Neuroscience},
number = {3},
pages = {735 -- 743},
publisher = {Elsevier},
title = {{Ultra-slow oscillation (0.025 Hz) triggers hippocampal afterdischarges in Wistar rats}},
doi = {10.1016/S0306-4522(99)00367-X},
volume = {94},
year = {1999},
}
@article{3518,
abstract = {Information in neuronal networks may be represented by the spatiotemporal patterns of spikes. Here we examined the temporal coordination of pyramidal cell spikes in the rat hippocampus during slow-wave sleep. In addition, rats were trained to run in a defined position in space (running wheel) to activate a selected group of pyramidal cells. A template-matching method and a joint probability map method were used for sequence search. Repeating spike sequences in excess of chance occurrence were examined by comparing the number of repeating sequences in the original spike trains and in surrogate trains after Monte Carlo shuffling of the spikes. Four different shuffling procedures were used to control for the population dynamics of hippocampal neurons. Repeating spike sequences in the recorded cell assemblies were present in both the awake and sleeping animal in excess of what might be predicted by random variations. Spike sequences observed during wheel running were “replayed” at a faster timescale during single sharp-wave bursts of slow-wave sleep. We hypothesize that the endogenously expressed spike sequences during sleep reflect reactivation of the circuitry modified by previous experience. Reactivation of acquired sequences may serve to consolidate information.},
author = {Nádasdy, Zoltán and Hirase, Hajima and Czurkó, András and Jozsef Csicsvari and Buzsáki, György},
journal = {Journal of Neuroscience},
number = {21},
pages = {9497 -- 9507},
publisher = {Society for Neuroscience},
title = {{Replay and time compression of recurring spike sequences in the hippocampus}},
volume = {19},
year = {1999},
}
@article{3519,
abstract = {In contrast to sensory cortical areas of the brain, the relevant physiological inputs to the hippocampus, leading to selective activation of pyramidal cells, are largely unknown. Pyramidal cells are thought to be phasically activated by spatial cues and a variety of sensory and motor stimuli. Here, we used a behavioural `space clamp' method, which involved the confinement of the actively running animal in a defined position in space (running wheel) and kept sensory inputs constant. Twelve percent of the recorded CA1 pyramidal cells were selectively active while the rat was running in the wheel. Cell firing was specific to the direction of running and disappeared after rotating the recording apparatus. The discharge frequency of pyramidal cells and interneurons was sustained as long as the rat ran continuously in the wheel. Furthermore, the discharge frequency of pyramidal cells and interneurons increased with increasing running velocity, even though the frequency of hippocampal theta waves remained constant. The discharge frequency of some `wheel-related' pyramidal cells could increase more than 10-fold between 10 and 100 cm/s, whereas the firing rate of `non-wheel' cells remained constantly low. We hypothesize that: (i) a necessary condition for place-specific discharge of hippocampal pyramidal cells is the presence of theta oscillation; and (ii) relevant stimuli can tonically and selectively activate hippocampal pyramidal cells as long as theta activity is present.},
author = {Czurkó, András and Hirase, Hajima and Jozsef Csicsvari and Buzsáki, György},
journal = {European Journal of Neuroscience},
number = {1},
pages = {344 -- 352},
publisher = {Wiley-Blackwell},
title = {{Sustained activation of hippocampal pyramidal cells by ‘space clamping' in a running wheel}},
doi = {10.1046/j.1460-9568.1999.00446.x},
volume = {11},
year = {1999},
}
@article{3524,
abstract = {We examined whether excitation and inhibition are balanced in hippocampal cortical networks. Extracellular field and single-unit activity were recorded by multiple tetrodes and multisite silicon probes to reveal the timing of the activity of hippocampal CAI pyramidal cells and classes of interneurons during theta waves and sharp wave burst (SPW)-associated field ripples. The somatic and dendritic inhibition of pyramidal cells was deduced from the activity of interneurons in the pyramidal layer [int(p)] and in the alveus and st. oriens [int(a/o)], respectively. int(p) and int(a/o) discharged an average of 60 and 20 degrees before the population discharge of pyramidal cells during the theta cycle, respectively. SPW ripples were associated with a 2.5-fold net increase of excitation. The discharge frequency of int(a/o) increased, decreased (”anti-SPW” cells), or did not change (”SPW-independent” cells) during SPW suggesting that not all interneurons are innervated by pyramidal cells. Int(p) either fired together with (unimodal cells) or both before and after (bimodal cells) the pyramidal cell burst. During fast-ripple oscillation, the activity of interneurons in both the int(p) and int(a/o) groups lagged the maximum discharge probability of pyramidal neurons by 1-2 msec. Network state changes, as reflected by field activity, covaried with changes in the spike train dynamics of single cells and their interactions. Summed activity of parallel-recorded interneurons, but not of pyramidal cells, reliably predicted theta cycles, whereas the reverse was true for the ripple cycles of SPWs. We suggest that network-driven excitability changes provide temporal windows of opportunity for single pyramidal cells to suppress, enable, or facilitate selective synaptic inputs.},
author = {Jozsef Csicsvari and Hirase, Hajima and Czurkó, András and Mamiya, Akira and Buzsáki, György},
journal = {Journal of Neuroscience},
number = {1},
pages = {274 -- 287},
publisher = {Society for Neuroscience},
title = {{Oscillatory coupling of hippocampal pyramidal cells and interneurons in the behaving rat}},
volume = {19},
year = {1999},
}
@article{3531,
abstract = {The medial septal region and the hippocampus are connected reciprocally via GABAergic neurons, but the physiological role of this loop is still not well understood. In an attempt to reveal the physiological effects of the hippocamposeptal GABAergic projection, we cross-correlated hippocampal sharp wave (SPW) ripples or theta activity and extracellular units recorded in the medial septum and diagonal band of Broca (MSDB) in freely moving rats. The majority of single MSDB cells (60%) were significantly suppressed during SPWs. Most cells inhibited during SPW (80%) fired rhythmically and phase-locked to the negative peak of the CA1 pyramidal layer theta waves. Because both SPW and the negative peak of local theta waves correspond to the maximum discharge probability of CA1 pyramidal cells and interneuron classes, the findings indicate that the activity of medial septal neurons can be negatively (during SPW) or positively (during theta waves) correlated with the activity of hippocampal interneurons. We hypothesize that the functional coupling between medial septal neurons and hippocampal interneurons varies in a state-dependent manner.},
author = {Dragoi, George and Carpi, Daniel and Recce, Michael and Jozsef Csicsvari and Buzsáki, György},
journal = {Journal of Neuroscience},
number = {14},
pages = {6191 -- 6199},
publisher = {Society for Neuroscience},
title = {{Interactions between hippocampus and medial septum during sharp waves and theta oscillation in the behaving rat}},
volume = {19},
year = {1999},
}
@article{3539,
abstract = {In the hippocampus, spatial representation of the environment has been suggested to be coded by either the firing rate of pyramidal cell assemblies or the relative timing of the action potentials during the theta EEG cycle. Here, we used a behavioural `space clamp' method, which involved the confinement of the actively running animal in a defined position in space (running wheel) to examine how `spatial' and other inputs affect firing rate and timing of hippocampal CA1 pyramidal cells and interneurons. Nineteen per cent of the recorded CA1 pyramidal cells were selectively active while the rat was running in the wheel in a given direction ('wheel' cells). Spatial rotation of the apparatus showed that selective discharge of pyramidal cells in the wheel was under the combined influence of distal and apparatus cues. During steady running, both discharge rate and theta phase were constant. Rotation of the wheel apparatus resulted in a shift of both firing rate and preferred theta phase. The discharge frequency of `wheel' cells increased threefold (on average) with increasing running velocity. In contrast, change in running speed had relatively little effect on the theta phase-related discharge of `wheel' cells. Our findings indicate that mechanisms that regulate rate and phase of spikes are overlapping but not necessarily identical.},
author = {Hirase, Hajima and Czurkó, András and Jozsef Csicsvari and Buzsáki, György},
journal = {European Journal of Neuroscience},
number = {12},
pages = {4373 -- 4380},
publisher = {Wiley-Blackwell},
title = {{Firing rate and theta-phase coding by hippocampal pyramidal neurons during ‘space clamping’}},
doi = {10.1046/j.1460-9568.1999.00853.x},
volume = {11},
year = {1999},
}
@inproceedings{3554,
abstract = {In computational simulation of coupled, multicomponent systems, it is frequently necessary to transfer data between meshes that may differ in resolution, structure, and discretization methodology. Typically, nodes from one mesh must be associated with elements of another mesh. In this paper, we formulate mesh association as a geometric problem and introduce two efficient mesh association algorithms. One of these algorithms requires linear time in the worst case if the meshes are well shaped and geometrically well aligned. Our formulation of the problem and our algorithms are more general than previous work and can be applied to surface meshes with curved elements.},
author = {Jiao, Xiangmin and Herbert Edelsbrunner and Heath, Michael T},
pages = {75 -- 82},
publisher = {Elsevier},
title = {{Mesh association: formulation and algorithms}},
year = {1999},
}
@inbook{3571,
author = {Dey, Tamal K and Herbert Edelsbrunner and Guha, Sumanta},
booktitle = {Advances in Discrete and Computational Geometry},
pages = {109 -- 143},
publisher = {American Mathematical Society},
title = {{Computational topology}},
volume = {223},
year = {1999},
}
@article{3582,
abstract = {We study edge contractions in simplicial complexes and local conditions under which they preserve the topological type. The conditions are based on a generalized notion of boundary, which lends itself to defining a nested hierarchy of triangulable spaces measuring the distance to being a manifold.},
author = {Dey, Tamal K and Herbert Edelsbrunner and Guha, Sumanta and Nekhayev, Dmitry V},
journal = {Publications de l'Institut Mathématique},
pages = {23 -- 45},
publisher = {Jugostampa},
title = {{Topology preserving edge contraction}},
volume = {66},
year = {1999},
}
@article{3625,
abstract = {This article outlines theoretical models of clines in additive polygenic traits, which are maintained by stabilizing selection towards a spatially varying optimum. Clines in the trait mean can be accurately predicted, given knowledge of the genetic variance. However, predicting the variance is difficult, because it depends on genetic details. Changes in genetic variance arise from changes in allele frequency, and in linkage disequilibria. Allele frequency changes dominate when selection is weak relative to recombination, and when there are a moderate number of loci. With a continuum of alleles, gene flow inflates the genetic variance in the same way as a source of mutations of small effect. The variance can be approximated by assuming a Gaussian distribution of allelic effects; with a sufficiently steep cline, this is accurate even when mutation and selection alone are better described by the 'House of Cards' approximation. With just two alleles at each locus, the phenotype changes in a similar way: the mean remains close to the optimum, while the variance changes more slowly, and over a wider region. However, there may be substantial cryptic divergence at the underlying loci. With strong selection and many loci, linkage disequilibria are the main cause of changes in genetic variance. Even for strong selection, the infinitesimal model can be closely approximated by assuming a Gaussian distribution of breeding values. Linkage disequilibria can generate a substantial increase in genetic variance, which is concentrated at sharp gradients in trait means.},
author = {Nicholas Barton},
journal = {Genetical Research},
number = {3},
pages = {223 -- 236},
publisher = {Cambridge University Press},
title = {{Clines in polygenic traits}},
doi = {10.1017/S001667239900422X},
volume = {74},
year = {1999},
}
@article{3626,
abstract = {There has recently been considerable debate over the relative importance of selection against hybrids ("endogenous" selection) vs. adaptation to different environments ("exogenous") in maintaining stable hybrid zones and hence in speciation. Single-locus models of endogenous and exogenous viability selection generate clines of similar shape, but the comparison has not been extended to multilocus systems, which are both quantitatively and qualitatively very different from the single-locus case. Here we develop an analytical multilocus model of differential adaptation across an environmental transition and compare it to previous heterozygote disadvantage models. We show that the shape of clines generated by exogenous selection is indistinguishable from that generated by endogenous selection. A stochastic simulation model is used to test the robustness of the analytical description to the effects of drift and strong selection, and confirms the prediction that pairwise linkage disequilibria are predominantly generated by migration. However, although analytical predictions for the width of clines maintained by heterozygote disadvantage fit well with the simulation results, those for environmental adaptation are consistently too narrow; reasons for the discrepancy are discussed. There is a smooth transition between a system in which a set of loci effectively act independently of each other and one in which they act as a single nonrecombining unit.},
author = {Kruuk, Loeske E and Baird, Stuart J and Gale, Katherine S and Nicholas Barton},
journal = {Genetics},
number = {4},
pages = {1959 -- 1971},
publisher = {Genetics Society of America},
title = {{A comparison of multilocus clines maintained by environmental adaptation or by selection against hybrids}},
volume = {153},
year = {1999},
}
@article{2583,
abstract = {Substance P receptor (SPR)-immunoreactive neurons projecting to the periaqueductal gray (PAG) were examined in the rat spinal trigeminal nucleus and spinal cord by a retrograde tracing method combined with immunofluorescence histochemistry. After injection of Fluoro-gold (FG) into the PAG, SPR-immunoreactive neurons labeled with FG were observed mainly in the lateral spinal nucleus and lamina I of the medullary and spinal dorsal horns and additionally in laminae V and X of the spinal cord.},
author = {Li, Jin-Lian and Ding, Yu-Qiang and Xiong, Kang-Hui and Li, Ji-Shuo and Ryuichi Shigemoto and Mizuno, Noboru},
journal = {Neuroscience Research},
number = {3},
pages = {219 -- 225},
publisher = {Elsevier},
title = {{Substance P receptor (NK1)-immunoreactive neurons projecting to the periaqueductal gray: Distribution in the spinal trigeminal nucleus and the spinal cord of the rat}},
doi = {10.1016/S0168-0102(97)00132-6},
volume = {30},
year = {1998},
}