TY - JOUR
AB - The retinal bipolar cell receiving glutamate transmission from photoreceptors mediates a key process in segregating visual signals into ON center and OFF center pathways. This transmission involves a G protein- coupled metabotropic glutamate receptor (mGluR). Immunocytochemical and immunoelectron microscopic studies indicate the restricted localization of a specific mGluR subtype, mGluR6, at the postsynaptic site of the rat rod bipolar cell. This specialization is developmentally regulated: mGluR6 is initially distributed in both the soma and dendrites and is finally concentrated on the postsynaptic site. The mGluR6 localization is reversed when photoreceptors degenerate in the mutant rat with retinal dystrophy. Evidence is thus presented indicating specialized, developmentally regulated receptor distribution in the central nervous system and the crucial role of mGluR6 in photoreceptor-bipolar cell synaptic transmission.
AU - Nomura, Akinori
AU - Ryuichi Shigemoto
AU - Nakamura, Yasuhisa
AU - Okamoto, Naoyuki
AU - Mizuno, Noboru
AU - Nakanishi, Shigetada
ID - 2554
IS - 3
JF - Cell
TI - Developmentally regulated postsynaptic localization of a metabotropic glutamate receptor in rat rod bipolar cells
VL - 77
ER -
TY - JOUR
AB - Antibodies were raised against two distinct extracellular sequences of the rat mGluR1 metabotropic glutamate receptor expressed as bacterial fusion proteins. Both antibodies specifically reacted with mGluR1 in the rat cerebellum and inhibited the mGluR1 activity as assessed by the analysis of glutamate-stimulated inositol phosphate formation in CHO cells expressing mGluR1. Using these antibodies, we examined the role of mGluR1 in the induction of long-term depression in cultured Purkinje cells. In voltage- clamped Purkinje cells, current induced by iontophoretically applied glutamate was persistently depressed by depolarization of the Purkinje cells in conjunction with the glutamate application. The mGluR1 antibodies completely blocked the depression of glutamate-induced current. The results indicate that activation of mGluR1 is necessary for the induction of cerebellar long-term depression and that these mGluR1 antibodies can be used as selective antagonists.
AU - Ryuichi Shigemoto
AU - Abe, Takaaki
AU - Nomura, Sakashi
AU - Nakanishi, Shigetada
AU - Hirano, Tomoo
ID - 2555
IS - 6
JF - Neuron
TI - Antibodies inactivating mGluR1 metabotropic glutamate receptor block long-term depression in cultured Purkinje cells
VL - 12
ER -
TY - JOUR
AB - The distribution of the metabotropic glutamate receptors mGluR2 and mGluR3 was immunohistochemically examined in the rat cerebellar cortex at both light and electron microscope levels. An antibody was raised against a fusion protein containing a C-terminal portion of mGluR2. On immunoblot, the antibody reacted with both mGluR2 and mGluR3 in rat brain. mGluR2/3 immunoreactivity was expressed in cell bodies, dendrites, and axon terminals of Golgi cells, as well as in presumed glial processes. Golgi axon terminals with mGluR2/3 immunoreactivity were often encountered in the vicinity of glutamatergic mossy fiber terminals. The results suggest that transmitter glutamate may exert control influences upon Golgi cells not only through dendritic mGluR2/3, but also through axonal mGluR2/3.
AU - Ohishi, Hitoshi
AU - Ogawa-Meguro, Reiko
AU - Ryuichi Shigemoto
AU - Kaneko, Takeshi
AU - Nakanishi, Shigetada
AU - Mizuno, Noboru
ID - 2557
IS - 1
JF - Neuron
TI - Immunohistochemical localization of metabotropic glutamate receptors, mGluR2 and mGluR3, in rat cerebellar cortex
VL - 13
ER -
TY - JOUR
AB - Every collection of t≥2 n2 triangles with a total of n vertices in ℝ3 has Ω(t4/n6) crossing pairs. This implies that one of their edges meets Ω(t3/n6) of the triangles. From this it follows that n points in ℝ3 have only O(n8/3) halving planes.
AU - Dey, Tamal K
AU - Herbert Edelsbrunner
ID - 4032
IS - 1
JF - Discrete & Computational Geometry
TI - Counting triangle crossings and halving planes
VL - 12
ER -
TY - JOUR
AB - A collection of geometric selection lemmas is proved, such as the following: For any set P of n points in three-dimensional space and any set S of m spheres, where each sphere passes through a distinct point pair in P. there exists a point x, not necessarily in P, that is enclosed by Ω(m2/(n2 log6 n2/m)) of the spheres in S. Similar results apply in arbitrary fixed dimensions, and for geometric bodies other than spheres. The results have applications in reducing the size of geometric structures, such as three-dimensional Delaunay triangulations and Gabriel graphs, by adding extra points to their defining sets.
AU - Chazelle, Bernard
AU - Herbert Edelsbrunner
AU - Guibas, Leonidas J
AU - Hershberger, John E
AU - Seidel, Raimund
AU - Sharir, Micha
ID - 4033
IS - 6
JF - SIAM Journal on Computing
TI - Selecting heavily covered points
VL - 23
ER -
TY - JOUR
AB - Frequently, data in scientific computing is in its abstract form a finite point set in space, and it is sometimes useful or required to compute what one might call the `'shape” of the set. For that purpose, this article introduces the formal notion of the family of alpha-shapes of a finite point set in R3. Each shape is a well-defined polytope, derived from the Delaunay triangulation of the point set, with a parameter alpha is-an-element-of R controlling the desired level of detail. An algorithm is presented that constructs the entire family of shapes for a given set of size n in time O(n2), worst case. A robust implementation of the algorithm is discussed, and several applications in the area of scientific computing are mentioned.
AU - Herbert Edelsbrunner
AU - Mücke, Ernst P
ID - 4037
IS - 1
JF - ACM Transactions on Graphics
TI - Three-dimensional alpha shapes
VL - 13
ER -
TY - JOUR
AB - We consider a variety of problems on the interaction between two sets of line segments in two and three dimensions. These problems range from counting the number of intersecting pairs between m blue segments and n red segments in the plane (assuming that two line segments are disjoint if they have the same color) to finding the smallest vertical distance between two nonintersecting polyhedral terrains in three-dimensional space. We solve these problems efficiently by using a variant of the segment tree. For the three-dimensional problems we also apply a variety of recent combinatorial and algorithmic techniques involving arrangements of lines in three-dimensional space, as developed in a companion paper.
AU - Chazelle, Bernard
AU - Herbert Edelsbrunner
AU - Guibas, Leonidas J
AU - Sharir, Micha
ID - 4038
IS - 2
JF - Algorithmica
TI - Algorithms for bichromatic line-segment problems and polyhedral terrains
VL - 11
ER -
TY - JOUR
AB - Let P be a simple polygon with n vertices. We present a simple decomposition scheme that partitions the interior of P into O(n) so-called geodesic triangles, so that any line segment interior to P crosses at most 2 log n of these triangles. This decomposition can be used to preprocess P in a very simple manner, so that any ray-shooting query can be answered in time O(log n). The data structure requires O(n) storage and O(n log n) preprocessing time. By using more sophisticated techniques, we can reduce the preprocessing time to O(n). We also extend our general technique to the case of ray shooting amidst k polygonal obstacles with a total of n edges, so that a query can be answered in O(√ log n) time.
AU - Chazelle, Bernard
AU - Herbert Edelsbrunner
AU - Grigni, Michelangelo
AU - Guibas, Leonidas
AU - Hershberger, John
AU - Sharir, Micha
AU - Snoeyink, Jack
ID - 4039
IS - 1
JF - Algorithmica
TI - Ray shooting in polygons using geodesic triangulations
VL - 12
ER -
TY - JOUR
AB - Evolutionary explanations of aging (or senescence) fall into two classes. First, organisms might have evolved the optimal life history, in which survival and fertility late in life are sacrificed for the sake of early reproduction or high pre-adult survival. Second, the life history might be depressed below this optimal compromise by the influx of deleterious mutations; since selection against late-acting mutations is weaker, deleterious mutations will impose a greater load on late life. We discuss ways in which these theories might be investigated and distinguished, with reference to experimental work withDrosophila. While genetic correlations between life history traits determine the immediate response to selection, they are hard to measure, and may not reflect the fundamental constraints on life history. Long term selection experiments are more likely to be informative. The third approach of using experimental manipulations suffers from some of the same problems as measures of genetic correlations; however, these two approaches may be fruitful when used together. The experimental results so far suggest that aging inDrosophila has evolved in part as a consequence of selection for an optimal life history, and in part as a result of accumulation of predominantly late-acting deleterious mutations. Quantification of these effects presents a major challenge for the future.
AU - Partridge, Linda
AU - Nicholas Barton
ID - 4299
IS - 1-3
JF - Genetica
TI - Evolution of aging: Testing the theory using Drosophila
VL - 91
ER -
TY - CONF
AB - We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems (cptss), the specification language of Hybrid Temporal Logic (htl), the graphical system description language of Hybrid Automata, and a proof system for verifying that hybrid automata satisfy their HTL specifications.
The novelty of the approach lies in the continuous-time logic, which allows specification of both point-based and interval-based properties (i.e., properties which describe changes over an interval) and provides direct references to derivatives of variables, and in the proof system that supports verification of point-based and interval-based properties. The proof rules demonstrate that sound and convenient induction rules can be established for continuous-time logics. The proof rules are illustrated on several examples.
AU - Kapur,Arjun
AU - Thomas Henzinger
AU - Manna, Zohar
AU - Pnueli,Amir
ID - 4420
TI - Proving safety properties of hybrid systems
VL - 863
ER -
TY - CONF
AB - We present a methodology for proving temporal properties of the divergent runs of reactive systems with real-valued clocks. A run diverges if time advances beyond any bound. Since the divergent runs of a system may satisfy liveness properties that are not satisfied by some convergent runs, the standard proof rules are incomplete if only divergent runs are considered.
First, we develop a sound and complete proof calculus for divergence, which is based on translating clock systems into discrete systems. Then, we show that simpler proofs can be obtained for stronger divergence assumptions, such as unknown -divergence, which requires that all delays have a minimum duration of some unknown constant . We classify all real-time systems into an infinite hierarchy, according to how well they admit the translation of eventuality properties into equivalent safety properties.
AU - Thomas Henzinger
AU - Kopke, Peter W
ID - 4440
TI - Verification methods for the divergent runs of clock systems
VL - 863
ER -
TY - JOUR
AB - We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties.
AU - Thomas Henzinger
AU - Manna, Zohar
AU - Pnueli,Amir
ID - 4501
IS - 2
JF - Information and Computation
TI - Temporal proof methodologies for timed transition systems
VL - 112
ER -
TY - JOUR
AB - We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
AU - Thomas Henzinger
AU - Nicollin, Xavier
AU - Sifakis, Joseph
AU - Yovine, Sergio
ID - 4503
IS - 2
JF - Information and Computation
TI - Symbolic model checking for real-time systems
VL - 111
ER -
TY - CONF
AB - Fairness is a mathematical abstraction: in a multiprogramming environment, fairness abstracts the details of admissible (“fair”) schedulers; in a distributed environment, fairness abstracts the speeds of independent processors. We argue that the standard definition of fairness often is unnecessarily weak and can be replaced by the stronger, yet still abstract, notion of finitary fairness. While standard weak fairness requires that no enabled transition is postponed forever, finitary weak fairness requires that for every run of a system there is an unknown bound k such that no enabled transition is postponed more than k consecutive times. In general, the finitary restriction fin(F) of any given fairness assumption F is the union of all w-regular safety properties that are contained in F. The adequacy of the proposed abstraction is demonstrated in two ways. Suppose that we prove a program property under the assumption of finitary fairness. In a multiprogramming environment, the program then satisfies the property for all fair finite-state schedulers. In a distributed environment, the program then satisfies the property for all choices of lower and upper bounds on the speeds (or timings) of processors
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4586
TI - Finitary fairness
ER -
TY - CHAP
AB - We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the "freeze" quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.
AU - Alur, Rajeev
AU - Thomas Henzinger
ED - Rus, Teodor
ED - Rattray,Charles
ID - 4590
T2 - Theories and Experiences for Real-Time System Development
TI - Real-time system = discrete system + clock variables
VL - 2
ER -
TY - JOUR
AB - We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4591
IS - 1
JF - Journal of the ACM
TI - A really temporal logic
VL - 41
ER -
TY - CONF
AB - We develop a theory of equivalences for timed systems. Two systems are equivalent iff external observers cannot observe differences in their behavior. The notion of equivalence depends, therefore, on the distinguishing power of the observers. The power of an observer to measure time results in untimed, clock, and timed equivalences: an untimed observer cannot measure the time difference between events; a clock observer uses a clock to measure time differences with finite precision; a timed observer is able to measure time differences with arbitrary precision.
We show that the distinguishing power of clock observers grows with the number of observers, and approaches, in the limit, the distinguishing power of a timed observer. More precisely, given any equivalence for untimed systems, two timed systems are k-clock congruent, for a nonnegative integer k, iff their compositions with every environment that uses k clocks are untimed equivalent. Both k-clock bisimulation congruence and k-clock trace congruence form strict decidable hierarchies that converge towards the corresponding timed equivalences. Moreover, k-clock bisimulation congruence and k-clock trace congruence provide an adequate and abstract semantics for branching-time and linear-time logics with k clocks.
Our results impact on the verification of timed systems in two ways. First, our decision procedure for k-clock bisimulation congruence leads to a new, symbolic, decision procedure for timed bisimilarity. Second, timed trace equivalence is known to be undecidable. If the number of environment clocks is bounded, however, then our decision procedure for k-clock trace congruence allows the verification of timed systems in a trace model.
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
ID - 4614
TI - The observational power of clocks
VL - 836
ER -
TY - CONF
AB - We introduce the class of event- recording timed automata (ERA). An event-recording automaton contains, for every event a, a clock that records the time of the last occurrence of a. The class ERA is, on one hand, expressive enough to model (finite) timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the language inclusion problem is decidable for event-recording automata. We present a translation from timed transition systems to event-recording automata, which leads to an algorithm for checking if two timed transition systems have the same set of timed behaviors.
We also consider event-predicting timed automata (EPA), which contain clocks that predict the time of the next occurrence of an event. The class of event-clock automata (ECA), which contain both event-recording and event-predicting clocks, is a suitable specification language for real-time properties. We provide an algorithm for checking if a timed automaton meets a specification that is given as an event-clock automaton.
AU - Alur, Rajeev
AU - Fix, Limor
AU - Thomas Henzinger
ID - 4615
TI - A determinizable class of timed automata
VL - 818
ER -
TY - CONF
AU - Alur, Rajeev
AU - Courcoubetis, Costas
AU - Thomas Henzinger
AU - Ho, Pei-Hsin
AU - Nicollin, Xavier
AU - Olivero,Alfredo
AU - Sifakis, Joseph
AU - Yovine, Sergio
ID - 4617
TI - The algorithmic analysis of hybrid systems
VL - 199
ER -
TY - JOUR
AB - The tra-1 gene is the terminal regulator in the sex determination pathway in C. elegans, directing all aspects of somatic sexual differentiation. Recessive loss-of-function (lf) mutations in tra-1 masculinize XX animals (normally somatically female), while dominant gain-of-function mutations feminize XO animals (normally male). Most tra-1 (lf) mutations can be fitted into a simple allelic series of somatic masculinization, but a small number of lf alleles do not fit into this series. Here we show that three of these mutations are associated with DNA rearrangements 5' to the coding region. One allele is an inversion that may be subject to a position effect. We also report the isolation of a new class of tra-1 alleles that are responsive to mutations in the smg system of RNA surveillance. We show that two of these express RNAs of aberrant size. We suggest that the smg-sensitive mutations may identify a carboxy-terminal domain required for negative regulation of tra-1 activity.
AU - Zarkower, David
AU - de Bono, Mario
AU - Aronoff, Rachel
AU - Hodgkin, Jonathan
ID - 6167
IS - 3
JF - Developmental Genetics
SN - 0192-253X
TI - Regulatory rearrangements and smg-sensitive allels of the C. elegans sex-determining gene tra-1
VL - 15
ER -