@article{2546,
  abstract     = {Immunochemical characteristics of neostriatal neurons producing substance P receptor (SPR) were examined in adult rats by double- and triple-immunofluorescence methods. In the neostriatum, SPR immunoreactivity was detected in large and medium-sized aspiny neurons. Virtually all SPR-immunoreactive neurons in the neostriatum contained somatostatin (SS) or choline acetyltransferase (ChAT), but not parvalbumin. All SS- and ChAT-immunoreactive neurons in the neostriatum showed SPR immunoreactivity. The co-existence of SS and ChAT was, however, not found in single neurons expressing SPR immunoreactivity. The present results indicate that neostriatal neurons immunoreactive for SPR are segregated into 2 groups: (1) medium-sized, aspiny somatostatinergic, and (2) large, aspiny cholinergic neurons.},
  author       = {Kaneko, Takeshi and Shigemoto, Ryuichi and Nakanishi, Shigetada and Mizuno, Noboru},
  issn         = {0006-8993},
  journal      = {Brain Research},
  number       = {2},
  pages        = {297 -- 303},
  publisher    = {Elsevier},
  title        = {{Substance P receptor-immunoreactive neurons in the rat neostriatum are segregated into somatostatinergic and cholinergic aspiny neurons}},
  doi          = {10.1016/0006-8993(93)91548-7},
  volume       = {631},
  year         = {1993},
}

@article{2723,
  abstract     = {The ground-state density of the Pauli operator in the case of a nonconstant magnetic field with constant direction is studied. It is shown that in the large field limit, the naturally rescaled ground-state density function is bounded from above by the megnetic field, and under some additional conditions, the limit density function is equal to the magnetic field. A restatement of this result yields an estimate on the density of complex orthogonal polynomials with respect to a fairly general weight function. We also prove a special case of the paramagnetic inequality. },
  author       = {Erdös, László},
  issn         = {0377-9017},
  journal      = {Letters in Mathematical Physics},
  number       = {3},
  pages        = {219 -- 240},
  publisher    = {Springer},
  title        = {{Ground-state density of the Pauli operator in the large field limit}},
  doi          = {10.1007/BF00761110},
  volume       = {29},
  year         = {1993},
}

@article{1947,
  abstract     = {Mitochondrial transhydrogenase has been reported previously to be inhibited by high, rather non-physiological concentrations (in the range of 2-20 mM) of divalent cations. We show that the enzyme could be activated by low (from about 1 μM to 1 mM) concentrations of Ca2+ and Mg2+, which are within physiological range. These results bring in line the effects observed with mitochondrial enzyme to the findings with bacterial transhydrogenases. The activation of transhydrogenase by divalent cations is interpreted as an increase in affinity of the NADP(H)-binding site of the enzyme-NAD(H) complex. Reported effects of the metal ions could be important for the enzyme function in vivo.},
  author       = {Sazanov, Leonid A and Jackson, Julie},
  issn         = {0005-2728},
  journal      = {Biochimica et Biophysica Acta - Bioenergetics},
  number       = {2},
  pages        = {225 -- 228},
  publisher    = {Elsevier},
  title        = {{Activation and inhibition of mitochondrial transhydrogenase by metal ions}},
  doi          = {10.1016/0005-2728(93)90177-H},
  volume       = {1144},
  year         = {1993},
}

@article{1948,
  author       = {Sazanov, Leonid A and Jackson, Julie},
  issn         = {0300-5127},
  journal      = {Biochemical Society Transactions},
  number       = {3},
  pages        = {260},
  publisher    = {Portland Press},
  title        = {{Possible functions of the NADP-linked isocitrate dehydrogenase and H+ -transhydrogenase in heart mitochondria }},
  doi          = {10.1042/bst021260s},
  volume       = {21},
  year         = {1993},
}

@article{1950,
  author       = {Jackson, Julie and Cotton, N P J and Williams, Ross and Bizouarn, Tania and Hutton, Mike and Sazanov, Leonid A and Thomas, Christopher},
  issn         = {0300-5127},
  journal      = {Biochemical Society Transactions},
  number       = {4},
  pages        = {1010 -- 1013},
  publisher    = {Portland Press},
  title        = {{Proton-translocating transhydrogenase in bacteria}},
  doi          = {10.1042/bst0211010},
  volume       = {21},
  year         = {1993},
}

