TY - GEN AU - Barton, Nicholas H AU - Goldman, Nick ID - 4306 T2 - Nature TI - Genetics and geography VL - 357 ER - TY - JOUR AB - Glutamate-operated ion channels (GluR channels) of the L-alpha-amino-3-hydroxy-5-methyl-4-isoxazolepropionic acid (AMPA)-kainate subtype are found in both neurons and glial cells of the central nervous system. These channels are assembled from the GluR-A, -B, -C, and -D subunits; channels containing a GluR-B subunit show an outwardly rectifying current-voltage relation and low calcium permeability, whereas channels lacking the GluR-B subunit are characterized by a doubly rectifying current-voltage relation and high calcium permeability. Most cell types in the central nervous system coexpress several subunits, including GluR-B. However, Bergmann glia in rat cerebellum do not express GluR-B subunit genes. In a subset of cultured cerebellar glial cells, likely derived from Bergmann glial cells. GluR channels exhibit doubly rectifying current-voltage relations and high calcium permeability, whereas GluR channels of cerebellar neurons have low calcium permeability. Thus, differential expression of the GluR-B subunit gene in neurons and glia is one mechanism by which functional properties of native GluR channels are regulated. AU - Burnashev, Nail AU - Khodorova, Alla AU - Jonas, Peter M AU - Helm, P. AU - Wisden, William AU - Monyer, Hannah AU - Seeburg, Peter AU - Sakmann, Bert ID - 3469 IS - 5063 JF - Science SN - 0036-8075 TI - Calcium-permeable AMPA-kainate receptors in fusiform cerebellar glial cells. VL - 256 ER - TY - JOUR AB - A number of rendering algorithms in computer graphics sort three-dimensional objects by depth and assume that there is no cycle that makes the sorting impossible. One way to resolve the problem caused by cycles is to cut the objects into smaller pieces. In this paper we address the problem of estimating how many such cuts arc always sufficient. We also consider a few related algorithmic and combinatorial geometry problems. For example, we demonstrate that n lines in space can be sorted in randomized expected time O(n4’st’), provided that they define no cycle. We also prove an 0(n7’4) upper bound on the number of points in space so that there are n lines with the property that for each point there are at least three noncoplanar lines that contain it. AU - Chazelle, Bernard AU - Edelsbrunner, Herbert AU - Guibas, Leonidas AU - Pollack, Richard AU - Seidel, Raimund AU - Sharir, Micha AU - Snoeyink, Jack ID - 3581 IS - 6 JF - Computational Geometry: Theory and Applications SN - 0925-7721 TI - Counting and cutting cycles of lines and rods in space VL - 1 ER - TY - JOUR AB - Three components of mating call (pulse duration, cycle length, and fundamental frequency) were measured and six diagnostic enzyme loci scored across the hybrid zone between the toads Bombina bombina and B. variegata. All three call components differ significantly, but only cycle length is diagnostic. The clines in call coincide with those for enzymes, and have similar widths. This suggests that there is no strong selection on any of these characters. There are significant correlations between electrophoretic markers and call components, but these are no stronger than would be expected if the electrophoretic loci and the genes causing mating call were neutral. The selection differential on the call is no greater than 6% of the difference in mean cycle length between the two taxa. There is a substantial increase in the variance of cycle length in the center of the zone, suggesting that a small number of loci are involved (≈ three). Recombination between these loci will hinder the evolution of reinforcement and may partly be responsible for the lack of premating isolation between B. bombina and B. variegata. AU - Sanderson, Neil AU - Szymura, Jacek AU - Barton, Nicholas H ID - 3645 IS - 3 JF - Evolution SN - 0014-3820 TI - Variation in mating call across the hybrid zone between the fire-bellied toads Bombina bombina and B. variegata VL - 46 ER - TY - CONF AB - The edge-insertion paradigm improves a triangulation of a finite point set in R2 iteratively by adding a new edge, deleting intersecting old edges, and retriangulating the resulting two polygonal regions. After presenting an abstract view of the paradigm, this paper shows that it can be used to obtain polynomial time algorithms for several types of optimal triangulations. AU - Bern, Marshall AU - Edelsbrunner, Herbert AU - Eppstein, David AU - Mitchell, Stephen AU - Tan, Tiow ED - Simon, Imre ID - 4049 SN - 978-3-540-55284-0 T2 - 1st Latin American Symposium on Theoretical Informatics TI - Edge insertion for optimal triangulations VL - 583 ER - TY - JOUR AB - Arrangements of curves in the plane are fundamental to many problems in computational and combinatorial geometry (e.g. motion planning, algebraic cell decomposition, etc.). In this paper we study various topological and combinatorial properties of such arrangements under some mild assumptions on the shape of the curves, and develop basic tools for the construction, manipulation, and analysis of these arrangements. Our main results include a generalization of the zone theorem of Edelsbrunner (1986) and Chazelle (1985) to arrangements of curves (in which we show that the combinatorial complexity of the zone of a curve is nearly linear in the number of curves) and an application of that theorem to obtain a nearly quadratic incremental algorithm for the construction of such arrangements. AU - Edelsbrunner, Herbert AU - Guibas, Leonidas AU - Pach, János AU - Pollack, Richard AU - Seidel, Raimund AU - Sharir, Micha ID - 4047 IS - 2 JF - Theoretical Computer Science SN - 0304-3975 TI - Arrangements of curves in the plane - topology, combinatorics, and algorithms VL - 92 ER - TY - JOUR AB - The main contribution of this work is an O(n log n + k)-time algorithm for computing all k intersections among n line segments in the plane. This time complexity is easily shown to be optimal. Within the same asymptotic cost, our algorithm can also construct the subdivision of the plane defined by the segments and compute which segment (if any) lies right above (or below) each intersection and each endpoint. The algorithm has been implemented and performs very well. The storage requirement is on the order of n + k in the worst case, but it is considerably lower in practice. To analyze the complexity of the algorithm, an amortization argument based on a new combinatorial theorem on line arrangements is used. AU - Chazelle, Bernard AU - Edelsbrunner, Herbert ID - 4046 IS - 1 JF - Journal of the ACM SN - 0004-5411 TI - An optimal algorithm for intersecting line segments in the plane VL - 39 ER - TY - JOUR AB - It is shown that a triangulation of a set of n points in the plane that minimizes the maximum angle can be computed in time O(n2 log n) and space O(n). The algorithm is fairly easy to implement and is based on the edge-insertion scheme that iteratively improves an arbitrary initial triangulation. It can be extended to the case where edges are prescribed, and, within the same time- and space-bounds, it can lexicographically minimize the sorted angle vector if the point set is in general position. Experimental results on the efficiency of the algorithm and the quality of the triangulations obtained are included. AU - Edelsbrunner, Herbert AU - Tan, Tiow AU - Waupotitsch, Roman ID - 4043 IS - 4 JF - SIAM Journal on Scientific Computing SN - 0097-5397 TI - An O(n^2 log n) time algorithm for the MinMax angle triangulation VL - 13 ER - TY - JOUR AB - Given a sequence of n points that form the vertices of a simple polygon, we show that determining a closest pair requires OMEGA(n log n) time in the algebraic decision tree model. Together with the well-known O(n log n) upper bound for finding a closest pair, this settles an open problem of Lee and Preparata. We also extend this O(n log n) upper bound to the following problem: Given a collection of sets with a total of n points in the plane, find for each point a closest neighbor that does not belong to the same set. AU - Aggarwal, Alok AU - Edelsbrunner, Herbert AU - Raghavan, Prabhakar AU - Tiwari, Prasoon ID - 4048 IS - 1 JF - Information Processing Letters SN - 0020-0190 TI - Optimal time bounds for some proximity problems in the plane VL - 42 ER - TY - CONF 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 mu-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 mu-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 - Henzinger, Thomas A AU - Nicollin, Xavier AU - Sifakis, Joseph AU - Yovine, Sergio ID - 4505 SN - 0-8186-2735-2 T2 - Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science TI - Symbolic model checking for real-time systems ER - TY - CONF AB - Real-time systems operate in “real,” continuous time and state changes may occur at any real-numbered time point. Yet many verification methods are based on the assumption that states are observed at integer time points only. What can we conclude if a real-time system has been shown “correct” for integral observations? Integer time verification techniques suffice if the problem of whether all real-numbered behaviors of a system satisfy a property can be reduced to the question of whether the integral observations satisfy a (possibly modified) property. We show that this reduction is possible for a large and important class of systems and properties: the class of systems includes all systems that can be modeled as timed transition systems; the class of properties includes time-bounded invariance and time-bounded response. AU - Henzinger, Thomas A AU - Manna, Zohar AU - Pnueli, Amir ID - 4504 T2 - 19th International Colloquium on Automata, Languages and Programming TI - What good are digital clocks? VL - 623 ER - TY - CHAP AB - We incorporate time into an interleaving model of concurrency. In timed transition systems, the qualitative fairness requirements of traditional transition system are replaced (and superseded) by quantitative lower-bound and upperbound timing constraints on transitions. The purpose of this paper is to explore the scope of applicability for the abstract model of timed transition systems. We demonstrate that the model can represent a wide variety of phenomena that routinely occur in conjunction with the timed execution of concurrent processes. Our treatment covers both processes that are executed in parallel on separate processors and communicate either through shared variables or by message passing, and processes that time-share a limited number of processors under a given scheduling policy. Often it is this scheduling policy that determines if a system meets its real-time requirements. Thus we explicitly address such questions as time-outs, interrupts, static and dynamic priorities. AU - Henzinger, Thomas A AU - Manna, Zohar AU - Pnueli, Amir ID - 4507 T2 - Real Time: Theory in Practice TI - Timed transition systems VL - 600 ER - TY - JOUR AB - It has been observed repeatedly that the standard safety-liveness classification for properties of reactive systems does not fit for real-time properties. This is because the implicit “liveliness” of time shifts the spectrum towards the safety side. While, for example, response—that “something good” will happen eventually—is a classical liveness property, bounded response—that “something good” will happen soon, within a certain amount of time—has many characteristics of safety. We account for this phenomenon formally by defining safety and liveness relative to a given condition, such as the progress of time. AU - Henzinger, Thomas A ID - 4517 IS - 3 JF - Information Processing Letters SN - 0020-0190 TI - Sooner Is Safer Than Later VL - 43 ER - TY - CONF AB - We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification. AU - Alur, Rajeev AU - Henzinger, Thomas A ID - 4593 T2 - REX Workshop on Real Time: Theory in Practice TI - Logics and models of real time: A survey VL - 600 ER - TY - CONF AB - The authors introduce two-way timed automata-timed automata that can move back and forth while reading a timed word. Two-wayness in its unrestricted form leads, like nondeterminism, to the undecidability of language inclusion. However, if they restrict the number of times an input symbol may be revisited, then two-wayness is both harmless and desirable. The authors show that the resulting class of bounded two-way deterministic timed automata is closed under all boolean operations, has decidable (PSPACE-complete) emptiness and inclusion problems, and subsumes all decidable real-time logics we know. They obtain a strict hierarchy of real-time properties: deterministic timed automata can accept more languages as the bound on the number of times an input symbol may be revisited is increased. This hierarchy is also enforced by the number of alternations between past and future operators in temporal logic. The combination of the results leads to a decision procedure for a real-time logic with past operators AU - Alur, Rajeev AU - Henzinger, Thomas A ID - 4594 T2 - Proceedings of the 33rd Annual Symposium on Foundations of Computer Science TI - Back to the future: Towards a theory of timed regular languages ER -