@inbook{4506,
abstract = {We propose a formal framework for designing hybrid systems by stepwise refinement. Starting with a specification in hybrid temporal logic, we make successively more transitions explicit until we obtain an executable system.},
author = {Thomas Henzinger and Manna, Zohar and Pnueli,Amir},
booktitle = {Hybrid Systems},
editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P and Rischel, Hans},
pages = {60 -- 76},
publisher = {Springer},
title = {{Towards refining temporal specifications into hybrid systems}},
doi = {10.1007/3-540-57318-6_24},
volume = {736},
year = {1993},
}
@article{4589,
abstract = {The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics that are suitable for reasoning about real-time systems, we combine this classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. The resulting theory of timed state sequences is shown to be decidable, albeit nonelementary, and its expressive power is characterized by ω-regular sets. Several more expressive variants are proved to be highly undecidable. This framework allows us to classify a wide variety of real-time logics according to their complexity and expressiveness. Indeed, it follows that most formalisms proposed in the literature cannot be decided. We are, however, able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and we present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.
Copyright © 1993 Academic Press. All rights reserved.},
author = {Alur, Rajeev and Thomas Henzinger},
journal = {Information and Computation},
number = {1},
pages = {35 -- 77},
publisher = {Elsevier},
title = {{Real-time logics: Complexity and expressiveness}},
doi = {10.1006/inco.1993.1025},
volume = {104},
year = {1993},
}
@inproceedings{4616,
abstract = {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},
author = {Alur, Rajeev and Thomas Henzinger and Ho, Pei-Hsin},
pages = {2 -- 11},
publisher = {IEEE},
title = {{Automatic symbolic verification of embedded systems}},
doi = {10.1109/REAL.1993.393520 },
year = {1993},
}
@inbook{4618,
abstract = {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.},
author = {Alur, Rajeev and Courcoubetis, Costas and Thomas Henzinger and Ho, Pei-Hsin},
booktitle = {Hybrid Systems},
editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P and Rischel, Hans},
pages = {209 -- 229},
publisher = {Springer},
title = {{Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}},
doi = {10.1007/3-540-57318-6_30},
volume = {736},
year = {1993},
}
@inproceedings{4619,
abstract = {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.},
author = {Alur, Rajeev and Thomas Henzinger and Vardi, Moshe Y},
pages = {592 -- 601},
publisher = {ACM},
title = {{Parametric real-time reasoning}},
doi = {10.1145/167088.167242},
year = {1993},
}
@inproceedings{4620,
abstract = {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.},
author = {Alur, Rajeev and Courcoubetis, Costas and Thomas Henzinger},
pages = {181 -- 193},
publisher = {Springer},
title = {{Computing accumulated delays in real-time systems}},
doi = {10.1007/3-540-56922-7_16},
volume = {697},
year = {1993},
}
@article{3446,
abstract = {An effective character recognition procedure implemented on a new type of hardware system and using a new architecture called CNND is proposed. This CNND contains one or more analog cellular neural networks (CNNs) and some digital logic, combining the advantages of the fast analog CNN signal processing and the fast and easy decision capability of digital logic. It is shown that the CNND system can be used for recognition of multifont printed or handwritten characters and could recognize 100,000 char/s with a recognition rate of more than 95%. The more advantage of the system over competing types is that there is not an extra feature extraction procedure implemented in slow hardware},
author = {Sziranyi, Tamas and Jozsef Csicsvari},
journal = {IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing},
number = {3},
pages = {223 -- 231},
publisher = {IEEE},
title = {{High-speed character recognition using a dual cellular neural network architecture (CNND)}},
doi = {10.1109/82.222823},
volume = {40},
year = {1993},
}
@inbook{3451,
author = {Peter Jonas},
booktitle = {Molecular Basis of Ion Channels and Receptors Involved in Nerve Excitation, Synaptic Transmission, and Muscle Contraction},
pages = {126 -- 135},
publisher = {New York Academy of Sciences},
title = {{Glutamate receptors in the central nervous system}},
volume = {707},
year = {1993},
}
@inbook{3452,
abstract = {In recent years, considerable progress in our understanding of the molecular events underlying excitatory synaptic transmission has been made. This progress was mainly achieved by technical advances, among them the patch-clamp technique in brain slices (Edwards et al., 1989), fast application of agonists (Franke et al., 1987), and cloning and functional expression of GluR channels of the nonNMDA type (e.g., Hollmann et al., 1989). A suitable model for studying excitatory postsynaptic currents (EPSCs) in the brain slice with patch-clamp techniques is the mossy fiber synapse on CA3 pyramidal cells of rat hippocampus (MF-CA3 synapse). This synapse is located close to the cell soma and should provide almost ideal space-clamp conditions. A comparison of MF-CA3 EPSCs with the currents activated by fast application of glutamate on membrane patches isolated from CA3 cell somata suggests that the concentration of glutamate in the synaptic cleft during excitatory synaptic transmission is high (about 1 mM) and that the transmitter remains in the synaptic cleft only briefly (about 1 ms). It seems likely that desensitization influences the peak amplitude of the EPSC in several ways. Brief pulses of glutamate cause desensitization, from which the glutamate receptor channels recover only slowly, and micromolar ambient glutamate concentrations produce desensitization at equilibrium. From the functional properties of recombinant GluR channels, in situ hybridization data, and patch-clamp experiments on different neuronal and nonneuronal cell types, a picture of the molecular identity of native channels emerges. In neurons of the hippocampus the pharmacological features of these channels were similar to recombinant channels assembled from subunits of the AMPA/kainate subtype which are strongly expressed in these cells. The native channels are characterized by outward rectification of the steady-state I-V and low Ca permeability, similar to recombinant channels containing the GluR-B subunit. This is consistent with the ubiquitous expression of this subunit in hippocampal neurones. In contrast, GluR channels from cerebellar glial cells, which uniquely in the central nervous system lack the expression of GluR-B subunits, show double rectification and high Ca permeability. The results suggest that the native functional nonNMDA glutamate receptor channels in the CNS are assembled form subunits of the AMPA/kainate subtype in a cell-specific way, with the functional properties of GluR channels in neurones being dominated by the GluR-B subunit.},
author = {Peter Jonas},
booktitle = {Nonselective cation channels: Pharmacology, Physiology and Biophysics.},
editor = {Siemen, Detlef},
pages = {61 -- 76},
publisher = {Birkhäuser},
title = {{AMPA-type glutamate receptors - nonselective cation channels mediating fast excitatory transmission in the CNS}},
volume = {66},
year = {1993},
}
@article{3473,
abstract = {Sixteen different K+ channel subtypes have been cloned from mammalian tissue. Considering their sequence homology to Drosophila Shaker, Shab, Shaw and Shal channels, they were classified into four corresponding classes Kv1-4. All K+ channels belonging to these classes consist of four subunits with each six hydrophobic segments (S1-S6) and a characteristic structure-function relationship of certain domains in their amino acid sequence. These domains are, the inactivation gate in the N-terminal region of the sequence, the voltage sensor in the fourth hydrophobic segment (S4), and the pore-region in the H5 segment between S5 and S6. In some functional properties K+ channels cloned from the mammalian brain, however, differ from Drosophila K+ channels. These are pharmacological differences, differences in the threshold of activation and in regulation of inactivation. Part of these differences are important to understand their physiological role in the brain. Based on their functional characteristics the expression pattern of cloned K+ channels in the rat brain can be correlated with the properties of K+ currents measured in central neurones.
Copyright © 1993 S. Karger AG, Basel},
author = {Ruppersberg, Peter and Ermler, Mamfred and Knopf, Martin and Kues, Wilfried and Peter Jonas and Koenen, Michael},
journal = {Cellular Physiology and Biochemistry},
pages = {250 -- 269},
publisher = {S. Karger AG},
title = {{Properties of Shaker-homologous potassium channels expressed in the mammalian brain.}},
doi = {10.1159/000154691},
volume = {3},
year = {1993},
}
@article{3474,
abstract = {1. Excitatory postsynaptic currents (EPSCs) were recorded in CA3 pyramidal cells of hippocampal slices of 15- to 24-day-old rats (22 degrees C) using the whole-cell configuration of the patch clamp technique. 2. Composite EPSCs were evoked by extracellular stimulation of the mossy fibre tract. Using the selective blockers 6-cyano-7-nitroquinoxaline-2,3-dione (CNQX) and D-2-amino-5-phosphonopentanoic acid (APV), a major alpha-amino-3-hydroxy-5-methylisoxazole-4-propionate (AMPA)/kainate receptor-mediated component and a minor NMDA receptor-mediated component with slower time course were distinguished. For the AMPA/kainate receptor-mediated component, the peak current-voltage (I-V) relation was linear, with a reversal potential close to 0 mV. The half-maximal blocking concentration of CNQX was 353 nM. 3. Unitary EPSCs of the mossy fibre terminal (MF)-CA3 pyramidal cell synapse were evoked at membrane potentials of -70 to -90 mV by low-intensity extracellular stimulation of granule cell somata using fine-tipped pipettes. The EPSC peak amplitude as a function of stimulus intensity showed all-or-none behaviour. The region of low threshold was restricted to a few micrometres. This suggests that extracellular stimulation was focal, and that the stimulus-evoked EPSCs were unitary. 4. Latency and rise time histograms of EPSCs evoked by granule cell stimulation showed narrow unimodal distributions within each experiment. The mean latency was 4.2 +/- 1.0 ms, and the mean 20-80% rise time was 0.6 +/- 0.1 ms (23 cells). When fitted within the range 0.7 ms to 20 ms after the peak, the decay of the EPSCs with the fastest rise (rise time 0.5 ms or less) could be described by a single exponential function; the mean time constant was in the range 3.0-6.6 ms with a mean of 4.8 ms (8 cells). 5. Peak amplitudes of the EPSCs evoked by suprathreshold granule cell stimulation fluctuated between trials. The apparent EPSC peak conductance in normal extracellular solution (2 mM Ca2+, 1 mM Mg2+), excluding failures, was 1 nS. Reducing the Ca2+ concentration and increasing the Mg2+ concentration reduced the mean peak amplitude in a concentration-dependent manner. 6. Peaks in EPSC peak amplitude distributions were apparent in low Ca2+ and high Mg2+. Using the criteria of equidistance and the presence of peaks and dips in the autocorrelation function, five of nine EPSC peak amplitude distributions were judged to be quantal.},
author = {Peter Jonas and Major, Guy and Sakmann, Bert},
journal = {Journal of Physiology},
pages = {615 -- 663},
publisher = {Wiley-Blackwell},
title = {{Quantal components of unitary EPSCs at the mossy fibre synapse on CA3 pyramidal cells of rat hippocampus}},
doi = {10.1113/jphysiol.1993.sp019965},
volume = {472},
year = {1993},
}
@inbook{3568,
author = {Herbert Edelsbrunner},
booktitle = {Handbook of Convex Geometry},
pages = {699 -- 735},
publisher = {North Holland},
title = {{Geometric algorithms}},
year = {1993},
}
@inbook{3569,
author = {Herbert Edelsbrunner},
booktitle = {Current Trends in Theoretical Computer Science, Essays and Tutorials},
pages = {1 -- 48},
publisher = {World Scientific Publishing},
title = {{Computational geometry}},
doi = {10.1007/978-3-662-04245-8_1},
year = {1993},
}
@article{3643,
abstract = {We investigate the establishment and spread of new adaptive peaks within Wright's ‘shifting balance’. The third phase of the ‘shifting balance’ involves a kind of group selection, since demes in which a superior peak has been established contain more individuals, and so send out more migrants. We assume that population size, N, increases with mean fitness, , according to the exponential relation, . Here, k is a measure of the weakness of density-dependent regulation, and equals the inverse of the regression of log (fitness) on log(N). In the island model, we find that just as with soft selection (k = 0), two distinct types of behaviour exist: group selection makes no qualitative difference. With low numbers of migrants, demes fluctuate almost independently, and only one equilibrium exists. With large numbers of migrants, all the demes evolve towards the same adaptive peak, and so the whole population can move towards one or other of the peaks. Group selection can be understood in terms of an effective mean fitness function. Its main consequence is to increase the effect of selection relative to drift (Ns), and so increase the bias towards the fitter peak. However, this increased bias depends on the ratio between k and the deme size (k/N), and so is very small when density-dependence is reasonably strong.},
author = {Rouhani, Shahin and Nicholas Barton},
journal = {Genetical Research},
number = {2},
pages = {127 -- 136},
publisher = {Cambridge University Press},
title = {{Group selection and the 'shifting balance'}},
doi = {10.1017/S0016672300031232},
volume = {61},
year = {1993},
}
@article{3644,
author = {Nicholas Barton and Rouhani, Shahin},
journal = {Genetical Research},
number = {1},
pages = {57 -- 74},
publisher = {Cambridge University Press},
title = {{Adaptation and the 'shifting balance'}},
doi = {10.1017/S0016672300031098 },
volume = {61},
year = {1993},
}
@article{4036,
abstract = {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.},
author = {Chazelle, Bernard and Herbert Edelsbrunner and Guibas, Leonidas and Sharir, Micha and Snoeyink, Jack},
journal = {SIAM Journal on Computing},
number = {6},
pages = {1286 -- 1302},
publisher = {SIAM},
title = {{Computing a face in an arrangement of line segments and related problems}},
doi = {10.1137/0222077 },
volume = {22},
year = {1993},
}
@article{4040,
abstract = {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.},
author = {Herbert Edelsbrunner and Tan, Tiow Seng},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {197 -- 213},
publisher = {Springer},
title = {{An upper bound for conforming Delaunay triangulations}},
doi = {10.1007/BF02573974},
volume = {10},
year = {1993},
}
@article{4041,
abstract = {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.},
author = {Herbert Edelsbrunner and Seidel, Raimund and Sharir, Micha},
journal = {SIAM Journal on Computing},
number = {2},
pages = {418 -- 429},
publisher = {SIAM},
title = {{On the zone theorem for hyperplane arrangements}},
doi = {10.1137/0222031},
volume = {22},
year = {1993},
}
@article{4042,
abstract = {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.},
author = {Herbert Edelsbrunner and Tan, Tiow Seng},
journal = {SIAM Journal on Computing},
number = {3},
pages = {527 -- 551},
publisher = {SIAM},
title = {{A quadratic time algorithm for the minmax length triangulation}},
doi = {10.1137/0222036 },
volume = {22},
year = {1993},
}
@article{4044,
abstract = {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.},
author = {Bern, Marshall and Herbert Edelsbrunner and Eppstein, David and Mitchell, Stephen and Tan, Tiow Seng},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {47 -- 65},
publisher = {Springer},
title = {{Edge insertion for optimal triangulations}},
doi = {10.1007/BF02573962},
volume = {10},
year = {1993},
}