@inproceedings{3447,
author = {Krishnendu Chatterjee and Dasgupta, Pallab and Chakrabarti, Partha P},
publisher = {Elsevier},
title = {{Weighted quantified computation tree logic}},
year = {2001},
}
@article{3493,
abstract = {Although agonists and competitive antagonists presumably occupy overlapping binding sites on ligand-gated channels, these interactions cannot be identical because agonists cause channel opening whereas antagonists do not. One explanation is that only agonist binding performs enough work on the receptor to cause the conformational changes that lead to gating. This idea is supported by agonist binding rates at GABAA and nicotinic acetylcholine receptors that are slower than expected for a diffusion-limited process, suggesting that agonist binding involves an energy-requiring event. This hypothesis predicts that competitive antagonist binding should require less activation energy than agonist binding. To test this idea, we developed a novel deconvolution-based method to compare binding and unbinding kinetics of GABAA receptor agonists and antagonists in outside-out patches from rat hippocampal neurons. Agonist and antagonist unbinding rates were steeply correlated with affinity. Unlike the agonists, three of the four antagonists tested had binding rates that were fast, independent of affinity, and could be accounted for by diffusion- and dehydration-limited processes. In contrast, agonist binding involved additional energy-requiring steps, consistent with the idea that channel gating is initiated by agonist-triggered movements within the ligand binding site. Antagonist binding does not appear to produce such movements, and may in fact prevent them.},
author = {Jones, M.V . and Peter Jonas and Sahara, Y. and Westbrook, G. L.},
journal = {Biophysical Journal},
number = {5},
pages = {2660 -- 2670},
publisher = {Biophysical Society},
title = {{Microscopic kinetics and energetics distinguish GABAA receptor agonists from antagonists}},
doi = {10.1016/S0006-3495(01)75909-7 },
volume = {81},
year = {2001},
}
@article{3494,
abstract = {Mutual synaptic interactions between GABAergic interneurons are thought to be of critical importance for the generation of network oscillations and for temporal encoding of information in the hippocampus. However, the functional properties of synaptic transmission between hippocampal interneurons are largely unknown. We have made paired recordings from basket cells (BCs) in the dentate gyrus of rat hippocampal slices, followed by correlated light and electron microscopical analysis. Unitary GABAAreceptor-mediated IPSCs at BC–BC synapses recorded at the soma showed a fast rise and decay, with a mean decay time constant of 2.5 ± 0.2 msec (32°C). Synaptic transmission at BC–BC synapses showed paired-pulse depression (PPD) (32 ± 5% for 10 msec interpulse intervals) and multiple-pulse depression during repetitive stimulation. Detailed passive cable model simulations based on somatodendritic morphology and localization of synaptic contacts further indicated that the conductance change at the postsynaptic site was even faster, decaying with a mean time constant of 1.8 ± 0.6 msec. Sequential triple recordings revealed that the decay time course of IPSCs at BC–BC synapses was approximately twofold faster than that at BC–granule cell synapses, whereas the extent of PPD was comparable. To examine the consequences of the fast postsynaptic conductance change for the generation of oscillatory activity, we developed a computational model of an interneuron network. The model showed robust oscillations at frequencies >60 Hz if the excitatory drive was sufficiently large. Thus the fast conductance change at interneuron–interneuron synapses may promote the generation of high-frequency oscillations observed in the dentate gyrusin vivo. },
author = {Bartos, Marlene and Vida, Imre and Frotscher, Michael and Geiger, Jörg R and Peter Jonas},
journal = {Journal of Neuroscience},
number = {8},
pages = {2687 -- 2698},
publisher = {Society for Neuroscience},
title = {{Rapid signaling at inhibitory synapses in a dentate gyrus interneuron network.}},
volume = {21},
year = {2001},
}
@article{3495,
abstract = {High Ca2+ permeability and its control by voltage-dependent Mg2+ block are defining features of NMDA receptors. These features are lost if the principal NR1 subunit carries an asparagine (N) to arginine (R) substitution in a critical channel site at NR1 position 598. NR1(R) expression from a single allele in gene-targeted NR1+/R mice is lethal soon after birth, precluding analysis of altered synaptic functions later in life. We therefore employed the forebrain specific αCaMKII promoter to drive tTA-mediated tetracyclin sensitive transcription of transgenes for NR1(R) and for lacZ as reporter. Transgene expression was observed in cortex, striatum, hippocampus, amygdala and olfactory bulb and was mosaic in all these forebrain regions. It was highest in olfactory bulb granule cells, in most of which Ca2+ permeability and voltage-dependent Mg2+ block of NMDA receptors were reduced to different extents. This indicates significant impairment of NMDA receptor function by NR1(R) in presence of the wild-type NR1 complement. Indeed, even though NR1(R) mRNA constituted only 18% of the entire NR1 mRNA population in forebrain, the transgenic mice died during adolescence unless transgene expression was suppressed by doxycycline. Thus, glutamate receptor function can be altered in the mouse by regulated NR1(R) transgene expression.},
author = {Jerecic, Jasna and Schulze, Christian H and Peter Jonas and Sprengel, Rolf and Seeburg, Peter H and Bischofberger, Joseph},
journal = {Molecular brain research},
number = {1-2},
pages = {96 -- 104},
publisher = {Elsevier},
title = {{Impaired NMDA receptor function in mouse olfactory bulb neurons by tetracycline-sensitive NR1 (N598R) expression}},
doi = {10.1016/S0169-328X(01)00221-2},
volume = {94},
year = {2001},
}
@article{3496,
abstract = {The mossy fiber-CA3 pyramidal neuron synapse is a main component of the hippocampal trisynaptic circuitry. Recent studies, however, suggested that inhibitory interneurons are the major targets of the mossy fiber system. To study the regulation of mossy fiber-interneuron excitation, we examined unitary and compound excitatory postsynaptic currents in dentate gyrus basket cells, evoked by paired recording between granule and basket cells or extracellular stimulation of mossy fiber collaterals. The application of an associative high-frequency stimulation paradigm induced posttetanic potentiation (PTP) followed by homosynaptic long-term potentiation (LTP). Analysis of numbers of failures, coefficient of variation, and paired-pulse modulation indicated that both PTP and LTP were expressed presynaptically. The Ca2+ chelator 1,2-bis(2-aminophenoxy)ethane-N,N,N′,N′-tetraacetic acid (BAPTA) did not affect PTP or LTP at a concentration of 10 mM but attenuated LTP at a concentration of 30 mM. Both forskolin, an adenylyl cyclase activator, and phorbolester diacetate, a protein kinase C stimulator, lead to a long-lasting increase in excitatory postsynaptic current amplitude. H-89, a protein kinase A inhibitor, and bisindolylmaleimide, a protein kinase C antagonist, reduced PTP, whereas only bisindolylmaleimide reduced LTP. These results may suggest a differential contribution of protein kinase A and C pathways to mossy fiber-interneuron plasticity. Interneuron PTP and LTP may provide mechanisms to maintain the balance between synaptic excitation of interneurons and that of principal neurons in the dentate gyrus-CA3 network. },
author = {Alle, Henrik and Peter Jonas and Geiger, Jörg R},
journal = {PNAS},
number = {25},
pages = {14708 -- 14713},
publisher = {National Academy of Sciences},
title = {{PTP and LTP at a hippocampal mossy fiber-interneuron synapse}},
doi = {10.1073/pnas.251610898 },
volume = {98},
year = {2001},
}
@misc{3507,
abstract = {A molecular classification method is based on a space filling description of a molecule. The three dimensional body corresponding to the space filling molecular structure is divided into Voronoi regions to provide a basis for efficiently processing local structural information. A Delaunay triangulation provides a basis for systematically processing information relating to the Voronoi regions into shape descriptors in the form of topological elements. Preferably, additional shape and/or property descriptors are included in the classification method. The classification methods generally are used to identify similarities between molecules that can be used as property predictors for a variety of applications. Generally, the property predictions are the basis for selection of compounds for incorporation into efficacy evaluations.},
author = {Liang, Jie and Herbert Edelsbrunner},
publisher = {Elsevier},
title = {{Molecular classification for property prediction}},
doi = {US 6,182,016 B1},
year = {2001},
}
@article{3517,
abstract = {A modular multichannel microdrive ('hyperdrive') is described. The microdrive uses printed circuit board technology and flexible fused silica capillaries. The modular design allows for the fabrication of 4-32 independently movable electrodes or `tetrodes'. The drives are re-usable and re-loading the drive with electrodes is simple. },
author = {Szabo,I. and Czurkó, András and Jozsef Csicsvari and Hirase, Hajima and Leinekugel, Xavier and Buzsáki, György},
journal = {Journal of Neuroscience Methods},
number = {1},
pages = {105 -- 110},
publisher = {Elsevier},
title = {{The application of printed circuit board technology for fabrication of multi-channel micro-drives}},
doi = {10.1016/S0165-0270(00)00362-9},
volume = {105},
year = {2001},
}
@article{3540,
abstract = {What determines the firing rate of cortical neurons in the absence of external sensory input or motor behavior, such as during sleep? Hero we report that, in a familiar environment, the discharge frequency of simultaneously recorded individual CA1 pyramidal neurons and the coactivation of cell pairs remain highly correlated across sleep-wake-steep sequences. However, both measures were affected when new sets of neurons were activated in a novel environment. Nevertheless, the grand mean firing rate of the whole pyramidal cell population remained constant across behavioral states and testing conditions. The findings suggest that long-term firing patterns of single cells can be modified by experience. We hypothesize that increased firing rates of recently used neurons are associated with a concomitant decrease in the discharge activity of the remaining population, leaving the mean excitability of the hippocampal network unaltered.},
author = {Hirase, Hajima and Leinekugel, Xavier and Czurkó, András and Jozsef Csicsvari and Buzsáki, György},
journal = {PNAS},
number = {16},
pages = {9386 -- 9390},
publisher = {National Academy of Sciences},
title = {{Firing rates of hippocampal neurons are preserved during subsequent sleep episodes and modified by novel awake experience}},
doi = {10.1073/pnas.161274398},
volume = {98},
year = {2001},
}
@article{3546,
abstract = {Local versus distant coherence of hippocampal CA1 pyramidal cells was investigated in the behaving rat. Temporal cross-correlation of pyramidal cells revealed a significantly stronger relationship among local (<140 <mu>m) pyramidal neurons compared with distant (>300 mum) neurons during non-theta-associated immobility and sleep but not during theta-associated running and walking. In contrast, cross-correlation between local pyramidal cell-interneuron pairs was significantly stronger than between distant pairs during theta oscillations but were similar during non-theta-associated behaviors. We suggest that network state-dependent functional clustering of neuronal activity emerges because of the differential contribution of the main excitatory inputs, the perforant path, and Schaffer collaterals during theta and non-theta behaviors.},
author = {Hirase, Hajima and Leinekugel, Xavier and Jozsef Csicsvari and Czurkó, András and Buzsáki, György},
journal = {Journal of Neuroscience},
number = {10},
publisher = {Society for Neuroscience},
title = {{Behavior-dependent states of the hippocampal network affect functional clustering of neurons}},
volume = {21},
year = {2001},
}
@book{3586,
abstract = {The book combines topics in mathematics (geometry and topology), computer science (algorithms), and engineering (mesh generation). The original motivation for these topics was the difficulty faced (both conceptually and in the technical execution) in any attempt to combine elements of combinatorial and of numerical algorithms. Mesh generation is a topic where a meaningful combination of these different approaches to problem solving is inevitable. The book develops methods from both areas that are amenable to combination, and explains recent breakthrough solutions to meshing that fit into this category.The book should be an ideal graduate text for courses on mesh generation. The specific material is selected giving preference to topics that are elementary, attractive, lend themselves to teaching, useful, and interesting.},
author = {Edelsbrunner, Herbert},
pages = {190},
publisher = {Cambridge University Press},
title = {{Geometry and Topology for Mesh Generation}},
doi = {10.1017/CBO9780511530067},
volume = {7},
year = {2001},
}
@misc{3596,
abstract = {Bürger has written an outstanding book. As well as discussing selection, recombination and mutation, he explains how random drift interacts with these evolutionary forces. Thus, his book covers a large fraction of population genetics, the main exception being the neutral theory of molecular evolution. Although the book is primarily theoretical, it focuses on the biological issues and includes excellent concise summaries of our present empirical knowledge.},
author = {Nicholas Barton},
booktitle = {Trends in Genetics},
pages = {420 -- 420},
publisher = {Elsevier},
title = {{Mendel and mathematics}},
doi = {10.1016/S0168-9525(01)02315-0},
volume = {17},
year = {2001},
}
@article{3622,
abstract = {The extent of genetic variation in fitness and its components and genetic variation's dependence on environmental conditions remain key issues in evolutionary biology. We present measurements of genetic variation in preadult viability in a laboratory-adapted population of Drosophila melanogaster, made at four different densities. By crossing flies heterozygous for a wild-type chromosome and one of two different balancers (TM1, TM2), we measure both heterozygous (TM1/+, TM2/+) and homozygous (+/+) viability relative to a standard genotype (TM1/TM2). Forty wild-type chromosomes were tested, of which 10 were chosen to be homozygous viable. The mean numbers produced varied significantly between chromosome lines, with an estimated between-line variance in loge numbers of 0.013. Relative viabilities also varied significantly across chromosome lines, with a variance in loge homozygous viability of 1.76 and of loge heterozygous viability of 0.165. The between-line variance for numbers emerging increased with density, from 0.009 at lowest density to 0.079 at highest. The genetic variance in relative viability increases with density, but not significantly. Overall, the effects of different chromosomes on relative viability were remarkably consistent across densities and across the two heterozygous genotypes (TM1, TM2). The 10 lines that carried homozygous viable wild-type chromosomes produced significantly more adults than the 30 lethal lines at low density and significantly fewer adults at the highest density. Similarly, there was a positive correlation between heterozygous viability and mean numbers at low density, but a negative correlation at high density.},
author = {Gardner, Michael P and Fowler, Kevin and Patridge, Linda and Nicholas Barton},
journal = {Evolution},
number = {8},
pages = {1609 -- 1620},
publisher = {Wiley-Blackwell},
title = {{Genetic variation for preadult viability in Drosophila melanogaster}},
volume = {55},
year = {2001},
}
@inproceedings{2325,
author = {Robert Seiringer},
pages = {53 -- 72},
publisher = {American Mathematical Society},
title = {{Inequalities for Schrödinger operators and applications to the stability of matter problem }},
doi = {10.1090/conm/529},
volume = {529},
year = {2000},
}
@inproceedings{2342,
author = {Robert Seiringer and Lieb, Élliott H and Yngvason, Jakob},
pages = {101 -- 110},
publisher = {World Scientific Publishing},
title = {{The ground state energy and density of interacting bosons in a trap}},
year = {2000},
}
@article{2343,
abstract = {We study the energy levels of a single particle in a homogeneous magnetic field and in an axially symmetric external potential. For potentials that are superharmonic off the central axis, we find a general 'pseudoconcave' ordering of the ground state energies of the Hamiltonian restricted to the sectors with fixed angular momentum. The physical applications include atoms and ions in strong magnetic fields. There the energies are monotone increasing and concave in angular momentum. In the case of a periodic chain of atoms, the pseudoconcavity extends to the entire lowest band of Bloch functions.},
author = {Baumgartner, Bernhard and Robert Seiringer},
journal = {Letters in Mathematical Physics},
number = {3},
pages = {213 -- 226},
publisher = {Springer},
title = {{On the ordering of energy levels in homogeneous magnetic fields}},
doi = { 10.1023/A:1010978807635},
volume = {54},
year = {2000},
}
@article{2344,
abstract = {The ground-state properties of interacting Bose gases in external potentials, as considered in recent experiments, are usually described by means of the Gross-Pitaevskii energy functional. We present here a rigorous proof of the asymptotic exactness of this approximation for the ground-state energy and particle density of a dilute Bose gas with a positive interaction.},
author = {Lieb, Élliott H and Robert Seiringer and Yngvason, Jakob},
journal = {Physical Review A - Atomic, Molecular, and Optical Physics},
number = {4},
pages = {436021 -- 4360213},
publisher = {American Physical Society},
title = {{Bosons in a trap: A rigorous derivation of the Gross-Pitaevskii energy functional}},
doi = {10.1103/PhysRevA.61.043602},
volume = {61},
year = {2000},
}
@inproceedings{2418,
abstract = {For an absolutely continuous probability measure μ on Rd and a nonnegative integer k, let sk(μ, 0) denote the probability that the convex hull of k+d+1 random points which are i.i.d. according to μ contains the origin 0. For d and k given, we determine a tight upper bound on sk(μ, 0), and we characterize the measures in Rd which attain this bound. This result can be considered a continuous analogue of the Upper Bound Theorem for the maximal number of faces of convex polytopes with a given number of vertices. For our proof we introduce so-called h-functions, continuous counterparts of h-vectors for simplicial convex polytopes.},
author = {Uli Wagner and Welzl, Emo},
pages = {50 -- 56},
publisher = {ACM},
title = {{Origin-embracing distributions or a continuous analogue of the Upper Bound Theorem}},
doi = {10.1145/336154.336176},
year = {2000},
}
@inbook{2494,
abstract = {This chapter focuses on metabotropic glutamate receptors (mGluRs). These receptors are linked to several intracellular signal transduction mechanisms via G-protein and are implicated in diverse functions of the mammalian central nervous system (CNS). These functions include mediation of slow excitatory and inhibitory responses; regulation of calcium channels, potassium channels, and non-selective cation channels; inhibition and facilitation of transmitter release; induction of long-term potentiation and long-term depression; and regulation of neuronal development. Functional diversity of the metabotropic glutamate receptor is reflected in molecular diversity of receptor subtypes. The sites of action of mGluRs are widely found throughout different membrane compartments of neuronal and glial cells. The chapter reviews the differential subcellular localization of metabotropic glutamate receptors in relation to transmitter release sites. Patterns of subcellular localization of mGluRs are different among three subgroups: group I and III mGluRs are mainly localized to somatodendritic and axonal domains of neurons, respectively, while group II mGluRs are extensively localized to both domains as well as to glial cell processes.},
author = {Ryuichi Shigemoto and Mizuno, Noboru},
booktitle = {Glutamate},
pages = {63 -- 98},
publisher = {Elsevier},
title = {{Chapter III Metabotropic glutamate receptors - immunocytochemical and in situ hybridization analyses}},
doi = {10.1016/S0924-8196(00)80044-5},
volume = {18},
year = {2000},
}
@article{2598,
author = {Sillevis-Smitt, Peter A and Kinoshita, Ayae and De Leeuw, Bertie H and Moll, Wiebe J and Coesmans, Michiel P and Jaarsma, Dick and Henzen-Logmans, Sonja C and Vecht, Charles J and De Zeeuw, Chris I and Sekiyama, Naotaka and Nakanishi, Shigetada and Ryuichi Shigemoto},
journal = {New England Journal of Medicine},
number = {1},
pages = {21 -- 27},
publisher = {Massachussetts Medical Society},
title = {{Paraneoplastic cerebellar ataxia due to autoantibodies against a glutamate receptor}},
doi = {10.1056/NEJM200001063420104},
volume = {342},
year = {2000},
}
@article{2599,
abstract = {The synaptic relationship between substance P (SP) and its receptor, i.e., neurokinin-1 receptor (NK1R), was examined in the striatum of the rat by confocal laser-scanning microscopy and electron microscopy. For confocal laser-scanning microscopy, triple-immunofluorescence histochemistry was performed to label NK1R, SP, and vesicular acetylcholine transporter (a specific marker for cholinergic neurons). In electron microscopic double- immunolabeling study, immunoreactivity for NK1R was detected with the silver- intensified gold method, while immunoreactivity for SP was detected with peroxidase immunohistochemistry. Simultaneous immunolabeling of NK1R and SP revealed significant mismatch at the synaptic level: although some SP- immunopositive axon terminals were in synaptic contact with NK1R- immunopositive sites of plasma membrane, NK1R-immunoreactivity was observed at both synaptic and non-synaptic sites of plasma membrane. Thus, SP released from the sites remote from NK1Rs might diffuse in the extracellular fluid to act, as a paracrine neurotransmitter, on NK1Rs distant from its releasing site. SP neurotransmission in the striatum might occur not only synaptically but also extrasynaptically. The SP-NK1R system might constitute an association system within the striatum.},
author = {Li, Jin-Lian and Wang, Dan and Kaneko, Takeshi and Ryuichi Shigemoto and Nomura, Sakashi and Mizuno, Noboru},
journal = {Journal of Comparative Neurology},
number = {2},
pages = {156 -- 163},
publisher = {Wiley-Blackwell},
title = {{Relationship between neurokinin-1 receptor and substance P in the striatum: Light and electron microscopic immunohistochemical study in the rat}},
doi = {10.1002/(SICI)1096-9861(20000306)418:2<156::AID-CNE3>3.0.CO;2-Z},
volume = {418},
year = {2000},
}
@article{2600,
abstract = {The synaptic relationship between substance P (SP) and its receptor, i.e. neurokinin-1 receptor (NK1R), was examined in the superficial laminae of the caudal subnucleus of the spinal trigeminal nucleus (medullary dorsal horn; MDH) of the rat. For confocal laser-scanning microscopy, double-immunofluorescence histochemistry for NK1 and SP was performed. In electron microscopic double-immunolabeling study, immunoreactivity for NK1R was detected with the silver-intensified gold method, while immunoreactivity for SP was detected with peroxidase immunohistochemistry. SP-immunoreactive axon terminals were observed to be in synaptic (mostly asymmetric) contact with NK1R-immunoreactive neuronal profiles in lamina I and lamina IIo. Although some SP-immunoreactive axon terminals were in synaptic contact with NK1R-immunoreactive sites of plasma membranes, NK1R-immunoreactivity was observed at both synaptic and non-synaptic sites of plasma membrane. Thus, SP released from axon terminals might not only act on NK1Rs facing the SP-containing axon terminals, but also diffuse in the extracellular fluid for distances larger than the synaptic cleft to act on NK1Rs at some distances from the synaptic sites. },
author = {Li, Jin-Lian and Wang, Dan and Kaneko, Takeshi and Ryuichi Shigemoto and Nomura, Sakashi and Mizuno, Noboru},
journal = {Neuroscience Research},
number = {4},
pages = {327 -- 334},
publisher = {Elsevier},
title = {{The relationship between neurokinin-1 receptor and substance P in the medullary dorsal horn: A light and electron microscopic immunohistochemical study in the rat}},
doi = {10.1016/S0168-0102(00)00095-X},
volume = {36},
year = {2000},
}
@article{2601,
abstract = {Targeted deletion of metabotropic glutamate receptor-subtype 1 (mGluR1) gene can cause defects in development and function in the cerebellum. We introduced the mGluR1α transgene into mGluR1-null mutant [mGluR1 (-/-)] mice with a Purkinje cell (PC)-specific promoter. mGluR1-rescue mice showed normal cerebellar long-term depression and regression of multiple climbing fiber innervation, events significantly impaired in mGluR1 (-/-) mice. The impaired motor coordination was rescued by this transgene, in a dose-dependent manner. We propose that mGluR1 in PCs is a key molecule for normal synapse formation, synaptic plasticity, and motor control in the cerebellum.},
author = {Ichise, Taeko and Kano, Masanobu and Hashimoto, Kouichi and Yanagihara, Dai and Nakao, Kazuki and Ryuichi Shigemoto and Katsuki, Motoya and Aiba, Atsu},
journal = {Science},
number = {5472},
pages = {1832 -- 1835},
publisher = {American Association for the Advancement of Science},
title = {{mGluR1 in cerebellar Purkinje cells essential for long-term depression, synapse elimination, and motor coordination}},
doi = {10.1126/science.288.5472.1832},
volume = {288},
year = {2000},
}
@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},
}
@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 and Cirino, Paola and Toscano, Alfonso and Giuliano, Paola and Marino, Rita and Pinto, Maria Rosaria 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 and Tada, Masazumi and Rauch, Gerd-Jörg and Saúde, Leonor and Concha, Miguel L and Geisler, Robert and Stemple, Derek L and Smith, James C and Wilson, Stephen W},
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},
}
@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},
}
@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{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},
}
@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},
}
@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{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},
}
@misc{1031,
abstract = {Normal function of organs and cells is tightly linked to the cytoarchitecture. Control of the cell volume is therefore vital for the organism. A widely established strategy of cells to counteract swelling is the activation of chloride and potassium channels, which leads to a net efflux of salt followed by water - a process termed regulatory volume decrease. Since there is evidence for swelling-dependent chloride channels (IClswell) being activated also during pathological processes, the identification of the molecular entity underlying IClswell is of utmost importance. Several proteins are discussed as the channel forming IClswell, i.e. phospholemman, p-glycoprotein, CLC-3 and ICln. In this review we would like to focus on the properties of ICln, a protein cloned from a Madin Darby canine kidney (MDCK) cell library whose expression in Xenopus laevis oocytes resulted in a nucleotide sensitive, outwardly rectifying chloride current closely resembling the biophysical properties of IClswell.},
author = {Fürst, Johannes and Jakab, Martin and König, Matthias A and Ritter, Markus and Gschwentner, Martin and Rudzki, Jakob and Danzl, Johannes G and Mayer, Michael R and Burtscher, Carmen M and Schirmer, Johanna and Maier, Brigitte and Nairz, Manfred and Chwatal, Sabine and Paulmichl, Markus},
booktitle = {Cellular Physiology and Biochemistry},
number = {5-6},
pages = {329 -- 334},
publisher = {S. Karger AG},
title = {{Structure and function of the ion channel ICln}},
doi = {10.1159/000016374},
volume = {10},
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{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{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},
}
@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 and Brennan, Caroline H and Wilson, Stephen W},
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},
}
@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},
}
@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},
}