@article{4038,
abstract = {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.},
author = {Chazelle, Bernard and Herbert Edelsbrunner and Guibas, Leonidas J and Sharir, Micha},
journal = {Algorithmica},
number = {2},
pages = {116 -- 132},
publisher = {Springer},
title = {{Algorithms for bichromatic line-segment problems and polyhedral terrains}},
doi = {10.1007/BF01182771},
volume = {11},
year = {1994},
}
@article{4039,
abstract = {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.},
author = {Chazelle, Bernard and Herbert Edelsbrunner and Grigni, Michelangelo and Guibas, Leonidas and Hershberger, John and Sharir, Micha and Snoeyink, Jack},
journal = {Algorithmica},
number = {1},
pages = {54 -- 68},
publisher = {Springer},
title = {{Ray shooting in polygons using geodesic triangulations}},
doi = {10.1007/BF01377183},
volume = {12},
year = {1994},
}
@article{4299,
abstract = {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.},
author = {Partridge, Linda and Nicholas Barton},
journal = {Genetica},
number = {1-3},
pages = {89 -- 98},
publisher = {Springer},
title = {{Evolution of aging: Testing the theory using Drosophila}},
doi = {10.1007/BF01435990},
volume = {91},
year = {1994},
}
@inproceedings{4420,
abstract = {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.},
author = {Kapur,Arjun and Thomas Henzinger and Manna, Zohar and Pnueli,Amir},
pages = {431 -- 454},
publisher = {Springer},
title = {{Proving safety properties of hybrid systems}},
doi = {10.1007/3-540-58468-4_177},
volume = {863},
year = {1994},
}
@inproceedings{4440,
abstract = {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.},
author = {Thomas Henzinger and Kopke, Peter W},
pages = {351 -- 372},
publisher = {Springer},
title = {{Verification methods for the divergent runs of clock systems}},
doi = {10.1007/3-540-58468-4_173},
volume = {863},
year = {1994},
}
@article{4501,
abstract = {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.
},
author = {Thomas Henzinger and Manna, Zohar and Pnueli,Amir},
journal = {Information and Computation},
number = {2},
pages = {273 -- 337},
publisher = {Elsevier},
title = {{Temporal proof methodologies for timed transition systems}},
doi = {10.1006/inco.1994.1060},
volume = {112},
year = {1994},
}
@article{4503,
abstract = {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.
},
author = {Thomas Henzinger and Nicollin, Xavier and Sifakis, Joseph and Yovine, Sergio},
journal = {Information and Computation},
number = {2},
pages = {193 -- 244},
publisher = {Elsevier},
title = {{Symbolic model checking for real-time systems}},
doi = {10.1006/inco.1994.1045},
volume = {111},
year = {1994},
}
@inproceedings{4586,
abstract = {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},
author = {Alur, Rajeev and Thomas Henzinger},
pages = {52 -- 61},
publisher = {IEEE},
title = {{Finitary fairness}},
doi = {10.1109/LICS.1994.316087 },
year = {1994},
}
@inbook{4590,
abstract = {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.},
author = {Alur, Rajeev and Thomas Henzinger},
booktitle = {Theories and Experiences for Real-Time System Development},
editor = {Rus, Teodor and Rattray,Charles},
pages = {1 -- 29},
publisher = {World Scientific Publishing},
title = {{Real-time system = discrete system + clock variables}},
volume = {2},
year = {1994},
}
@article{4591,
abstract = {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.},
author = {Alur, Rajeev and Thomas Henzinger},
journal = {Journal of the ACM},
number = {1},
pages = {181 -- 204},
publisher = {ACM},
title = {{A really temporal logic}},
doi = {10.1145/174644.174651},
volume = {41},
year = {1994},
}
@inproceedings{4614,
abstract = {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.},
author = {Alur, Rajeev and Courcoubetis, Costas and Thomas Henzinger},
pages = {162 -- 177},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The observational power of clocks}},
doi = {10.1007/BFb0015008},
volume = {836},
year = {1994},
}
@inproceedings{4615,
abstract = {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.},
author = {Alur, Rajeev and Fix, Limor and Thomas Henzinger},
pages = {1 -- 13},
publisher = {Springer},
title = {{A determinizable class of timed automata}},
doi = {10.1007/3-540-58179-0_39},
volume = {818},
year = {1994},
}
@inproceedings{4617,
author = {Alur, Rajeev and Courcoubetis, Costas and Thomas Henzinger and Ho, Pei-Hsin and Nicollin, Xavier and Olivero,Alfredo and Sifakis, Joseph and Yovine, Sergio},
pages = {331 -- 351},
publisher = {Springer},
title = {{The algorithmic analysis of hybrid systems}},
doi = {10.1007/BFb0033565},
volume = {199},
year = {1994},
}
@article{6167,
abstract = {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.},
author = {Zarkower, David and de Bono, Mario and Aronoff, Rachel and Hodgkin, Jonathan},
issn = {0192-253X},
journal = {Developmental Genetics},
number = {3},
pages = {240--250},
publisher = {Wiley},
title = {{Regulatory rearrangements and smg-sensitive allels of the C. elegans sex-determining gene tra-1}},
doi = {10.1002/dvg.1020150306},
volume = {15},
year = {1994},
}
@article{2713,
author = {László Erdös},
journal = {Duke Mathematical Journal},
number = {2},
pages = {541 -- 566},
publisher = {Duke University Press},
title = {{Estimates on stochastic oscillatory integrals and on the heat kernel of the magnetic Schrödinger operator}},
doi = {10.1215/S0012-7094-94-07619-9},
volume = {76},
year = {1994},
}
@article{1949,
abstract = {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).},
author = {Leonid Sazanov and Jackson, Julie B},
journal = {FEBS Letters},
number = {2-3},
pages = {109 -- 116},
publisher = {Elsevier},
title = {{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}},
doi = {10.1016/0014-5793(94)00370-X},
volume = {344},
year = {1994},
}
@article{1953,
abstract = {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.},
author = {Efanov, Alexander M and Koshkin, Aleksei A and Leonid Sazanov and Borodulina, O I and Varfolomeev, Sergei D and Zaǐtsev, Sergei V},
journal = {FEBS Letters},
number = {2},
pages = {114 -- 116},
publisher = {Elsevier},
title = {{Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism}},
doi = {10.1016/0014-5793(94)01109-5},
volume = {355},
year = {1994},
}
@inbook{3453,
abstract = {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.},
author = {von Kitzing, Eberhard and Peter Jonas and Sakmann, Bert},
booktitle = {Molecular and cellular mechanisms of neurotransmitter release},
editor = {Stjärne, Lennart and Greengard, Paul and Grillner, Sten E and Hökfelt, Tomas G M and Ottoson, David R},
pages = {235 -- 260},
publisher = {Raven Press},
title = {{Quantal analysis of excitatory postsynaptic currents at the hippocampal mossy fiber-CA3 pyramidal cell synapse}},
doi = {10.1016/0166-2236(95)90088-8},
volume = {29},
year = {1994},
}
@article{3460,
abstract = {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.},
author = {Peter Jonas and Spruston, Nelson},
journal = {Current Opinion in Neurobiology},
number = {3},
pages = {366 -- 372},
publisher = {Elsevier},
title = {{Mechanisms shaping glutamate-mediated excitatory postsynaptic currents in the CNS}},
doi = {10.1016/0959-4388(94)90098-1},
volume = {4},
year = {1994},
}
@article{3475,
abstract = {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.},
author = {Koh, Duk S and Peter Jonas and Vogel, Werner},
journal = {Journal of Physiology},
pages = {183 -- 197},
publisher = {Wiley-Blackwell},
title = {{Na+-activated K+ channels localized in the nodal region of myelinated axons of Xenopus}},
doi = {10.1113/jphysiol.1994.sp020287},
volume = {479},
year = {1994},
}