@article{2560,
abstract = {Chemical irritation of the urinary bladder with formalin in the rat induced c-fos protein-like immunoreactivity in more than 80% of substance P receptor-like immunoreactive (SPR-LI) neurons of the dorsal commissural nucleus, sacral parasympathetic nucleus and lamina I in the 6th lumbar and 1st sacral cord segments. These neurons with SPR-LI may receive noxious information from the urinary bladder through the primary afferent fibers with substance P.},
author = {Lü, Yan and Jin, Shan-Xue and Xu, Tian-Le and Qin, Bing-Zhi and Li, Ji-Shuo and Ding, Yu-Qiang and Ryuichi Shigemoto and Mizuno, Noboru},
journal = {Neuroscience Letters},
number = {2},
pages = {139 -- 142},
publisher = {Elsevier},
title = {{Expression of c-fos protein in substance P receptor-like immunoreactive neurons in response to noxious stimuli on the urinary bladder: an observation in the lumbosacral cord segments of the rat}},
doi = {10.1016/0304-3940(95)11991-5},
volume = {198},
year = {1995},
}
@article{2724,
abstract = {We study the generalizations of the well-known Lieb-Thirring inequality for the magnetic Schrödinger operator with nonconstant magnetic field. Our main result is the naturally expected magnetic Lieb-Thirring estimate on the moments of the negative eigenvalues for a certain class of magnetic fields (including even some unbounded ones). We develop a localization technique in path space of the stochastic Feynman-Kac representation of the heat kernel which effectively estimates the oscillatory effect due to the magnetic phase factor.},
author = {László Erdös},
journal = {Communications in Mathematical Physics},
number = {3},
pages = {629 -- 668},
publisher = {Springer},
title = {{Magnetic Lieb-Thirring inequalities}},
doi = {10.1007/BF02099152},
volume = {170},
year = {1995},
}
@inproceedings{2712,
abstract = {We study the generalizations of the well-known Lieb-Thirring inequality for the magnetic Schrödinger operator with a nonconstant magnetic field. We use stochastic methods to prove estimates on the moments of the negative eigenvalues.},
author = {László Erdös},
pages = {127 -- 132},
publisher = {Birkhäuser},
title = {{Magnetic Lieb-Thirring inequalities and stochastic oscillatory integrals}},
doi = {10.1007/978-3-0348-9092-2_13},
volume = {78},
year = {1995},
}
@inbook{3455,
author = {Peter Jonas},
booktitle = {Single-channel recording},
editor = {Sakmann, Bert and Neher, Erwin},
pages = {231 -- 243},
publisher = {Plenum},
title = {{Fast application of agonists to isolated membrane patches}},
year = {1995},
}
@article{3638,
abstract = {Any sample of genes traces back to a single common ancestor. Each gene also has other properties: its sequence, its geographic location and the phenotype and fitness of the organism that carries it. With sexual reproduction, different genes have different genealogies, which gives us much more information, but also greatly complicates population genetic analysis. We review the close relation between the distribution of genealogies and the classic theory of identity by descent in spatially structured populations, and develop a simple diffusion approximation to the distribution of coalescence times in a homogeneous two-dimensional habitat. This shows that when neighbourhood size is large (as in most populations) only a small fraction of pairs of genes are closely related, and only this fraction gives information about current rates of gene flow. The increase of spatial dispersion with lineage age is thus a poor estimator of gene flow. The bulk of the genealogy depends on the long-term history of the population; we discuss ways of inferring this history from the concordance between genealogies across loci.},
author = {Nicholas Barton and Wilson, I},
journal = {Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences},
number = {1327},
pages = {49 -- 59},
publisher = {Royal Society, The},
title = {{Genealogies and geography}},
doi = {10.1098/rstb.1995.0090},
volume = {349},
year = {1995},
}
@article{3640,
abstract = {The probability of fixation of a favorable mutation is reduced if selection at other loci causes inherited variation in fitness. A general method for calculating the fixation probability of an allele that can find itself in a variety of genetic backgrounds is applied to find the effect of substitutions, fluctuating polymorphisms, and deleterious mutations in a large population. With loose linkage, r, the effects depend on the additive genetic variance in relative fitness, var(W), and act by reducing effective population size by (N/Ne) = 1 + var(W)/2r2. However, tightly linked loci can have a substantial effect not predictable from Ne. Linked deleterious mutations reduce the fixation probability of weakly favored alleles by exp (-2U/R), where U is the total mutation rate and R is the map length in Morgans. Substitutions can cause a greater reduction: an allele with advantage s < scrit = (pi 2/6) loge (S/s) [var(W)/R] is very unlikely to be fixed. (S is the advantage of the substitution impeding fixation.) Fluctuating polymorphisms at many (n) linked loci can also have a substantial effect, reducing fixation probability by exp [square root of 2Kn var(W)/R] [K = -1/E((u-u)2/uv) depending on the frequencies (u,v) at the selected polymorphisms]. Hitchhiking due to all three kinds of selection may substantially impede adaptation that depends on weakly favored alleles.},
author = {Nicholas Barton},
journal = {Genetics},
number = {2},
pages = {821 -- 841},
publisher = {Genetics Society of America},
title = {{Linkage and the limits to natural selection}},
doi = {http://www.genetics.org/content/140/2/821.long},
volume = {140},
year = {1995},
}
@inproceedings{3551,
abstract = {Common geometric models for proteins and other molecules are the space filling diagram, the solvent accessible surface, and the molecular surface. We describe software that computes metric properties of these models, including volume and surface area. It also measures voids or empty space enclosed by the protein, and it keeps track of surface area contributions of individual atoms. The software is based on 3-dimensional alpha complexes and on inclusion-exclusion formulas with terms derived from the simplices in this complex.},
author = {Herbert Edelsbrunner and Facello, Michael and Fu, Ping and Liang, Jie},
pages = {256 -- 264},
publisher = {IEEE},
title = {{Measuring proteins and voids in proteins}},
doi = {10.1109/HICSS.1995.375331},
year = {1995},
}
@article{3479,
abstract = {1. Glutamate receptor (GluR) channels were studied in basket cells in the dentate gyrus of rat hippocampal slices. Basket cells were identified by their location, dendritic morphology and high frequency of action potentials generated during sustained current injection. 2. Dual-component currents were activated by fast application of glutamate to outside-out membrane patches isolated from basket cell somata (10 μM glycine, no external Mg2+). The fast component was selectively blocked by 6-cyano-7-nitroquinoxaline-2,3-dione (CNQX), the slow component by D-2-amino-5-phosphonopentanoic acid (D-AP5). This suggests that the two components were mediated by α-amino-3-hydroxy-5-methyl-4-isoxazolepropionate receptor (AMPAR)/kainate receptor and N-methyl-D-aspartate receptor (NMDAR) channels, respectively. The mean ratio of the peak current of the NMDAR component to that of the AMPAR/kainate receptor component was 0.22 (1 ms pulses of 10 mM glutamate). 3. The AMPAR/kainate receptor component, which was studied in isolation in the presence of D-AP5, was identified as AMPAR mediated on the basis of the preferential activation by AMPA as compared with kainate, the weak desensitization of kainate-activated currents, the cross-desensitization between AMPA and kainate, and the reduction of desensitization by cyclothiazide. 4. Deactivation of basket cell AMPARs following 1 ms pulses of glutamate occurred with a time constant (τ) of 1.2 ± 0.1 ms (mean ± S.E.M.). During 100 ms glutamate pulses, AMPARs desensitized with a τ of 3.7 ± 0.2 ms. 5. The peak current-voltage (I-V) relation of AMPAR-mediated currents in Na+-rich extracellular solution showed a reversal potential of -4.0 ± 2.6 mV and was characterized by a doubly rectifying shape. The conductance of single AMPAR channels was estimated as 22.6 ± 1.6 pS using non-stationary fluctuation analysis. AMPARs expressed in hippocampal basket cells mere highly Ca2+ permeable (P(Ca)/P(K) = 1.79). 6. NMDARs in hippocampal basket cells were studied in isolation in the presence of CNQX. Deactivation of NMDARs activated by glutamate pulses occurred bi-exponentially with mean τ values of 266 ± 23 ms (76%) and 2620 ± 383 ms (24%). 7. The peak I-V relation of the NMDAR-mediated component in Na+-rich extracellular solution showed a reversal potential of 1.5 ± 0.6 mV and a region of negative slope at negative membrane potentials in the presence of external Mg2+, due to voltage-dependent block by these ions. The conductance of single NMDAR channels in the main open state was 50.2 ± 1.8 pS. NMDARs in hippocampal basket cells were highly permeable to Ca2+ (P(Ca)/P(K) = 6.68). 8. AMPARs in hippocampal basket cells are characterized by about threefold faster kinetics and twentyfold higher Ca2+ permeability than AMPARs in hippocampal granule or pyramidal cells. Simulations show that the Ca2+ influx through basket cell AMPARs is comparable to that through NMDARs at negative membrane potentials with physiological concentrations of Ca2+ and Mg2+. This suggests a dual pathway of synaptically mediated Ca2+ entry into interneurones.},
author = {Koh, Duk S and Geiger, Jörg R and Peter Jonas and Sakmann, Bert},
journal = {Journal of Physiology},
number = {Pt 2},
pages = {383 -- 402},
publisher = {Wiley-Blackwell},
title = {{Ca(2+)-permeable AMPA and NMDA receptor channels in basket cells of rat hippocampal dentate gyrus}},
doi = {10.1113/jphysiol.1995.sp020737},
volume = {485},
year = {1995},
}
@article{3481,
abstract = {1. The influence of intracellular factors on current rectification of different subtypes of native α-amino-3-hydroxy-5-methyl-4-isoxazolepropionate receptors (AMPARs) was studied in rat brain slices by combining fast application of glutamate with patch pipette perfusion. 2. The peak current-voltage (I-V) relation of the AMPARs expressed in Bergmann glial cells of cerebellum and dentate gyrus (DG) basket cells of hippocampus was weakly rectifying in outside-out patches and nystatin-perforated vesicles, but showed a doubly rectifying shape with a region of reduced slope between 0 and +40 mV in nucleated patches. The I-V relation of AMPARs expressed in hippocampal CA3 pyramidal neurones was linear in all recording configurations. 3. Intracellular application of 2.5 μM spermine, a naturally occurring polyamine, blocked outward currents in outside-oat patches from Bergmann glial cells and DG basket cells in a voltage-dependent manner, generating I-V relations with a doubly rectifying shape which were similar to those recorded in nucleated patches. AMPARs in CA3 pyramidal cell patches were unaffected by 25 μM spermine. 4. The half-maximal blocking concentration of spermine at +40 mV was 0.3 μM in Bergmann glial cell patches and 1.5 μM in DG basket cell patches, whereas it was much higher (≥ 100 μM) for CA3 pyramidal. cell patches. Spermidine also affected current rectification, but with lower affinity. The block of outward current by polyamines following voltage jumps developed within < 0.5 ms. 5. We conclude that current rectification, rather than being an intrinsic property of the Ca2+ permeable AMPAR channel, is generated by polyamine block.},
author = {Koh, Duk S and Burnashev, Nail A and Peter Jonas},
journal = {Journal of Physiology},
number = {Pt 2},
pages = {305 -- 312},
publisher = {Wiley-Blackwell},
title = {{Block of native Ca(2+)-permeable AMPA receptors in rat brain by intracellular polyamines generates double rectification}},
doi = {10.1113/jphysiol.1995.sp020813},
volume = {486},
year = {1995},
}
@article{4028,
abstract = {Efficient algorithms are described for computing topological, combinatorial, and metric properties of the union of finitely many spherical balls in R(d) These algorithms are based on a simplicial complex dual to a decomposition of the union of balls using Voronoi cells, and on short inclusion-exclusion formulas derived from this complex. The algorithms are most relevant in R(3) where unions of finitely many balls are commonly used as models of molecules.},
author = {Herbert Edelsbrunner},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {415 -- 440},
publisher = {Springer},
title = {{The union of balls and its dual shape}},
doi = {10.1007/BF02574053},
volume = {13},
year = {1995},
}
@article{4035,
abstract = {Let S be a set of n points in ℝd . A set W is a weak ε-net for (convex ranges of)S if, for any T⊆S containing εn points, the convex hull of T intersects W. We show the existence of weak ε-nets of size {Mathematical expression}, where β2=0, β3=1, and βd ≈0.149·2d-1(d-1)!, improving a previous bound of Alon et al. Such a net can be computed effectively. We also consider two special cases: when S is a planar point set in convex position, we prove the existence of a net of size O((1/ε) log1.6(1/ε)). In the case where S consists of the vertices of a regular polygon, we use an argument from hyperbolic geometry to exhibit an optimal net of size O(1/ε), which improves a previous bound of Capoyleas.},
author = {Chazelle, Bernard and Herbert Edelsbrunner and Grigni, Michelangelo and Guibas, Leonidas and Sharir, Micha and Welzl, Emo},
journal = {Discrete & Computational Geometry},
number = {1},
pages = {1 -- 15},
publisher = {Springer},
title = {{Improved bounds on weak ε-nets for convex sets}},
doi = {10.1007/BF02574025},
volume = {13},
year = {1995},
}
@article{1943,
abstract = {Transhydrogenase from beef-heart mitochondria was solubilised with Triton X-100 and purified by column chromatography. The detergent-dispersed enzyme catalysed the reduction of acetylpyridine adenine dinucleotide (AcPdAD+) by NADH, but only in the presence of NADP+. Experiments showed that this reaction was cyclic; NADP(H), whilst remaining bound to the enzyme, was alternately reduced by NADH and oxidised by AcPdAD+. A period of incubation of the enzyme with NADPH at pH 6.0 led to inhibition of the simple transhydrogenation reaction between AcPdAD+ and NADPH. However, after such treatment, transhydrogenase acquired the ability to catalyse the (NADPH-dependent) reduction of AcPdAD+ by NADH. It is suggested that this is a similar cycle to the one described above. Evidently, the binding affinity for NADP+ increases as a consequence of the inhibition process resulting from prolonged incubation with NADPH. The pH dependences of simple and cyclic transhydrogenation reactions are described. Though more complex than those in Escherichia coli transhydrogenase, they are consistent with the view [Hutton, M., Day, J.M., Bizouarn, T. and Jackson, J.B. (1994) Eur. J. Biochem. 219, 1041–10511] that, also in the mitochondrial enzyme, binding the release of NADP+ and NADP are accompanied by binding and release of a proton. The enzyme was successfully reconstituted into liposomes by a cholate dilution procedure. The proteoliposomes catalysed cyclic NADPH-dependent reduction of AcPdAD+ by NADH only when they were tightly coupled. However, they catalysed cyclic NADP+-dependent reduction of AcPdAD+ by NADH only when they were uncoupled eg. by addition of carbonylcyanide-p-trifluoromethoxyphenyl hydrazone. These observations are evidence that the proton binding and release which accompany NADP+ binding and release, respectively, take place on the inside of the vesicle, and that they are components of the electrogenic processes of the enzyme.},
author = {Leonid Sazanov and Jackson, Baz J},
journal = {Biochimica et Biophysica Acta - Bioenergetics},
number = {3},
pages = {304 -- 312},
publisher = {Elsevier},
title = {{Cyclic reactions catalysed by detergent-dispersed and reconstituted transhydrogenase from beef heart mitochondria; implications for the mechanism of proton translocation}},
doi = {10.1016/0005-2728(95)00096-2},
volume = {1231},
year = {1995},
}
@article{2559,
abstract = {Taking advantage of the restricted expression of metabotropic glutamate receptor subtype 6 (mGIuR6) in retinal ON bipolar cells, we generated knockout mice lacking mGIuR6 expression. The homozygous mutant mice showed a loss of ON responses but unchanged OFF responses to light. The mutant mice displayed no obvious changes in retinal cell organization nor in the projection of optic fibers to the brain. Furthermore, the mGIuR6-deficient mice showed visual behavioral responses to light stimulation as examined by shuttle box avoidance behavior experiments using light exposure as a conditioned stimulus. The results demonstrate that mGIuR6 is essential in synaptic transmission to the ON bipolar cell and that the OFF response provides an important means for transmitting visual information.},
author = {Masu, Masayuki and Iwakabe, Hideki and Tagawa, Yoshiaki and Miyoshi, Tomomitsu and Yamashita, Masayuki and Fukuda, Yutaka and Sasaki, Hitoshi and Hiroi, Kano and Nakamura, Yasuhisa and Ryuichi Shigemoto and Takada, Masahiko and Nakamura, Kenji and Nakao, Kazuki and Katsuki, Motoya and Nakanishi, Shigetada},
journal = {Cell},
number = {5},
pages = {757 -- 765},
publisher = {Cell Press},
title = {{Specific deficit of the ON response in visual transmission by targeted disruption of the mGIuR6 gene}},
doi = {10.1016/0092-8674(95)90354-2},
volume = {80},
year = {1995},
}
@article{2561,
abstract = {An antibody which recognizes specifically a metabotropic glutamate receptor, mGluR7, was produced by using a trpE fusion protein containing a C-terminal sequence of rat mGluR7. Neuropil in laminae I and II of the dorsal horn of the rat, as well as many neuronal cell bodies in the dorsal root ganglion, showed mGluR7-like immunoreactivity; the immunoreactivity in neuropil was seen in axon terminals, which were filled with round synaptic vesicles and constituted axodendritic and axosomatic asymmetric synapses. The mGluR7-like immunoreactivity in laminae I and II in the dorsal horn was reduced after dorsal rhizotomy. The results indicate that some axon terminals of the primary afferent fibers to laminae I and II of the dorsal horn are provided with mGluR7.},
author = {Ohishi, Hitoshi and Nomura, Sakashi and Ding, Yu-Qiang and Ryuichi Shigemoto and Wada, Eiki and Kinoshita, Ayae and Li, Jin-Lian and Neki, Akio and Nakanishi, Shigetada and Mizuno, Noboru},
journal = {Neuroscience Letters},
number = {1-2},
pages = {85 -- 88},
publisher = {Elsevier},
title = {{Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study in the rat}},
doi = {10.1016/0304-3940(95)12207-9},
volume = {202},
year = {1995},
}
@inbook{2465,
author = {Morris, David A and Jirí Friml and Zažímalová, Eva},
booktitle = {Plant Hormones: Biosynthesis, Signal Transduction, Action!},
editor = {Davies, Peter J},
pages = {451 -- 484},
publisher = {Kluwer},
title = {{Auxin transport}},
doi = {10.1007/978-1-4020-2686-7_21},
year = {1995},
}
@article{2491,
abstract = {The distribution of mRNAs for metabotropic glutamate receptors, mGluR4 and mGluR7, which are highly sensitive for L-2-amino-4-phosphonobutyrate (L- AP4), was examined in the central nervous system of the rat by in situ hybridization. In general, the hybridization signals of mGluR7 mRNA were more widely distributed than those of mGluR4 mRNA, and differential expression of mGluR4 mRNA and mGluR7 mRNA was clearly indicated in some brain regions. Intense or moderate expression of mGluR4 mRNA was detected in the granule cells of the olfactory bulb and cerebellum, whereas no significant expression of mGluR7 mRNA was found in these cells. In other neurons or regions where mGluR7 mRNA was intensely or moderately expressed, no significant expression of mGluR4 mRNA was observed. Such were the mitral and tufted cells of the olfactory bulb; anterior olfactory nucleus; neocortical regions; cingulate cortex; retrosplenial cortex; piriform cortex; perirhinal cortex; CA1; CA3; granule cells of the dentate gyrus; superficial layers of the subicular cortex; deep layers of the entorhinal, parasubicular, and presubicular cortices; ventral part of the lateral septal nucleus; septohippocampal nucleus; triangular septal nucleus; nuclei of the diagonal band; bed nucleus of the stria terminalis; ventral pallidum; claustrum; amygdaloid nuclei other than the intercalated nuclei; preoptic region; hypothalamic nuclei other than the medial mammillary nucleus; ventral lateral geniculate nucleus; locus coeruleus; Purkinje cells; many nuclei of the lower brainstem other than the superior colliculus, periaqueductal gray, interpeduncular nucleus, pontine nuclei, and dorsal cochlear nucleus; and dorsal horn of the spinal cord. Both mGluR4 mRNA and mGluR7 mRNA were moderately or intensely expressed in the olfactory tubercle, superficial layers of the entorhinal cortex, CA4, septofimbrial nucleus, intercalated nuclei of the amygdala, medial mammillary nucleus, many thalamic nuclei, and pontine nuclei. Intense expression of both mGluR4 mRNA and mGluR7 mRNA was further detected in the trigeminal ganglion and dorsal root ganglia, whereas no significant expression of them was found in the pterygopalatine ganglion and superior cervical ganglion. The results indicate differential roles of the L-AP4-sensitive metabotropic glutamate receptors in the glutamatergic nervous system.},
author = {Ohishi, Hitoshi and Akazawa, Chihiro and Ryuichi Shigemoto and Nakanishi, Shigetada and Mizuno, Noboru},
journal = {Journal of Comparative Neurology},
number = {4},
pages = {555 -- 570},
publisher = {Wiley-Blackwell},
title = {{Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic glutamate receptors, mGluR4 and mGluR7, in the rat brain}},
doi = {10.1002/cne.903600402},
volume = {360},
year = {1995},
}
@article{3639,
abstract = {A general representation of multilocus selection is extended to allow recombination to depend on genotype. The equations simplify if modifier alleles have small effects on recombination. The evolution of such modifiers only depends on how they alter recombination between the selected loci, and does not involve dominance in modifier effects. The net selection on modifiers can be found explicitly if epistasis is weak relative to recombination. This analysis shows that recombination can be favoured in two ways: because it impedes the response to epistasis which fluctuates in sign, or because it facilitates the response to directional selection. The first mechanism is implausible, because epistasis must change sign over periods of a few generations: faster or slower fluctuations favour reduced recombination. The second mechanism requires weak negative epistasis between favourable alleles, which may either be increasing, or held in check by mutation. The selection (si) on recombination modifiers depends on the reduction in additive variance of log (fitness) due to linkage disequilibria (υ1 < 0), and on non-additive variance in log (fitness) (V′2, V′3,.. epistasis between 2, 3.. loci). For unlinked loci and pairwise epistasis, si = − (υ1 + 4V2/3)δr, where δr is the average increase in recombination caused by the modifier. The approximations are checked against exact calculations for three loci, and against Charlesworth's analyses of mutation/selection balance (1990), and directional selection (1993). The analysis demonstrates a general relation between selection on recombination and observable components of fitness variation, which is open to experimental test.},
author = {Nicholas Barton},
journal = {Genetical Research},
number = {2},
pages = {123 -- 144},
publisher = {Cambridge University Press},
title = {{A general model for the evolution of recombination}},
doi = {10.1017/S0016672300033140},
volume = {65},
year = {1995},
}
@inproceedings{3552,
abstract = {The concept of an α-shape of a finite set of points in R^d, with weights, is defined and illustrated. An α-shape is a polytope which is not necessarily convex nor connected and can be derived from the (weighted) Delaunay triangulation of the point set, with a parameter controlling the desired level of detail. The set of all α values leads to a descrete family of shapes capturing the intuitive notion of ``crude'' versus ``fine'' shapes of a point set. Software that computes such shapes in R^2 and R^3 is available via anonymous ftp from:
ftp://ftp.ncsa.uiuc.edu/Visualization/Alpha-shape/ },
author = {Akkiraju, Nataraj and Herbert Edelsbrunner and Facello, Michael and Fu, Ping and Mücke, Ernst P and Varela, Carlos},
pages = {63 -- 66},
publisher = {Elsevier},
title = {{Alpha shapes: definition and software}},
year = {1995},
}
@article{4029,
abstract = {A general and direct method for computing the Betti numbers of a finite simplicial complex in Bd is given. This method is complete for d less than or equal to 3, where versions of this method run in time O(n alpha(n)) and O(n), n the number of simplices. An implementation of the algorithm is applied to alpha shapes, which is a novel geometric modeling tool.},
author = {Delfinado, Cecil J and Herbert Edelsbrunner},
journal = {Computer Aided Geometric Design},
number = {7},
pages = {771 -- 784},
publisher = {Elsevier},
title = {{An incremental algorithm for Betti numbers of simplicial complexes on the 3-sphere}},
doi = {10.1016/0167-8396(95)00016-Y},
volume = {12},
year = {1995},
}
@phdthesis{4428,
abstract = {Hybrid systems are real-time systems that react to both discrete and continuous activities (such as analog signals, time, temperature, and speed). Typical examples of hybrid systems are embedded systems, timing-based communication protocols, and digital circuits at the transistor level. Due to the rapid development of microprocessor technology, hybrid systems directly control much of what we depend on in our daily lives. Consequently, the formal specification and verification of hybrid systems has become an active area of research. This dissertation presents the first general framework for the formal specification and verification of hybrid systems, as well as the first hybrid-system analysis tool--HyTech. The framework consists of a graphical finite-state-machine-like language for modeling hybrid systems, a temporal logic for modeling the requirements of hybrid systems, and a computer procedure that verifies modeled hybrid systems against modeled requirements. The tool HyTech is the implementation of the framework using C++ and Mathematica.
More specifically, our hybrid-system modeling language, Hybrid Automata, is an extension of timed automata with discrete and continuous variables whose dynamics are governed by differential equations. Our requirement modeling language, ICTL, is a branching-time temporal logic, and is an extension of TCTL with stop-watch variables. Our verification procedure is a symbolic model-checking procedure that verifies linear hybrid automata against ICTL formulas. To make HyTech more efficient and effective, we use model-checking strategies and abstract operators that can expedite the verification process. To enable HyTech to verify nonlinear hybrid automata, we introduce two translations from nonlinear hybrid automata to linear hybrid automata. We have applied HyTech to analyze more than 30 hybrid-system benchmarks. In this dissertation, we present the application of HyTech to three nontrivial hybrid systems taken from the literature.},
author = {Ho, Pei-Hsin},
pages = {1 -- 188},
publisher = {Cornell University},
title = {{Automatic Analysis of Hybrid Systems}},
doi = {CSD-TR95-1536},
year = {1995},
}