@article{4589,
  abstract     = {The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics that are suitable for reasoning about real-time systems, we combine this classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. The resulting theory of timed state sequences is shown to be decidable, albeit nonelementary, and its expressive power is characterized by ω-regular sets. Several more expressive variants are proved to be highly undecidable. This framework allows us to classify a wide variety of real-time logics according to their complexity and expressiveness. Indeed, it follows that most formalisms proposed in the literature cannot be decided. We are, however, able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and we present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.

Copyright © 1993 Academic Press. All rights reserved.},
  author       = {Alur, Rajeev and Henzinger, Thomas A},
  issn         = {0890-5401},
  journal      = {Information and Computation},
  number       = {1},
  pages        = {35 -- 77},
  publisher    = {Elsevier},
  title        = {{Real-time logics: Complexity and expressiveness}},
  doi          = {10.1006/inco.1993.1025},
  volume       = {104},
  year         = {1993},
}

@inproceedings{4616,
  abstract     = {We present a model checking procedure and its implementation for the automatic verification of embedded systems. Systems are represented by hybrid automata - machines with finite control and real-valued variables modeling continuous environment parameters such as time, pressure, and temperature. System properties are specified in a real-time temporal logic and verified by symbolic computation. The verification procedure, implemented in Mathematica, is used to prove digital controllers and distributed algorithms correct. The verifier checks safety, liveness, time-bounded, and duration properties of hybrid automata},
  author       = {Alur, Rajeev and Henzinger, Thomas A and Ho, Pei},
  booktitle    = {1993 Proceedings Real-Time Systems Symposium},
  isbn         = {0-8186-4480-X},
  location     = {Raleigh, NC, United States of America},
  pages        = {2 -- 11},
  publisher    = {IEEE},
  title        = {{Automatic symbolic verification of embedded systems}},
  doi          = {10.1109/REAL.1993.393520 },
  year         = {1993},
}

@inproceedings{4618,
  abstract     = {We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.},
  author       = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A and Ho, Pei},
  booktitle    = {Hybrid Systems},
  editor       = {Grossman, Robert and Nerode, Anil and Ravn, Anders and Rischel, Hans},
  pages        = {209 -- 229},
  publisher    = {Springer},
  title        = {{Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}},
  doi          = {10.1007/3-540-57318-6_30},
  volume       = {736},
  year         = {1993},
}

@inproceedings{4619,
  abstract     = {Traditional approaches to the algorithmic verification of real-time systems are limited to checking program correctness with respect to concrete timing properties (e.g., &quot;message delivery within 10 milliseconds&quot;). We address the more realistic and more ambitious problem of deriving symbolic constraints on the timing properties required of real-time systems (e.g., &quot;message delivery within the time it takes to execute two assignment statements&quot;). To model this problem, we introduce parametric timed automata -- finite-state machines whose transitions are constrained with parametric timing requirements. The emptiness question for parametric timed automata is central to the verification problem. On the negative side, we show that in general this question is undecidable. On the positive side, we provide algorithms for checking the emptiness of restricted classes of parametric timed automata. The practical relevance of these classes is illustrated with several verification examples. There remains a gap between the automata classes for which we know that emptiness is decidable and undecidable, respectively, and this gap is related to various hard and open problems of logic and automata theory.},
  author       = {Alur, Rajeev and Henzinger, Thomas A and Vardi, Moshe},
  booktitle    = {Proceedings of the 25th annual ACM symposium on Theory of Computing},
  location     = {San Diego, CA, United States of America},
  pages        = {592 -- 601},
  publisher    = {ACM},
  title        = {{Parametric real-time reasoning}},
  doi          = {10.1145/167088.167242},
  year         = {1993},
}

@inproceedings{4620,
  abstract     = {We present a verification algorithm for duration properties of finite-state real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated time during which certain state predicates hold. We formalize the concept of durations by introducing duration measures for (dense-time) timed automata. Given a timed automaton with a duration measure, a start and a target state, and a duration constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the start state to the target state such that the accumulated duration along the run satisfies the constraint. Our main result is a novel decision procedure for solving the duration-bounded reachability problem. We also prove that the problem is PSPACE-complete and demonstrate how the solution can be used to verify interesting duration properties of real-time systems.},
  author       = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A},
  booktitle    = {5th International Conference on Computer Aided Verification},
  location     = {Elounda, Greece},
  pages        = {181 -- 193},
  publisher    = {Springer},
  title        = {{Computing accumulated delays in real-time systems}},
  doi          = {10.1007/3-540-56922-7_16},
  volume       = {697},
  year         = {1993},
}

