TY - JOUR
AB - 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.
AU - László Erdös
ID - 2723
IS - 3
JF - Letters in Mathematical Physics
TI - Ground-state density of the Pauli operator in the large field limit
VL - 29
ER -
TY - JOUR
AB - 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.
AU - Leonid Sazanov
AU - Jackson, Julie B
ID - 1947
IS - 2
JF - Biochimica et Biophysica Acta - Bioenergetics
TI - Activation and inhibition of mitochondrial transhydrogenase by metal ions
VL - 1144
ER -
TY - JOUR
AU - Leonid Sazanov
AU - Jackson, Julie B
ID - 1948
IS - 3
JF - Biochemical Society Transactions
TI - Possible functions of the NADP-linked isocitrate dehydrogenase and H+ -transhydrogenase in heart mitochondria
VL - 21
ER -
TY - JOUR
AU - Jackson, Julie B
AU - Cotton, N P J
AU - Williams, Ross H
AU - Bizouarn, Tania
AU - Hutton, Mike N
AU - Leonid Sazanov
AU - Thomas, Christopher M
ID - 1950
IS - 4
JF - Biochemical Society Transactions
TI - Proton-translocating transhydrogenase in bacteria
VL - 21
ER -
TY - CONF
AB - 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
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
ID - 4616
TI - Automatic symbolic verification of embedded systems
ER -
TY - CHAP
AB - 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.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
ED - Grossman, Robert L.
ED - Nerode, Anil
ED - Ravn, Anders P
ED - Rischel, Hans
ID - 4618
T2 - Hybrid Systems
TI - Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems
VL - 736
ER -
TY - CONF
AB - Traditional approaches to the algorithmic verification of real-time systems are limited to checking program correctness with respect to concrete timing properties (e.g., "message delivery within 10 milliseconds"). We address the more realistic and more ambitious problem of deriving symbolic constraints on the timing properties required of real-time systems (e.g., "message delivery within the time it takes to execute two assignment statements"). 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.
AU - Alur, Rajeev
AU - Thomas Henzinger
AU - Vardi, Moshe Y
ID - 4619
TI - Parametric real-time reasoning
ER -
TY - CONF
AB - 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.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
ID - 4620
TI - Computing accumulated delays in real-time systems
VL - 697
ER -
TY - JOUR
AB - 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.
AU - Chazelle, Bernard
AU - Herbert Edelsbrunner
AU - Guibas, Leonidas
AU - Sharir, Micha
AU - Snoeyink, Jack
ID - 4036
IS - 6
JF - SIAM Journal on Computing
TI - Computing a face in an arrangement of line segments and related problems
VL - 22
ER -
TY - JOUR
AB - A plane geometric graph C in ℝ2 conforms to another such graph G if each edge of G is the union of some edges of C. It is proved that, for every G with n vertices and m edges, there is a completion of a Delaunay triangulation of O(m2 n) points that conforms to G. The algorithm that constructs the points is also described.
AU - Herbert Edelsbrunner
AU - Tan, Tiow Seng
ID - 4040
IS - 1
JF - Discrete & Computational Geometry
TI - An upper bound for conforming Delaunay triangulations
VL - 10
ER -
TY - JOUR
AB - The zone theorem for an arrangement of n hyperplanes in d-dimensional real space says that the total number of faces bounding the cells intersected by another hyperplane is O(n(d-1)). This result is the basis of a time-optimal incremental algorithm that constructs a hyperplane arrangement and has a host of other algorithmic and combinatorial applications. Unfortunately, the original proof of the zone theorem, for d greater-than-or-equal-to 3, turned out to contain a serious and irreparable error. This paper presents a new proof of the theorem. The proof is based on an inductive argument, which also applies in the case of pseudohyperplane arrangements. The fallacies of the old proof along with some ways of partially saving that approach are briefly discussed.
AU - Herbert Edelsbrunner
AU - Seidel, Raimund
AU - Sharir, Micha
ID - 4041
IS - 2
JF - SIAM Journal on Computing
TI - On the zone theorem for hyperplane arrangements
VL - 22
ER -
TY - JOUR
AB - It is shown that a triangulation of a set of n points in the plane that minimizes the maximum edge length can be computed in time 0(n2). The algorithm is reasonably easy to implement and is based on the theorem that there is a triangulation with minmax edge length that contains the relative neighborhood graph of the points as a subgraph. With minor modifications the algorithm works for arbitrary normed metrics.
AU - Herbert Edelsbrunner
AU - Tan, Tiow Seng
ID - 4042
IS - 3
JF - SIAM Journal on Computing
TI - A quadratic time algorithm for the minmax length triangulation
VL - 22
ER -
TY - JOUR
AB - Edge insertion iteratively improves a triangulation of a finite point set in ℜ2 by adding a new edge, deleting old edges crossing the new edge, and retriangulating the polygonal regions on either side of the new edge. This paper presents an abstract view of the edge insertion paradigm, and then shows that it gives polynomial-time algorithms for several types of optimal triangulations, including minimizing the maximum slope of a piecewise-linear interpolating surface.
AU - Bern, Marshall
AU - Herbert Edelsbrunner
AU - Eppstein, David
AU - Mitchell, Stephen
AU - Tan, Tiow Seng
ID - 4044
IS - 1
JF - Discrete & Computational Geometry
TI - Edge insertion for optimal triangulations
VL - 10
ER -
TY - JOUR
AB - We apply Megiddo's parametric searching technique to several geometric optimization problems and derive significantly improved solutions for them. We obtain, for any fixed ε>0, an O(n1+ε) algorithm for computing the diameter of a point set in 3-space, an O(8/5+ε) algorithm for computing the width of such a set, and on O(n8/5+ε) algorithm for computing the closest pair in a set of n lines in space. All these algorithms are deterministic.
AU - Chazelle, Bernard
AU - Herbert Edelsbrunner
AU - Guibas, Leonidas
AU - Sharir, Micha
ID - 4045
IS - 1
JF - Discrete & Computational Geometry
TI - Diameter, width, closest line pair, and parametric searching
VL - 10
ER -
TY - JOUR
AB - We have studied the effects of different neurotrophins on the survival and proliferation of rat cerebellar granule cells in culture. These neurons express trkB and trkC, the putative neuronal receptors for brain-derived neurotrophic factor (BDNF) and neurotrophin-3 (NT-3) respectively. Binding studies using iodinated BDNF and NT-3 demonstrated that both BDNF and NT-3 bind to the cerebellar granule neurons with a similar affinity of approximately 2 x 10(-9) M. The number of receptors per granule cell was surprisingly high, approximately 30 x 10(-4) and 2 x 10(5) for BDNF and NT-3, respectively. Both NT-3 and BDNF elevated c-fos mRNA in the granule neurons, but only BDNF up-regulated the mRNA encoding the low-affinity neurotrophin receptor (p75). In contrast to NT-3, BDNF acted as a survival factor for the granule neurons. BDNF also induced sprouting of the granule neurons and significantly protected them against neurotoxicity induced by high (1 mM) glutamate concentrations. Cultured granule neurons also expressed low levels of BDNF mRNA which were increased by kainic acid, a glutamate receptor agonist. Thus, BDNF, but not NT-3, is a survival factor for cultured cerebellar granule neurons and activation of glutamate receptor(s) up-regulates BDNF expression in these cells.
AU - Lindholm, Dan
AU - Dechant, Georg
AU - Heisenberg, Carl-Philipp J
AU - Thoenen, Hans
ID - 4175
IS - 11
JF - European Journal of Neuroscience
TI - Brain-derived neurotrophic factor is a survival factor for cultured rat cerebellar granule neurons and protects them against glutamate-induced neurotoxicity
VL - 5
ER -
TY - JOUR
AB - Thyroid hormones play an important role in brain development, but the mechanism(s) by which triiodothyronine (T3) mediates neuronal differentiation is poorly understood. Here we demonstrate that T3 regulates the neurotrophic factor, neurotrophin-3 (NT-3), in developing rat cerebellar granule cells both in cell culture and in vivo. In situ hybridization experiments showed that developing Purkinje cells do not express NT-3 mRNA but do express trkC, the putative neuronal receptor for NT-3. Addition of recombinant NT-3 to cerebellar cultures from embryonic rat brain induces hypertrophy and neurite sprouting of Purkinje cells, and upregulates the mRNA encoding the calcium-binding protein, calbindin-28 kD. The present study demonstrates a novel interaction between cerebellar granule neurons and developing Purkinje cells in which NT-3 induced by T3 in the granule cells promotes Purkinje cell differentiation.
AU - Lindholm, Dan
AU - Castrén, Eero
AU - Tsoulfas, Pantelis
AU - Kolbeck, Roland
AU - Berzaghi, Maria
AU - Leingärtner, Axel
AU - Heisenberg, Carl-Philipp J
AU - Tesarollo, Lino
AU - Parada, Luis
AU - Thoenen, Hans
ID - 4177
IS - 2
JF - Journal of Cell Biology
TI - Neurotrophin-3 induced by tri-iodothyronine in cerebellar granule cells promotes Purkinje cell differentiation
VL - 122
ER -
TY - JOUR
AB - Evolutionary explanations of ageing fall into two classes. Organisms might have evolved the optimal life history, in which survival and fertility late in life are sacrificed for the sake of early reproduction and survival. Alternatively, the life history might be depressed below this optimal compromise by deleterious mutations: because selection against late-acting mutations is weaker, these will impose a greater load on late life. Evidence for the importance of both is emerging, and unravelling their relative importance presents experimentalists with a major challenge.
AU - Partridge, Linda
AU - Nicholas Barton
ID - 4300
JF - Nature
TI - Optimality, mutation and the evolution of ageing
VL - 362
ER -
TY - CHAP
AU - Nicholas Barton
AU - Gale, Katherine S
ED - Harrison, Richard G
ID - 4301
T2 - Hybrid zones and the evolutionary process
TI - Genetic analysis of hybrid zones
ER -
TY - GEN
AU - Nicholas Barton
ID - 4302
IS - 1
T2 - Genetical Research
TI - Review of "The causes of molecular evolution" by J.H. Gillespie
VL - 62
ER -
TY - JOUR
AB - In a stably subdivided population with symmetric migration, the chance that a favoured allele will be fixed is independent of population structure. However, random extinction introduces an extra component of sampling drift, and reduces the probability of fixation. In this paper, the fixation probability is calculated using the diffusion approximation; comparison with exact solution of the discrete model shows this to be accurate. The key parameters are the rates of selection, migration and extinction, scaled relative to population size (S = 4Ns, M = 4Nm, Λ = 4Nλ); results apply to a haploid model, or to diploids with additive selection. If new colonies derive from many demes, the fixation probability cannot be reduced by more than half. However, if colonies are initially homogeneous, fixation probability can be much reduced. In the limit of low migration and extinction rates (M, Λ 1), it is 2s/{1 + (Λ/MS)(1 −exp(−S))}, whilst in the opposite limit (S 1), it is 4sM/{Λ(Λ + M)}. In the limit of weak selection (M, Λ 1), it is 4sM/{Λ(Λ + M)}. These factors are not the same as the reduction in effective population size (Ne/N), showing that the effects of population structure on selected alleles cannot be understood from the behaviour of neutral markers.
AU - Nicholas Barton
ID - 4303
IS - 2
JF - Genetical Research
TI - The probability of fixation of a favoured allele in a subdivided population
VL - 62
ER -