@misc{4290,
author = {Nicholas Barton},
booktitle = {Genetical Research},
number = {2},
pages = {178 -- 180},
publisher = {Cambridge University Press},
title = {{Natural hybridization and evolution}},
volume = {70},
year = {1997},
}
@misc{4291,
author = {Nicholas Barton},
booktitle = {Genetical Research},
number = {2},
pages = {180 -- 181},
publisher = {Cambridge University Press},
title = {{The ccological detective: Confronting models with data}},
volume = {70},
year = {1997},
}
@inbook{4293,
abstract = {Natural populations differ from the simplest models in ways which can significantly affect their evolution. Real populations are rarely all of the same size; the rates of migration into and out of populations vary in space and time; some populations go extinct, and new ones are established, while all populations fluctuate in size. Furthermore, the genetic properties of real species are not like those assumed in simple models. Alleles are exposed to a wide variety of selection mutation rarely creates novel genotypes with each mutation event, generations overlap, and environments vary from place to place. Evolution in a metapopulation can be substantially different from the predictions of single-population models and, indeed, very different from the simplest models of subdivided species.},
author = {Nicholas Barton and Whitlock, Michael},
booktitle = {Metapopulation Biology},
pages = {183 -- 210},
publisher = {Academic Press},
title = {{The evolution of metapopulations}},
doi = {10.1016/B978-012323445-2/50012-2},
year = {1997},
}
@inproceedings{4438,
abstract = {In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The model-checking problem for the branching-time temporal logic CTL can be solved in linear running time, and model-checking tools for CTL are used successfully in industrial applications. The development of programs that must meet rigid real-time constraints has brought with it a need for real-time temporal logics that enable quantitative reference to time. Early research on real-time temporal logics uses the discrete domain of the integers to model time. Present research on real-time temporal logics focuses on continuous time and uses the dense domain of the reals to model time. There, model checking becomes significantly more complicated. For example, the model-checking problem for TCTL, a continuous-time extension of the logic CTL, is PSPACE-complete.
In this paper we suggest a reduction from TCTL model checking to CTL model checking. The contribution of such a reduction is twofold. Theoretically, while it has long been known that model-checking methods for untimed temporal logics can be extended quite easily to handle discrete time, it was not clear whether and how untimed methods can handle the reset quantifier of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone who has a tool for CTL model checking to use it for TCTL model checking. The TCTL model-checking algorithm that follows from our reduction is in PSPACE, matching the known bound for this problem. In addition, it enjoys the wide distribution of CTL model-checking tools and the extensive and fruitful research efforts and heuristics that have been put into these tools.},
author = {Thomas Henzinger and Kupferman, Orna},
pages = {48 -- 62},
publisher = {Springer},
title = {{From quantity to quality}},
doi = { 10.1007/BFb0014712},
volume = {1201},
year = {1997},
}
@inproceedings{4441,
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 sharply 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},
pages = {582 -- 593},
publisher = {Springer},
title = {{Discrete-time control for rectangular hybrid automata}},
doi = {10.1007/3-540-63165-8_213},
volume = {1256},
year = {1997},
}
@article{4493,
author = {Thomas Henzinger and Ho, Pei-Hsin and Wong-Toi, Howard},
journal = {Software Tools For Technology Transfer},
number = {1-2},
pages = {110 -- 122},
publisher = {Springer},
title = {{HyTech: A model checker for hybrid systems}},
doi = {10.1007/s100090050008},
volume = {1},
year = {1997},
}
@inproceedings{4494,
abstract = {A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement.},
author = {Thomas Henzinger and Ho, Pei-Hsin and Wong-Toi, Howard},
pages = {460 -- 463},
publisher = {Springer},
title = {{HyTech: A model checker for hybrid systems}},
doi = {10.1007/3-540-63166-6_48},
volume = {1254},
year = {1997},
}
@inproceedings{4496,
abstract = {The simulation preorder for labeled transition systems is defined locally as a game that relates states with their immediate successor states. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We extend the local definition of simulation to account for fairness: system S fairly simulates system I iff in the simulation game, there is a strategy that matches with each fair computation of I a fair computation of S. Our definition enjoys a fully abstract semantics and has a logical characterization: S fairly simulates I iff every fair computation tree embedded in the unrolling of I can be embedded also in the unrolling of S or, equivalently, iff every Fair-AFMC formula satisfied by I is satisfied also by S (AFMC is the universal fragment of the alternation-free -calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace-containment, and is therefore useful as an efficientlycomputable local criterion for proving linear-time abstraction hierarchies.},
author = {Thomas Henzinger and Kupferman, Orna and Rajamani, Sriram K},
pages = {273 -- 287},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Fair simulation}},
doi = {10.1007/3-540-63141-0_19},
volume = {1243},
year = {1997},
}
@inproceedings{4520,
abstract = {We define robust timed automata, which are timed automata that accept all trajectories robustly: if a robust timed automaton accepts a trajectory, then it must accept neighboring trajectories also; and if a robust timed automaton rejects a trajectory, then it must reject neighboring trajectories also. We show that the emptiness problem for robust timed automata is still decidable, by modifying the region construction for timed automata. We then show that, like timed automata, robust timed automata cannot be determinized. This result is somewhat unexpected, given that in temporal logic, the removal of realtime equality constraints is known to lead to a decidable theory that is closed under all boolean operations.},
author = {Gupta, Vineet and Thomas Henzinger and Jagadeesan, Radha},
pages = {331 -- 345},
publisher = {Springer},
title = {{Robust timed automata}},
doi = {10.1007/BFb0014736},
volume = {1201},
year = {1997},
}
@inproceedings{4583,
abstract = {In a trace-based world, the modular specification, verification, and control of live systems require each module to be receptive; that is, each module must be able to meet its liveness assumptions no matter how the other modules behave. In a real-time world, liveness is automatically present in the form of diverging time. The receptiveness condition, then, translates to the requirement that a module must be able to let time diverge no matter how the environment behaves. We study the receptiveness condition for real-time systems by extending the model of reactive modules to timed and hybrid modules. We define the receptiveness of such a module as the existence of a winning strategy in a game of the module against its environment. By solving the game on region graphs, we present an (optimal) Exptime algorithm for checking the receptiveness of prepositional timed modules. By giving a fixpoint characterization of the game, we present a symbolic procedure for checking the receptiveness of linear hybrid modules. Finally, we present an assume-guarantee principle for reasoning about timed and hybrid modules, and a method for synthesizing receptive controllers of timed and hybrid modules.},
author = {Alur, Rajeev and Thomas Henzinger},
pages = {74 -- 88},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Modularity for timed and hybrid systems}},
doi = {10.1007/3-540-63141-0_6},
volume = {1243},
year = {1997},
}
@article{4584,
abstract = {This paper introduces, gently but rigorously, the clock approach to real-time programming. We present with mathematical precision, assuming no prerequisites other than familiarity with logical and programming notations, the concepts that are necessary for understanding, writing, and executing clock programs. In keeping with an expository style, all references are clustered in bibliographic remarks at the end of each section. The first appendix presents proof rules for verifying temporal properties of clock programs. The second appendix points to selected literature on formal methods and tools for programming with clocks. In particular, the timed automaton, which is a finite-state machine equipped with clocks, has become a standard paradigm for real-time model checking; it underlies the tools HyTech, Kronos, and Uppaal, which are discussed elsewhere in this volume.},
author = {Alur, Rajeev and Thomas Henzinger},
journal = {Software Tools For Technology Transfer},
number = {1-2},
pages = {86 -- 109},
publisher = {Springer},
title = {{Real-time system = discrete system + clock variables}},
doi = {10.1007/s100090050007},
volume = {1},
year = {1997},
}
@article{3482,
abstract = {AMPA- and NMDA-type glutamate receptors (AMPARs and NMDARs) mediate excitatory synoptic transmission in the basal ganglia and may contribute to excitotoxic injury. We investigated the functional properties of AMPARs and NMDARs expressed by six main types of basal ganglia neurons in acute rat brain slices (principal neurons and cholinergic interneurons of striatum, GABAergic and dopaminergic neurons of substantia nigra, globus pallidus neurons, and subthalamic nucleus neurons) using fast application of glutamate to nucleated and outside-out membrane patches, AMPARs in different types of basal ganglia neurons were functionally distinct. Those expressed in striatal principal neurons exhibited the slowest gating (desensitization time constant τ = 11.5 msec, 1 mM glutamate, 22°C), whereas those in striatal cholinergic interneurons showed the fastest gating (desensitization time constant τ = 3.6 msec). The lowest Ca2+ permeability of AMPARs was observed in nigral dopaminergic neurons (P(CA)/P(NA) = 0.10), whereas the highest Ca2+ permeability was found in subthalamic nucleus neurons (P(Ca)/P(Na) = 1.17). NMDARs of different types of basal ganglia neurons were less variable in their functional properties; those expressed in nigral dopaminergic neurons exhibited the slowest gating (deactivation time constant of predominant fast component τ1 150 msec, 100 μM glutamate), and those of globus pallidus neurons showed the fastest gating (τ1 = 67 msec). The Mg2+ block of NMDARs was similar; the average chord conductance ratio g(+60mv)/g(+40mV) was 0.18-0.22 in 100 μM external Mg2+. Hence, AMPARs expressed in different types of basal ganglia neurons are markedly diverse, whereas NMDARs are less variable in functional properties that are relevant for excitatory synoptic transmission and neuronal vulnerability.},
author = {Götz, Thomas and Kraushaar, Udo and Geiger, Jörg R and Lubke, Joachim H and Berger, Thomas G and Peter Jonas},
journal = {Journal of Neuroscience},
number = {1},
pages = {204 -- 215},
publisher = {Society for Neuroscience},
title = {{Functional properties of AMPA and NMDA receptors expressed in identified types of basal ganglia neurons}},
volume = {17},
year = {1997},
}
@article{3483,
abstract = {The main excitatory pathway of the hippocampal formation is controlled by a network of morphologically distinct populations of GABAergic interneurons. Here we describe a novel type of GABAergic interneuron located in the outer molecular layer (OML) of the rat dentate gyrus with a long- range forward projection from the dentate gyrus to the subiculum across the hippocampal fissure, OML interneurons were recorded in hippocampal slices by using the whole-cell patch-clamp configuration. During recording, cells were filled with biocytin for subsequent light and electron microscopic analysis. Neurons projecting to the subiculum were distributed throughout the entire OML. They had round or ovoid somata and a multipolar dendritic morphology. Two axonal domains could be distinguished: an extensive, tangential distribution within the OML and a long-range vertical and tangential projection to layer 1 and stratum pyramidale of the subiculum. Symmetric synaptic contacts were established by these interneurons on dendritic shafts in the OML and subiculum. OML interneurons were characterized physiologically by short action potential duration and marked afterhyperpolarization that followed the spike. On sustained current injection, they generated high- frequency (up to 130 Hz, 34°C) trains of action potentials with only little adaptation. In situ hybridization and single-call RT-PCR analysis for GAD67 mRNA confirmed the GABAergic nature of OML interneurons. GABAergic interneurons in the OML projecting to the subiculum connect the input and output regions of the hippocampus. Hence, they could mediate long-range feed- forward inhibition and may participate in an oscillating cross-regional interneuron network that may synchronize the activity of spatially distributed principal neurons in the dentate gyrus and the subiculum.},
author = {Ceranik, Katya and Bender, Roland and Geiger, Jörg R and Monyer, Hannah and Peter Jonas and Frotscher, Michael and Lubke, Joachim H},
journal = {Journal of Neuroscience},
number = {14},
pages = {5380 -- 5394},
publisher = {Society for Neuroscience},
title = {{A novel type of GABAergic interneuron connecting the input and the output regions of the hippocampus.}},
volume = {17},
year = {1997},
}
@article{3484,
abstract = {Glutamatergic transmission at a principal neuroninterneuron synapse was investigated by dual whole-cell patch-clamp recording in rat hippocampal slices combined with morphological analysis. Evoked EPSPs with rapid time course (half duration ≃ 4 ms; 34°C) were generated at multiple synaptic contacts established on the interneuron dendrites close to the soma. The underlying postsynaptic conductance change showed a submillisecond rise and decay, due to the precise timing of glutamate release and the rapid deactivation of the postsynaptic AMPA receptors. Simulations based on a compartmental model of the interneuron indicated that the rapid postsynaptic conductance change determines the shape and the somatodendritic integration of EPSPs, thus enabling interneurons to detect synchronous principal neuron activity.},
author = {Geiger, Jörg R and Lubke, Joachim H and Roth, Arnd and Frotscher, Michael and Peter Jonas},
journal = {Neuron},
number = {6},
pages = {1009 -- 1023},
publisher = {Elsevier},
title = {{Submillisecond AMPA receptor-mediated signaling at a principal neuron-interneuron synapse}},
doi = {10.1016/S0896-6273(00)80339-6},
volume = {18},
year = {1997},
}
@article{3485,
abstract = {1. GABAergic interneurones differ from glutamatergic principal neurones in their ability to discharge high-frequency trains of action potentials without adaptation. To examine whether Na+ channel gating contributed to these differences, Na+ currents were recorded in nucleated patches from interneurones (dentate gyrus basket cells, BCs) and principal neurones (CA1 pyramidal cells, PCs) of rat hippocampal slices. 2. The voltage dependence of Na+ channel activation in BCs and PCs was similar. The slope factors of the activation curves, fitted with Boltzmann functions raised to the third power, were 11.5 and 11.8 mV, and the mid-point potentials were -25.1 and -23.9 mV, respectively. 3. Whereas the time course of Na+ channel activation (-30 to +40 mV) was similar, the deactivation kinetics (-100 to -40 mV) were faster in BCs than in PCs (tail current decay time constants, 0.13 and 0.20 ms, respectively, at -40 mV). 4. Na+ channels in BCs and PCs differed in the voltage dependence of inactivation. The slope factors of the steady-state inactivation curves fitted with Boltzmann functions were 6.7 and 10.7 mV, and the mid-point potentials were -58.3 and -62.9 mV, respectively. 5. The onset of Na+ channel inactivation at -55 mV was slower in BC's than in PCs; the inactivation time constants were 18.6 and 9.3 ms, respectively. At more positive potentials the differences in inactivation onset were smaller. 6. The time course of recovery of Na+ channels from inactivation induced by a 30 ms pulse was fast and mono-exponential (τ = 2.0 ms at -120 mV) in BCs, whereas it was slower and biexponential in PCs (τ1 = 2.0 ms and τ2 = 133 ms; amplitude contribution of the slow component, 15%). 7. We conclude that Na+ channels of BCs and PCs differ in gating properties that contribute to the characteristic action potential patterns of the two types of neurones.},
author = {Martina, Marco and Peter Jonas},
journal = {Journal of Physiology},
number = {3},
pages = {593 -- 603},
publisher = {Wiley-Blackwell},
title = {{Functional differences in Na+ channel gating between fast-spiking interneurones and principal neurones in rat hippocampus}},
doi = {10.1111/j.1469-7793.1997.593ba.x},
volume = {505},
year = {1997},
}
@article{3486,
abstract = {1. Dendritic patch-clamp recordings were obtained from mitral cells in rat olfactory bulb slices, up to 350 μm from the soma. Simultaneous dendritic and somatic whole-cell recordings indicated that action potentials (APs) evoked by somatic or dendritic current injection were initiated near the soma. Both the large amplitude (100.7 ± 1.1 mV) and the short duration (1.38 ± 0.07 ms) of the AP were maintained as the AP propagated back into the primary mitral cell dendrites. 2. Outside-out patches isolated from mitral cell dendrites contained voltage-gated Na+ channels (peak conductance density, 90 pS μm-2 at -10 mV). When an AP was used as a somatic voltage-clamp command in the presence of 1 μM tetrodotoxin (TTX), the amplitude of the dendritic potential was attenuated to 48 ± 14 mV. This shows that dendritic Na+ channels support the active back-propagation of APs. 3. Dendritic patches contained voltage-gated K+ channels with high density (conductance density, 513 pS μm-2 at 30 mV. Dendritic K+ currents were reduced to 35% by 1 mM external tetraethylammonium chloride (TEACl). When an AP was used as a somatic voltage clamp command in the presence of TEACl, the dendritic potential was markedly prolonged. This indicates that dendritic K+ channels mediate the fast repolarization of dendritic APs. 4. We conclude that voltage gated Na+ and K+ channels support dendritic APs with large amplitudes and short durations that may trigger fast transmitter release at dendrodendritic synapses in the olfactory bulb.},
author = {Bischofberger, Joseph and Peter Jonas},
journal = {Journal of Physiology},
number = {Pt 2},
pages = {359 -- 365},
publisher = {Wiley-Blackwell},
title = {{Action potential propagation into the presynaptic dendrites of rat mitral cells}},
doi = {10.1111/j.1469-7793.1997.359be.x},
volume = {504},
year = {1997},
}
@article{3541,
abstract = {The contribution of the various hippocampal regions to the maintenance of epileptic activity, induced by stimulation of the perforant path or commissural system, was examined in the awake rat. Combination of multiple-site recordings with silicon probes, current source density analysis and unit recordings allowed for a high spatial resolution of the field events. Following perforant path stimulation, seizures began in the dentate gyrus, followed by events in the CA3-CA1 regions. After commissural stimulation, rhythmic bursts in the CA3-CA1 circuitry preceded the activation of the dentate gyrus. Correlation of events in the different subregions indicated that the sustained rhythmic afterdischarge (2-6 Hz) could not be explained by a cycle-by-cycle excitation of principal cell populations in the hippocampal-entorhinal loop. The primary afterdischarge always terminated in the CA1 region, followed by the dentate gyrus, CA3 region and the entorhinal cortex. The duration and pattern of the hippocampal afterdischarge was essentially unaffected by removal of the entorhinal cortex. The emergence of large population spike bursts coincided with a decreased discharge of interneurons in both CAI and hilar regions. The majority of hilar interneurons displayed a strong amplitude decrement prior to the onset of population spike phase of the afterdischarge. These findings suggest that (i) afterdischarges can independently arise in the CA3-CA1 and entorhinal-dentate gyrus circuitries, (ii) reverberation of excitation in the hippocampal-entorhinal loop is not critical for the maintenance of afterdischarges and (iii) decreased activity of the interneuronal network may release population bursting of principal cells. },
author = {Bragin, Anatol J and Jozsef Csicsvari and Penttonen, Markku and Buzsáki, György},
journal = {Neuroscience},
number = {4},
pages = {1187 -- 1203},
publisher = {Elsevier},
title = {{Epileptic afterdischarge in the hippocampal-entorhinal system: Current source density and unit studies}},
doi = {10.1016/S0306-4522(96)00446-0},
volume = {76},
year = {1997},
}
@article{3630,
abstract = {This paper derives the long-term effective size, Ne, for a general model of population subdivision, allowing for differential deme fitness, variable emigration and immigration rates, extinction, colonization, and correlations across generations in these processes. We show that various long-term measures of Ne are equivalent. The effective size of a metapopulation can be expressed in a variety of ways. At a demographic equilibrium, Ne can be derived from the demography by combining information about the ultimate contribution of each deme to the future genetic make-up of the population and Wright's FST's. The effective size is given by Ne = 1/(1 + var (upsilon) ((1 - FST)/Nin), where n is the number of demes, theta i is the eventual contribution of individuals in deme i to the whole population (scaled such that sigma theta i = n), and < > denotes an average weighted by theta i. This formula is applied to a catastrophic extinction model (where sites are either empty or at carrying capacity) and to a metapopulation model with explicit dynamics, where extinction is caused by demographic stochasticity and by chaos. Contrary to the expectation from the standard island model, the usual effect of population subdivision is to decrease the effective size relative to a panmictic population living on the same resource.},
author = {Whitlock, Michael and Nicholas Barton},
journal = {Genetics},
number = {1},
pages = {427 -- 441},
publisher = {Genetics Society of America},
title = {{The effective size of a subdivided population}},
volume = {146},
year = {1997},
}
@article{3631,
abstract = {In spatially heterogeneous environments, natural selection for maintenance of adaptation to habitats that contribute little to the population's reproduction is weak. In this paper we model a mechanism that can result in loss of fitness in such marginal habitats, and thus lead to specialisation on the main habitat. It involves accumulation of mutations that are deleterious in the marginal habitat but neutral or nearly so in the main habitat (mutations deleterious in the main habitat and neutral in the marginal habitat have a negligible influence). If the contribution of the marginal habitat to total reproduction in the absence of the mutations is less than a threshold value, selection is too weak to counter accumulation of such mutations. A positive feedback then results in loss of fitness in the marginal habitat. This mechanism does not require antagonistic pleiotropy in adaptation to different habitats, although antagonistic pleiotropy facilitates the mutational collapse of fitness in the marginal habitat. We suggest that deleterious mutations with habitat-specific expression may play a role in the evolution of ecological specialisation and promote evolutionary conservatism of ecological niches.},
author = {Kawecki, Tadeusz J and Nicholas Barton and Fry, James D},
journal = {Journal of Evolutionary Biology},
number = {3},
pages = {407 -- 430},
publisher = {Wiley-Blackwell},
title = {{Mutational collapse of fitness in marginal habitats and the evolution of ecological specialisation}},
doi = {10.1046/j.1420-9101.1997.10030407.x},
volume = {10},
year = {1997},
}
@article{3632,
abstract = {An important but controversial class of hypotheses concerning the evolution of female preferences for extreme male mating displays involves 'indirect selection.' Even in the absence of direct fitness effects, preference for males with high overall fitness can spread via a genetic correlation that develops between preference alleles and high fitness genotypes. Here we develop a quantitative expression for the force of indirect selection that (i) applies to any female mating behavior, (ii) is relatively insensitive to the underlying genetics, and (iii) is based on measurable quantities. In conjunction with the limited data now available, it suggests that the evolutionary force generated by indirect selection on preferences is weak in absolute terms. This finding raises the possibility that direct selection on preference genes may often be more important than indirect selection, but more data on the quantities identified by our model and on direct selection are needed to decide the question.},
author = {Kirkpatrick, Mark and Nicholas Barton},
journal = {PNAS},
number = {4},
pages = {1282 -- 1286},
publisher = {National Academy of Sciences},
title = {{The strength of indirect selection on female mating preferences}},
doi = {10.1073/pnas.94.4.1282},
volume = {94},
year = {1997},
}