@article{3446,
  abstract     = {An effective character recognition procedure implemented on a new type of hardware system and using a new architecture called CNND is proposed. This CNND contains one or more analog cellular neural networks (CNNs) and some digital logic, combining the advantages of the fast analog CNN signal processing and the fast and easy decision capability of digital logic. It is shown that the CNND system can be used for recognition of multifont printed or handwritten characters and could recognize 100,000 char/s with a recognition rate of more than 95%. The more advantage of the system over competing types is that there is not an extra feature extraction procedure implemented in slow hardware},
  author       = {Sziranyi, Tamas and Csicsvari, Jozsef L},
  issn         = {1057-7130},
  journal      = {IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing},
  number       = {3},
  pages        = {223 -- 231},
  publisher    = {IEEE},
  title        = {{High-speed character recognition using a dual cellular neural network architecture (CNND)}},
  doi          = {10.1109/82.222823},
  volume       = {40},
  year         = {1993},
}

@inbook{3451,
  author       = {Jonas, Peter M},
  booktitle    = {Molecular Basis of Ion Channels and Receptors Involved in Nerve Excitation, Synaptic Transmission, and Muscle Contraction},
  pages        = {126 -- 135},
  publisher    = {New York Academy of Sciences},
  title        = {{Glutamate receptors in the central nervous system}},
  doi          = {10.1111/j.1749-6632.1993.tb38048.x},
  volume       = {707},
  year         = {1993},
}

@inbook{3452,
  abstract     = {In recent years, considerable progress in our understanding of the molecular events underlying excitatory synaptic transmission has been made. This progress was mainly achieved by technical advances, among them the patch-clamp technique in brain slices (Edwards et al., 1989), fast application of agonists (Franke et al., 1987), and cloning and functional expression of GluR channels of the nonNMDA type (e.g., Hollmann et al., 1989). A suitable model for studying excitatory postsynaptic currents (EPSCs) in the brain slice with patch-clamp techniques is the mossy fiber synapse on CA3 pyramidal cells of rat hippocampus (MF-CA3 synapse). This synapse is located close to the cell soma and should provide almost ideal space-clamp conditions. A comparison of MF-CA3 EPSCs with the currents activated by fast application of glutamate on membrane patches isolated from CA3 cell somata suggests that the concentration of glutamate in the synaptic cleft during excitatory synaptic transmission is high (about 1 mM) and that the transmitter remains in the synaptic cleft only briefly (about 1 ms). It seems likely that desensitization influences the peak amplitude of the EPSC in several ways. Brief pulses of glutamate cause desensitization, from which the glutamate receptor channels recover only slowly, and micromolar ambient glutamate concentrations produce desensitization at equilibrium. From the functional properties of recombinant GluR channels, in situ hybridization data, and patch-clamp experiments on different neuronal and nonneuronal cell types, a picture of the molecular identity of native channels emerges. In neurons of the hippocampus the pharmacological features of these channels were similar to recombinant channels assembled from subunits of the AMPA/kainate subtype which are strongly expressed in these cells. The native channels are characterized by outward rectification of the steady-state I-V and low Ca permeability, similar to recombinant channels containing the GluR-B subunit. This is consistent with the ubiquitous expression of this subunit in hippocampal neurones. In contrast, GluR channels from cerebellar glial cells, which uniquely in the central nervous system lack the expression of GluR-B subunits, show double rectification and high Ca permeability. The results suggest that the native functional nonNMDA glutamate receptor channels in the CNS are assembled form subunits of the AMPA/kainate subtype in a cell-specific way, with the functional properties of GluR channels in neurones being dominated by the GluR-B subunit.},
  author       = {Jonas, Peter M},
  booktitle    = {Nonselective cation channels: Pharmacology, Physiology and Biophysics.},
  editor       = {Siemen, Detlef},
  isbn         = {978-3-0348-7327-7},
  pages        = {61 -- 76},
  publisher    = {Birkhäuser},
  title        = {{AMPA-type glutamate receptors - nonselective cation channels mediating fast excitatory transmission in the CNS}},
  doi          = {10.1007/978-3-0348-7327-7_4},
  volume       = {66},
  year         = {1993},
}

