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 -
TY - JOUR
AU - László Erdös
ID - 2713
IS - 2
JF - Duke Mathematical Journal
TI - Estimates on stochastic oscillatory integrals and on the heat kernel of the magnetic Schrödinger operator
VL - 76
ER -
TY - JOUR
AB - H+-transhydrogenase (H+-Thase) and NADP-linked isocitrate dehydrogenase (NADP-ICDH) are very active in animal mitochondria but their physiological function is only poorly understood. This is especially so in the case of the heart and muscle, where there are no major consumers of NADPH. We propose here that H+-Thase and NADP-ICDH have a combined function in the fine regulation of the activity of the tricarboxylic acid (TCA) cycle, providing enhanced sensitivy to changes in energy demand. This is achieved through cycling of substrates by NAD-linked ICDH, NADP-linked ICDH and H+-Thase. It is proposed that NAD-ICDH operates in the forward direction of the TCA cycle, but NADP-ICDH is driven in reverse by elevated levels of NADPH resulting from the action of the transmembrane proton electrochemical potential gradient (Δp) on H+-Thase. This has the effect of increasing the sensitivity to allosteric modifiers of NAD-ICDH (NADH, ADP, ATP, Ca2+ etc), potentially giving rise to large changes in the net flux from iso-citrate to α-ketoglutarate. Furthermore, changes in the level of Δp resulting from changes in the demand for ATP would, via H+-Thase, shift the redox state of the NADP pool and this, in turn, would lead to a change in the rate of the reaction catalysed by NADP-ICDH and hence to an additional and complementary effect on the net metabolic flux from isocitrate to α-ketoglutarate. Other consequences of this substrate cycle are, (i) the production of heat at the expense of Δp, which may contribute to thermoregulation in the animal, and (ii) an increased rate of dissipation of Δp (leak).
AU - Leonid Sazanov
AU - Jackson, Julie B
ID - 1949
IS - 2-3
JF - FEBS Letters
TI - Proton translocating transhydrogenase and NAD- and NADP-linked isocitrate dehydrogenases operate in a substrate cycle which contributes to fine regulation of the tricarboxylic acid cycle activity in mitochondria
VL - 344
ER -
TY - JOUR
AB - The respiratory burst induced by phorbol myristate acetate in mouse macrophages was inhibited by ultra-low doses (10-15 -10-13 M) of an opioid peptide [d-Ala2] methionine enkephalinamide. The effect disappeared at concentrations above and below this range. The inhibition approached 50% and was statistically significant (P < 0.001). Increasing the time of the opioid incubation with cells brought about a shift in the maximal effect to lower concentrations of the opioid (from 10-13 to 5 · 10-15 M) and led to a decrease in the value of the effect, fully in accord with the previously proposed adaptation mechanism of the action of ultra-low doses.
AU - Efanov, Alexander M
AU - Koshkin, Aleksei A
AU - Leonid Sazanov
AU - Borodulina, O I
AU - Varfolomeev, Sergei D
AU - Zaǐtsev, Sergei V
ID - 1953
IS - 2
JF - FEBS Letters
TI - Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism
VL - 355
ER -
TY - CHAP
AB - Unitary excitatory postsynaptic current (EPSC) amplitude histograms obtained from synapses between mossy fibers (MF) and CA3 pyramidal cells in hippocampus were analyzed with the aim of deriving the mean peak current of quantal events, its coefficient of variation CVq, the number of release sites NS, and the release probability PR. Unitary EPSC histograms with multiple peaks were fitted satisfactorily under the assumption that quantal events have a slightly skewed amplitude distribution and that the release mechanism is described by models with either binomial (standard), nonuniform, or nonstationary statistics. The average peak current of the quantal event derived from these fits reflected the opening of between 15 and 65 glutamate receptor (GluR) channels of the AMPAR subtype. The variability in the amplitude of quantal events is characterized by a CVq of 25% to 30%. The best fits to multiple peak EPSC histograms are obtained if it is assumed that the number of release sites contained within a single MF-bouton is between 8 and 21, a value comparable to the published number of morphologically measured presynpatic active zones and postsynaptic densities (PSDs) of individual MF-CA3 synapses. This suggests that at the MF-CA3 synapse each presynaptic zone and its associated PSD act as independent units, contributing one quantal event to unitary EPSCs. Simulations of unitary EPSC distributions, based on measurements of PSD size could, however, indicate that the interpretation of multipeak EPSC amplitude distributions at MF-CA3 synapses in terms of fluctuating release probabilities might be an over-simplification, and that postsynaptic factors may contribute significantly to fluctuations of unitary EPSC amplitudes.
AU - von Kitzing, Eberhard
AU - Peter Jonas
AU - Sakmann, Bert
ED - Stjärne, Lennart
ED - Greengard, Paul
ED - Grillner, Sten E
ED - Hökfelt, Tomas G M
ED - Ottoson, David R
ID - 3453
T2 - Molecular and cellular mechanisms of neurotransmitter release
TI - Quantal analysis of excitatory postsynaptic currents at the hippocampal mossy fiber-CA3 pyramidal cell synapse
VL - 29
ER -
TY - JOUR
AB - Excitatory postsynaptic currents in neurones of the central nervous system have a dual-component time course that results from the co-activation of AMPA/kainate-type and NMDA-type glutamate receptors. New approaches in electrophysiology and molecular biology have provided a better understanding of the factors that determine the kinectics of excitatory postsynaptic currents. Recent studies suggest that the time course of neurotransmitter concentration in the synaptic cleft, the gating properties of the native channels, and the glutamate receptor subunit composition all appear to be important factors.
AU - Peter Jonas
AU - Spruston, Nelson
ID - 3460
IS - 3
JF - Current Opinion in Neurobiology
TI - Mechanisms shaping glutamate-mediated excitatory postsynaptic currents in the CNS
VL - 4
ER -
TY - JOUR
AB - 1. A potassium channel activated by internal Na+ ions (K+Na channel) was identified in peripheral myelinated axons of Xenopus laevis using the cell-attached and excised configurations of the patch clamp technique. 2. The single-channel conductance for the main open state was 88 pS with [K+]o = 105 mM and pS with [K+]o = 2.5 mM ([K+]i = 105 mM). The channel was selectively permeable to K+ over Na+ ions. A characteristic feature of the K+Na channel was the frequent occurrence of subconductance states. 3. The open probability of the channel was strongly dependent on the concentration of Na+ ions at the inner side of the membrane. The half-maximal activating Na+ concentration and the Hill coefficient were 33 mM and 2.9, respectively. The open probability of the channel showed only weak potential dependence. 4. The K+Na channel was relatively insensitive to external tetraethylammonium (TEA+) in comparison with voltage-dependent axonal K+ channels; the half-maximal inhibitory concentration (IC50) was 21.3 mM (at -90 mV). In contrast, the channel was blocked by low concentrations of external Ba2+ and Cs+ ions, with IC50 values of 0.7 and 1.1 mM, respectively (at -90 mV). The block by Ba2+ and Cs+ was more pronounced at negative than at positive membrane potentials. 5. A comparison of the number of K+Na channels in nodal and paranodal patches from the same axon revealed that the channel density was about 10-fold higher at the node of Ranvier than at the paranode. Moreover, a correlation between the number of K+Na channels and voltage-dependent Na+ channels in the same patches was found, suggesting co-localization of both channel types. 6. As weakly potential-dependent ('leakage') channels, axonal K+Na channels may be involved in setting the resting potential of vertebrate axons. Simulations of Na+ ion diffusion suggest two possible mechanisms of activation of K+Na channels: the local increase of Na+ concentration in a cluster of Na+ channels during a single action potential or the accumulation in the intracellular axonal compartment during a train of action potentials.
AU - Koh, Duk S
AU - Peter Jonas
AU - Vogel, Werner
ID - 3475
JF - Journal of Physiology
TI - Na+-activated K+ channels localized in the nodal region of myelinated axons of Xenopus
VL - 479
ER -