@inproceedings{4426, abstract = {We use linear hybrid automata to define linear approximations of the phase portraits of nonlinear hybrid systems. The approximating automata can be analyzed automatically using the symbolic model checker HyTech. We demonstrate the technique through the study of predator-prey systems, where we compute population bounds for both species. We also identify a class of nonlinear hybrid automata for which linear phase-portrait approximations can be generated automatically.}, author = {Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Hybrid Systems III: Verification and Control}, editor = {Alur, Rajeev and Henzinger, Thomas A and Sontag, Eduardo}, isbn = {9783540611554}, pages = {377 -- 388}, publisher = {Springer}, title = {{Linear phase-portrait approximations for nonlinear hybrid systems}}, doi = {10.1007/BFb0020961}, volume = {1066}, year = {1996}, } @inbook{4427, abstract = {We model a steam-boiler control system using hybrid automata. We provide two abstracted linear models of the nonlinear behavior of the boiler. For each model, we define and verify a controller that maintains safe operation of the boiler. The less abstract model permits the design of a more efficient controller. We also demonstrate how the tool HyTech can be used to automatically synthesize control parameter constraints that guarantee safety of the boiler.}, author = {Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control}, isbn = {9783540495666}, pages = {265 -- 282}, publisher = {Springer}, title = {{Using HyTech to synthesize control parameters for a steam boiler}}, doi = {10.1007/BFb0027241}, volume = {1165}, year = {1996}, } @inproceedings{4443, abstract = {Three natural equivalence relations on the infinite state space of a hybrid automaton are language equivalence, simulation equivalence, and bisimulation equivalence. When one of these equivalence relations has a finite quotient, certain model checking and controller synthesis problems are decidable. When bounds on the number of equivalence classes are obtained, bounds on the running times of model checking and synthesis algorithms follow as corollaries. We characterize the time-abstract versions of these equivalence relations on the state spaces of rectangular hybrid automata (RHA), in which each continuous variable is a clock with bounded drift. These automata are useful for modeling communications protocols with drifting local clocks, and for the conservative approximation of more complex hybrid systems. Of our two main results, one has positive implications for automatic verification, and the other has negative implications. On the positive side, we find that the (finite) language equivalence quotient for RHA is coarser than was previously known by a multiplicative exponential factor. On the negative side, we show that simulation equivalence for RHA is equality (which obviously has an infinite quotient). Our main positive result is established by analyzing a subclass of timed automata, called one-sided timed automata (OTA), for which the language equivalence quotient is coarser than for the class of all timed automata. An exact characterization of language equivalence for OTA requires a distinction between synchronous and asynchronous definitions of (bi)simulation: if time actions are silent, then the induced quotient for OTA is coarser than if time actions (but not their durations) are visible.}, author = {Henzinger, Thomas A and Kopke, Peter}, booktitle = {7th International Conference on Concurrency Theory}, isbn = {9783540616047}, location = {Pisa, Italy}, pages = {530 -- 545}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{State equivalences for rectangular hybrid automata}}, doi = {10.1007/3-540-61604-7_74}, volume = {1119}, year = {1996}, } @inproceedings{4495, abstract = {In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The main practical limitation of model checking is caused by the size of the state space of the program, which grows exponentially with the number of concurrent components. This problem, known as the state-explosion problem, becomes more difficult when we consider real-time model checking, where the program and the specification involve quantitative references to time. In particular, when use timed automata to describe real-time programs and we specify timed behaviors in the logic TCTL, a real-time extension of the temporal logic CTL with clock variables, then the state space under consideration grows exponentially not only with the number of concurrent components, but also with the number of clocks and the length of the clock constraints used in the program and the specification. Two powerful methods for coping with the state-explosion problem are on-the-fly and space-efficient model checking. In on-the-fly model checking, we explore only the portion of the state space of the program whose exploration is essential for determining the satisfaction of the specification. In space-efficient model checking, we store in memory the minimal information required, preferring to spend time on reconstructing information rather than spend space on storing it. In this work we develop an automata-theoretic approach to TCTL model checking that combines both methods. We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for TCTL.}, author = {Henzinger, Thomas A and Kupferman, Orna and Vardi, Moshe}, booktitle = {7th International Conference on Concurrency Theory}, isbn = {978-3-540-70625-0}, location = {Pisa, Italy}, pages = {514 -- 529}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{A space-efficient on-the-fly algorithm for real-time model checking}}, doi = {10.1007/3-540-61604-7_73}, volume = {1119}, year = {1996}, } @inproceedings{4519, abstract = {We summarize several recent results about hybrid automata. Our goal is to demonstrate that concepts from the theory of discrete concurrent systems can give insights into partly continuous systems, and that methods for the verification of finite-state systems can be used to analyze certain systems with uncountable state spaces}, author = {Henzinger, Thomas A}, booktitle = {Proceedings 11th Annual IEEE Symposium on Logic in Computer Science}, issn = {1043-6871}, location = {New Brunswick, NJ, United States of America}, pages = {278 -- 292}, publisher = {IEEE}, title = {{The theory of hybrid automata}}, doi = {10.1109/LICS.1996.561342 }, year = {1996}, } @inbook{2465, abstract = {Auxins play a crucial role in the regulation of spatial and temporal aspects of plant growth and development1. As well as being required for the division, enlargement and differentiation of individual plant cells, auxins also function as signals between cells, tissues and organs. In this way they contribute to the coordination and integration of growth and development in the whole plant and to physiological responses of plants to environmental cues (63). At the individual cell level, fast changes or pulses in hormone concentration may function to initiate or to terminate a developmental process. In contrast, the maintenance of a stable concentration of the hormone (homeostasis) may be necessary to maintain the progress of a developmental event that has already been initiated.}, author = {Morris, David and Friml, Jirí and Zažímalová, Eva}, booktitle = {Plant Hormones: Biosynthesis, Signal Transduction, Action!}, editor = {Davies, Peter}, isbn = {978-1-4020-2684-3}, 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 Shigemoto, Ryuichi and Nakanishi, Shigetada and Mizuno, Noboru}, issn = {0021-9967}, 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{2556, abstract = {By using substance P receptor (SPR) immunofluorescence histochemistry combined with fluorescent retrograde labeling, SPR-like immunoreactive (SPR-LI) neurons sending their axons to the lateral parabrachial region were observed in the lumbar spinal cord of the rat. After injection of Fluoro-Gold into the lateral parabrachial region, retrogradely labeled neurons with SPR-LI were seen frequently in lamina I and the lateral spinal nucleus, and occasionally in laminae IV and V, with a predominantly contralateral distribution. Some of these neurons, especially those in lamina I, may convey nociceptive information to the lateral parabrachial region.}, author = {Ding, Yu and Takada, Masahiko and Shigemoto, Ryuichi and Mizuno, Noboru}, issn = {0006-8993}, journal = {Brain Research}, number = {2}, pages = {336 -- 340}, publisher = {Elsevier}, title = {{Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity in the lumbar spinal cord of the rat}}, doi = {10.1016/0006-8993(95)00022-I}, volume = {674}, year = {1995}, } @article{2558, abstract = {Brain areas involved in the genesis and control of daily rhythms receive a prominent neural input that contains the neurotransmitter substance P (SP), a peptide putatively involved in the synchronization of circadian rhythms by environmental light. We investigated the localization of receptors to SP in the suprachiasmatic nucleus of the hypothalamus (SCN) and in the intergeniculate leaflet of the thalamus (IGL) of the rat and hamster using in situ hybridization histochemistry and immunohistochemistry. Consistently with that previously described in the rat, a neuronal population distributed along the lateral margin and at the dorso-latero-caudal aspect of the hamster SCN expresses moderately the mRNA encoding the SP receptor. In both rat and hamster, immunohistochemical data confirm the previous finding and reveal an almost complete absence of SP receptors in the ventral part of the SCN, which receives a direct projection from the retina. In the IGL of both species, numerous neurons prominently express the mRNA encoding the SP receptor. The immunostaining shows a high density of SP receptors on perikarya and dendrites throughout the nucleus. A dense staining is also observed on individual cells and processes bordering the lumen of blood vessels in the SCN and IGL.}, author = {Mick, Gérard and Shigemoto, Ryuichi and Kitahama, Kunio}, issn = {0764-4469}, journal = {Comptes Rendus de l'Academie des Sciences - Series III}, number = {2}, pages = {209 -- 217}, publisher = {Gauthier Villars Editeur}, title = {{Localization of substance P receptors in central neural structures controlling daily rhythms in nocturnal rodents}}, volume = {318}, 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 Shigemoto, Ryuichi and Takada, Masahiko and Nakamura, Kenji and Nakao, Kazuki and Katsuki, Motoya and Nakanishi, Shigetada}, issn = {0092-8674}, 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{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 and Xu, Tian and Qin, Bing and Li, Ji and Ding, Yu and Shigemoto, Ryuichi and Mizuno, Noboru}, issn = {0304-3940}, 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{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 and Shigemoto, Ryuichi and Wada, Eiki and Kinoshita, Ayae and Li, Jin and Neki, Akio and Nakanishi, Shigetada and Mizuno, Noboru}, issn = {0304-3940}, 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}, } @article{2563, abstract = {By means of substance P receptor (SPR) immunofluorescence histochemistry combined with Fluoro-Gold fluorescent retrograde labeling, SPR-like immunoreactive neurons in the caudal subnucleus of the spinal trigeminal nucleus of the rat were observed to send their axons to the nucleus of Kolliker-Fuse and ventrolateral part of the lateral parabrachial nucleus bilaterally with a clear ipsilateral dominance. These neurons were distributed mainly in lamina I, and additionally in lamina III.}, author = {Ding, Yu and Takada, Masahiko and Shigemoto, Ryuichi and Mizuno, Noboru}, issn = {0168-0102}, journal = {Neuroscience Research}, number = {4}, pages = {415 -- 418}, publisher = {Elsevier}, title = {{Trigeminoparabrachial projection neurons showing substance P receptor-like immunoreactivity in the rat}}, doi = {10.1016/0168-0102(95)00961-R}, volume = {23}, 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 = {Erdös, László}, location = {Holzhau, Germany}, 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}, } @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 = {Erdös, László}, issn = {0010-3616}, 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}, } @article{11677, abstract = {We present an algorithm for maintaining the biconnected components of a graph during a sequence of edge insertions and deletions. It requires linear storage and preprocessing time. The amortized running time for insertions and for deletions isO(m 2/3 ), wherem is the number of edges in the graph. Any query of the form ‘Are the verticesu andv biconnected?’ can be answered in timeO(1). This is the first sublinear algorithm for this problem. We can also output all articulation points separating any two vertices efficiently. If the input is a plane graph, the amortized running time for insertions and deletions drops toO(√n logn) and the query time isO(log2 n), wheren is the number of vertices in the graph. The best previously known solution takes timeO(n 2/3 ) per update or query.}, author = {Henzinger, Monika H}, issn = {1432-0541}, journal = {Algorithmica}, number = {6}, pages = {503--538}, publisher = {Springer Nature}, title = {{Fully dynamic biconnectivity in graphs}}, doi = {10.1007/bf01189067}, volume = {13}, year = {1995}, } @inproceedings{11684, abstract = {This paper presents an algorithm for the fully dynamic biconnectivity problem whose running time is exponentially faster than all previously known solutions. It is the first dynamic algorithm that answers biconnectivity queries in time O(log/sup 2/n) in a n-node graph and can be updated after an edge insertion or deletion in polylogarithmic time. Our algorithm is a Las-Vegas style randomized algorithm with the update time amortized update time O(log/sup 4/n). Only recently the best deterministic result for this problem was improved to O(/spl radic/nlog/sup 2/n). We also give the first fully dynamic and a novel deletions-only transitive closure (i.e. directed connectivity) algorithms. These are randomized Monte Carlo algorithms. Let n be the number of nodes in the graph and let m/spl circ/ be the average number of edges in the graph during the whole update sequence: The fully dynamic algorithms achieve (1) query time O(n/logn) and update time O(m/spl circ//spl radic/nlog/sup 2/n+n); or (2) query time O(n/logn) and update time O(nm/spl circ//sup /spl mu/-1/)log/sup 2/n=O(nm/spl circ//sup 0.58/log/sup 2/n), where /spl mu/ is the exponent for boolean matrix multiplication (currently /spl mu/=2.38). The deletions-only algorithm answers queries in time O(n/logn). Its amortized update time is O(nlog/sup 2/n).}, author = {Henzinger, Monika H and King, V.}, booktitle = {Proceedings of IEEE 36th Annual Foundations of Computer Science}, isbn = {0-8186-7183-1}, issn = {0272-5428}, location = {Milwaukee, WI, United States}, pages = {664--672}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Fully dynamic biconnectivity and transitive closure}}, doi = {10.1109/SFCS.1995.492668}, 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 = {Sazanov, Leonid A and Jackson, Baz}, issn = {0005-2728}, 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}, } @inproceedings{4587, abstract = {We argue that the standard constraints on liveness conditions in nonblocking trace models—machine closure for closed systems, and receptiveness for open systems—are unnecessarily weak and complex, and that liveness should, instead, be specified by augmenting transition systems with acceptance conditions that satisfy a locality constraint. First, locality implies machine closure and receptiveness, and thus permits the composition and modular verification of live transition systems. Second, while machine closure and receptiveness are based on infinite games, locality is based on repeated finite games, and thus easier to check. Third, no expressive power is lost by the restriction to local liveness conditions. We illustrate the appeal of local liveness using the model of Fair Reactive Systems, a nonblocking trace model of communicating processes.}, author = {Alur, Rajeev and Henzinger, Thomas A}, booktitle = {7th International Conference on Computer Aided Verification}, isbn = {978-3-540-60045-9}, location = {Liege, Belgium}, pages = {166 -- 179}, publisher = {Springer}, title = {{Local liveness for compositional modeling of fair reactive systems}}, doi = {10.1007/3-540-60045-0_49}, volume = {939}, year = {1995}, } @article{4613, abstract = {We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.}, author = {Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, Pei and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio}, issn = {0304-3975}, journal = {Theoretical Computer Science}, number = {1}, pages = {3 -- 34}, publisher = {Elsevier}, title = {{The algorithmic analysis of hybrid systems}}, doi = {10.1016/0304-3975(94)00202-T}, volume = {138}, year = {1995}, }