@article{3473,
  abstract     = {Sixteen different K+ channel subtypes have been cloned from mammalian tissue. Considering their sequence homology to Drosophila Shaker, Shab, Shaw and Shal channels, they were classified into four corresponding classes Kv1-4. All K+ channels belonging to these classes consist of four subunits with each six hydrophobic segments (S1-S6) and a characteristic structure-function relationship of certain domains in their amino acid sequence. These domains are, the inactivation gate in the N-terminal region of the sequence, the voltage sensor in the fourth hydrophobic segment (S4), and the pore-region in the H5 segment between S5 and S6. In some functional properties K+ channels cloned from the mammalian brain, however, differ from Drosophila K+ channels. These are pharmacological differences, differences in the threshold of activation and in regulation of inactivation. Part of these differences are important to understand their physiological role in the brain. Based on their functional characteristics the expression pattern of cloned K+ channels in the rat brain can be correlated with the properties of K+ currents measured in central neurones.},
  author       = {Ruppersberg, Peter and Ermler, Mamfred and Knopf, Martin and Kues, Wilfried and Jonas, Peter M and Koenen, Michael},
  issn         = {1015-8987},
  journal      = {Cellular Physiology and Biochemistry},
  pages        = {250 -- 269},
  publisher    = {S. Karger AG},
  title        = {{Properties of Shaker-homologous potassium channels expressed in the mammalian brain.}},
  doi          = {10.1159/000154691},
  volume       = {3},
  year         = {1993},
}

@article{3474,
  abstract     = {1. Excitatory postsynaptic currents (EPSCs) were recorded in CA3 pyramidal cells of hippocampal slices of 15- to 24-day-old rats (22 degrees C) using the whole-cell configuration of the patch clamp technique. 2. Composite EPSCs were evoked by extracellular stimulation of the mossy fibre tract. Using the selective blockers 6-cyano-7-nitroquinoxaline-2,3-dione (CNQX) and D-2-amino-5-phosphonopentanoic acid (APV), a major alpha-amino-3-hydroxy-5-methylisoxazole-4-propionate (AMPA)/kainate receptor-mediated component and a minor NMDA receptor-mediated component with slower time course were distinguished. For the AMPA/kainate receptor-mediated component, the peak current-voltage (I-V) relation was linear, with a reversal potential close to 0 mV. The half-maximal blocking concentration of CNQX was 353 nM. 3. Unitary EPSCs of the mossy fibre terminal (MF)-CA3 pyramidal cell synapse were evoked at membrane potentials of -70 to -90 mV by low-intensity extracellular stimulation of granule cell somata using fine-tipped pipettes. The EPSC peak amplitude as a function of stimulus intensity showed all-or-none behaviour. The region of low threshold was restricted to a few micrometres. This suggests that extracellular stimulation was focal, and that the stimulus-evoked EPSCs were unitary. 4. Latency and rise time histograms of EPSCs evoked by granule cell stimulation showed narrow unimodal distributions within each experiment. The mean latency was 4.2 +/- 1.0 ms, and the mean 20-80% rise time was 0.6 +/- 0.1 ms (23 cells). When fitted within the range 0.7 ms to 20 ms after the peak, the decay of the EPSCs with the fastest rise (rise time 0.5 ms or less) could be described by a single exponential function; the mean time constant was in the range 3.0-6.6 ms with a mean of 4.8 ms (8 cells). 5. Peak amplitudes of the EPSCs evoked by suprathreshold granule cell stimulation fluctuated between trials. The apparent EPSC peak conductance in normal extracellular solution (2 mM Ca2+, 1 mM Mg2+), excluding failures, was 1 nS. Reducing the Ca2+ concentration and increasing the Mg2+ concentration reduced the mean peak amplitude in a concentration-dependent manner. 6. Peaks in EPSC peak amplitude distributions were apparent in low Ca2+ and high Mg2+. Using the criteria of equidistance and the presence of peaks and dips in the autocorrelation function, five of nine EPSC peak amplitude distributions were judged to be quantal.},
  author       = {Jonas, Peter M and Major, Guy and Sakmann, Bert},
  issn         = {0022-3751},
  journal      = {Journal of Physiology},
  pages        = {615 -- 663},
  publisher    = {Wiley-Blackwell},
  title        = {{Quantal components of unitary EPSCs at the mossy fibre synapse on CA3 pyramidal cells of rat hippocampus}},
  doi          = {10.1113/jphysiol.1993.sp019965},
  volume       = {472},
  year         = {1993},
}

@inbook{3568,
  author       = {Edelsbrunner, Herbert},
  booktitle    = {Handbook of Convex Geometry},
  isbn         = {978-0-444-89596-7},
  pages        = {699 -- 735},
  publisher    = {North Holland},
  title        = {{Geometric algorithms}},
  doi          = {10.1016/C2009-0-15705-7},
  year         = {1993},
}

@inbook{3569,
  author       = {Edelsbrunner, Herbert},
  booktitle    = {Current Trends in Theoretical Computer Science, Essays and Tutorials},
  isbn         = {978-9810214623},
  pages        = {1 -- 48},
  publisher    = {World Scientific Publishing},
  title        = {{Computational geometry}},
  year         = {1993},
}

@article{3643,
  abstract     = {We investigate the establishment and spread of new adaptive peaks within Wright's ‘shifting balance’. The third phase of the ‘shifting balance’ involves a kind of group selection, since demes in which a superior peak has been established contain more individuals, and so send out more migrants. We assume that population size, N, increases with mean fitness, , according to the exponential relation, . Here, k is a measure of the weakness of density-dependent regulation, and equals the inverse of the regression of log (fitness) on log(N). In the island model, we find that just as with soft selection (k = 0), two distinct types of behaviour exist: group selection makes no qualitative difference. With low numbers of migrants, demes fluctuate almost independently, and only one equilibrium exists. With large numbers of migrants, all the demes evolve towards the same adaptive peak, and so the whole population can move towards one or other of the peaks. Group selection can be understood in terms of an effective mean fitness function. Its main consequence is to increase the effect of selection relative to drift (Ns), and so increase the bias towards the fitter peak. However, this increased bias depends on the ratio between k and the deme size (k/N), and so is very small when density-dependence is reasonably strong.},
  author       = {Rouhani, Shahin and Barton, Nicholas H},
  issn         = {0016-6723},
  journal      = {Genetical Research},
  number       = {2},
  pages        = {127 -- 136},
  publisher    = {Cambridge University Press},
  title        = {{Group selection and the 'shifting balance'}},
  doi          = {10.1017/S0016672300031232},
  volume       = {61},
  year         = {1993},
}

@article{3644,
  abstract     = {Wright proposed that there is a ' shifting balance' between selection within demes, random drift, and selection between demes at different 'adaptive peaks'. We investigate the establishment and spread of new adaptive peaks, considering a chromosome rearrangement, and a polygenic character under disruptive selection. When the number of migrants (Nm) is small, demes fluctuate independently, with a bias towards the fitter peak. When Nm is large, the whole population can
move to one of two stable equilibria, and so can be trapped near the lower peak. These two regimes are separated by a sharp transition at a critical Nm of order 1. Just below this critical point, adaptation is most efficient, since the shifting balance greatly increases the proportion of demes that reach the global optimum. This is so even if one peak is only slightly fitter than the other (AWx \/N), and for both strong and weak selection (Ns <§ 1 or Ns > 1). Provided that Nm
varies sufficiently gradually from place to place, the fitter peak can be established in regions where Nm « 1, and can then spread through the rest of the range. Our analysis confirms Wright's argument that if selection, migration and drift are of the same order, the ' shifting balance' leads to efficient evolution towards the global optimum.},
  author       = {Barton, Nicholas H and Rouhani, Shahin},
  issn         = {0016-6723},
  journal      = {Genetical Research},
  number       = {1},
  pages        = {57 -- 74},
  publisher    = {Cambridge University Press},
  title        = {{Adaptation and the 'shifting balance'}},
  doi          = {10.1017/S0016672300031098 },
  volume       = {61},
  year         = {1993},
}

@article{4036,
  abstract     = {This paper presents a randomized incremental algorithm for computing a single face in an arrangement of n line segments in the plane that is fairly simple to implement. The expected running time of the algorithm is O(nα(n)log n). The analysis of the algorithm uses a novel approach that generalizes and extends the Clarkson-Shor analysis technique [in Discrete Comput. Geom., 4(1989), pp. 387-421]. A few extensions of the technique, obtaining efficient randomized incremental algorithms for constructing the entire arrangement of a collection of line segments and for computing a single face in an arrangement of Jordan arcs are also presented.},
  author       = {Chazelle, Bernard and Edelsbrunner, Herbert and Guibas, Leonidas and Sharir, Micha and Snoeyink, Jack},
  issn         = {0097-5397},
  journal      = {SIAM Journal on Computing},
  number       = {6},
  pages        = {1286 -- 1302},
  publisher    = {SIAM},
  title        = {{Computing a face in an arrangement of line segments and related problems}},
  doi          = {10.1137/0222077 },
  volume       = {22},
  year         = {1993},
}

