@inbook{2545,
  abstract     = {Glutamate receptors play an important role in many integrative brain functions and in neuronal development. We report the molecular diversity of NMDA receptors and metabotropic glutamate receptors on the basis of our studies of molecular cloning and characterization of the diverse members of these receptors. The NMDA receptors consist of two distinct types of subunits. NMDAR1 possesses all properties characteristic of the NMDA receptor-channel complex, whereas the four NMDAR2 subunits, termed NMDAR2A-2D, show no channel activity but potentiate the NMDAR1 activity and confer functional variability by different heteromeric formations. The NMDA receptor subunits are considerably divergent from the other ligand-gated ion channels, and the structural architecture of these subunits remains elusive. The mGluRs form a family of at least seven different subtypes termed mGluR1-mGluR7. These receptor subtypes have, seven transmembrane segments and possess a large extracellular domain at their N-terminal regions. The seven mGluR subtypes are classified into three subgroups according to their sequence similarities, signal transduction mechanisms and agonist selectivities: mGluR1/mGluR5, mGluR2/mGluR3 and mGluR4/mGluR6/mGluR7. On the basis of our knowledge of the molecular diversity of the NMDA receptors and mGluRs, we have studied the physiological roles of individual receptor subunits or subtypes. We have shown that K(+)-induced depolarization or NMDA treatment in primary cultures of neonatal cerebellar granule cells induces the functional NMDA receptor and specifically up-regulates NMDAR2A mRNA among the multiple NMDA receptor subunits through the increase in resting intracellular Ca2+ concentrations. Our study demonstrates that the regulation of the specific NMDA receptor subunit mRNA governs the NMDA receptor induction that is thought to play an important role in granule cell survival and death. Analysis of an agonist selectivity and an expression pattern of mGluR6 has indicated that mGluR6 is responsible for synaptic neurotransmission from photoreceptor cells to ON-bipolar cells in the visual system. We have also investigated the function of mGluR2 in granule cells of the accessory olfactory bulb by combining immunoelectron-microscopic analysis with slice-patch recordings on the basis of the identification of a new agonist selective for this receptor subtype. Our results demonstrate that mGluR2 is present at the presynaptic site of granule cells and modulates inhibitory GABA transmission from granule cells to mitral cells. This finding indicates that the mGluR2 activation relieves excited mitral cells from GABA inhibition but maintains the lateral inhibition of unexcited mitral cells, thus resulting in enhancement of the signal-to-noise ratio between the excited mitral cells and their neighboring unexcited mitral cells.},
  author       = {Nakanishi, Shigetada and Masu, Masayuki and Bessho, Yasumasa and Nakajima, Yoshiaki and Hayashi, Yasunori and Shigemoto, Ryuichi},
  booktitle    = {Experientia Supplementum},
  isbn         = {9783034873321},
  pages        = {71 -- 80},
  publisher    = {Birkhäuser},
  title        = {{Molecular diversity of glutamate receptors and their physiological functions}},
  doi          = {10.1007/978-3-0348-7330-7_8},
  volume       = {71},
  year         = {1994},
}

@inproceedings{2548,
  abstract     = {The induction mechanism of cerebellar long term depression (LTD) has been analysed in a cerebellar culture. Using nitr-5, a photolabile Ca chelator, we demonstrated that an increase in postsynaptic Ca together with glutamate application is sufficient to induce the LTD of glutamate responsiveness in Purkinje cells. It has also been shown that one subtype of genetically defined metabotropic glutamate receptor, mGluR1, is involved in the LTD induction. We raised antibodies which specifically recognized mGluR1 and inactivated its function. The antibodies suppressed the LTD induction in the cultured Purkinje cells.},
  author       = {Hirano, Tomoo and Kasono, Keizo and Ryuichi Shigemoto and Nakanishi, Shigetada},
  number       = {SUPPL. 1},
  pages        = {79 -- 81},
  publisher    = {Biomedical Research Foundation},
  title        = {{Induction mechanism of long term depression in cultured Purkinje neurons}},
  volume       = {15},
  year         = {1994},
}

@article{2549,
  abstract     = {In an attempt to reveal the function sites of substance P (SP) in the central nervous system (CNS), the distribution of SP receptor (SPR) was immunocytochemically investigated in adult rat and compared with that of SP- positive fibers. SPR-like immunoreactivity (LI) was mostly localized to neuronal cell bodies and dendrites. Neurons with intense SPR-LI were distributed densely in the cortical amygdaloid nucleus, hilus of the dentate gyrus, locus ceruleus, rostral half of the ambiguus nucleus, and intermediolateral nucleus of the thoracic cord; moderately in the caudatoputamen, nucleus accumbens, olfactory tubercle, median, pontine, and magnus raphe nuclei, laminae I and III of the caudal subnucleus of the spinal trigeminal nucleus, and lamina I of the spinal cord; and sparsely in the cerebral cortex, basal nucleus of Meynert, claustrum, gigantocellular reticular nucleus, and lobules IX and X of the cerebellar vermis. Neurons with weak to moderate SPR-LI were distributed more widely throughout the CNS. The regional patterns of distribution of SPR-LI were not necessarily the same as those of SP-positive fibers. The entopeduncular nucleus, substantia nigra, and lateral part of the interpeduncular nucleus showed intense SP-LI but displayed almost no SPR-LI. Conversely, the hilus of the dentate gyrus, anterodorsal thalamic nucleus, central nucleus of the inferior colliculus, and dorsal tegmental nucleus showed intense to moderate SPR-LI but contained few axons with SP-LI. These findings confirmed the presence of the 'mismatch' problem between SP and SPR localizations. However, the distribution of SPR- LI was quite consistent with that of the SP-binding activity, which has been studied via autoradiography. This indicates that the sites of SPR-LI revealed in the present study represent most, if not all, sites of SP-binding activity.},
  author       = {Nakaya, Yoshifumi and Kaneko, Takeshi and Shigemoto, Ryuichi and Nakanishi, Shigetada and Mizuno, Noboru},
  issn         = {0021-9967},
  journal      = {Journal of Comparative Neurology},
  number       = {2},
  pages        = {249 -- 274},
  publisher    = {Wiley-Blackwell},
  title        = {{Immunohistochemical localization of substance P receptor in the central nervous system of the adult rat}},
  doi          = {10.1002/cne.903470208},
  volume       = {347},
  year         = {1994},
}

@article{2550,
  abstract     = {A cDNA clone for a new rat metabotropic glutamate receptor termed mGluR7 was isolated through polymerase chain reaction-mediated DNA amplification by using primer sequences conserved among the metabotropic receptor (mGluR) family and by the subsequent screening of a rat forebrain cDNA library. The cloned mGluR7 subtype consists of 915 amino acid residues and exhibits a structural architecture common to the mGluR family with a large extracellular domain preceding the seven putative membrane-spanning domains. mGluR7 shows the highest sequence similarity to mGluR4 and mGluR6 among the members of the mGluR family. Similar to mGluR4 and mGluR6, mGluR7 inhibits forskolin- stimulated cyclic AMP accumulation in response to agonist interaction and potently reacts with L-2-amino-4-phosphonobutyrate and L-serine-O-phosphate in Chinese hamster ovary cells transfected with the cloned cDNA. RNA blot and in situ hybridization analyses of mGluR7 mRNA indicated that it is widely expressed in many neuronal cells of the central nervous system and is thus different from the more limitedly expressed mGluR4 or mGluR6 mRNA. mGluR7 together with mGluR4 thus corresponds to the putative L-2-amino-4- phosphonobutyrate receptor which plays an important role in modulation of glutamate transmission in the central nervous system.},
  author       = {Okamoto, Naoyuki and Hori, Seiji and Akazawa, Chihiro and Hayashi, Yasunori and Shigemoto, Ryuichi and Mizuno, Noboru and Nakanishi, Shigetada},
  journal      = {Journal of Biological Chemistry},
  number       = {2},
  pages        = {1231 -- 1236},
  publisher    = {American Society for Biochemistry and Molecular Biology},
  title        = {{Molecular characterization of a new metabotropic glutamate receptor mGluR7 coupled to inhibitory cyclic AMP signal transduction}},
  doi          = {10.1016/S0021-9258(17)42247-2},
  volume       = {269},
  year         = {1994},
}

@article{2551,
  abstract     = {Expression patterns of mRNAs of l-AP4-sensitive metabotropic glutamate receptors (mGluR4, mGluR6, mGluR7) in the rat retina were examined by northern blot analysis and in situ hybridization histochemistry. Expression patterns of mGluR4 and mGluR7 mRNAs were quite different from that of mGluR6 mRNA which was expressed at the outer part of the inner nuclear layer. The mGluR4 mRNA was expressed on the cell bodies of the ganglion cells, but not in the inner or outer nuclear layer. The expression of mGluR7 mRNA was observed throughout the entire region of the inner nuclear layer and on the cell bodies of the ganglion cells.},
  author       = {Akazawa, Chihiro and Ohishi, Hitoshi and Nakajima, Yoshiaki and Okamoto, Naoyuki and Shigemoto, Ryuichi and Nakanishi, Shigetada and Mizuno, Noboru},
  issn         = {0304-3940},
  journal      = {Neuroscience Letters},
  number       = {1-2},
  pages        = {52 -- 54},
  publisher    = {Elsevier},
  title        = {{Expression of mRNAs of l-AP4-sensitive metabotropic glutamate receptors (mGluR4, mGluR6, mGluR7) in the rat retina}},
  doi          = {10.1016/0304-3940(94)90602-5},
  volume       = {171},
  year         = {1994},
}

@article{2552,
  abstract     = {The superficial layers of the superior colliculus (SC) have been known to contain many axons showing substance P-like immunoreactivity (SP-LI). We, therefore, immunohistochemically examined the distribution of SP receptor (SPR) in the superficial layers of the SC in the rat by using a specific antibody against SPR. The majority of SC neurons with SPR-LI were distributed in the zonal and the superficial gray layers, the rest of them were in the optic layer. Electron microscopy revealed that SPR-immunoreaction products in SC neurons were distributed not only in postsynaptic sites, but also in non-synaptic regions of perikaryal and dendritic profiles.},
  author       = {Ogawa Meguro, Reiko and Shigemoto, Ryuichi and Itoh, Kazuo and Konishi, Akira and Mizuno, Noboru},
  issn         = {0304-3940},
  journal      = {Neuroscience Letters},
  number       = {2},
  pages        = {135 -- 138},
  publisher    = {Elsevier},
  title        = {{Immunohistochemical localization of substance P receptor in the superior colliculus. A light and electron microscope study in the rat}},
  doi          = {10.1016/0304-3940(94)90469-3},
  volume       = {166},
  year         = {1994},
}

@article{2553,
  abstract     = {Distribution of the mRNAs for three subtypes of prostaglandin E (PGE) receptors in the mouse kidney was investigated by in situ hybridization. The mRNA for EP1 subtype, which is coupled to Ca2+ mobilization, was specifically localized to the collecting ducts from the cortex to the papilla. The mRNA for EP2 subtype, which is linked to stimulation of adenylate cyclase, was localized to the glomeruli. The mRNA for EP3 subtype, which is coupled to inhibition of adenylate cyclase, was located densely in the tubules in the outer medulla and in the distal tubules in the cortex. These results exhibit distinct cellular localization of three subtypes of PGE receptor in the kidney and suggest that PGE2 exerts multiple functions via these subtypes expressed in different segments of the nephron.},
  author       = {Sugimoto, Yukihiko and Namba, Tsunehisa and Shigemoto, Ryuichi and Negishi, Manabu and Ichikawa, Atsushi and Narumiya, Shuh},
  issn         = {0363-6127},
  journal      = {American Journal of Physiology},
  number       = {5},
  pages        = {F823 -- F828},
  publisher    = {American Physiological Society},
  title        = {{Distinct cellular localization of mRNAs for three subtypes of prostaglandin E receptor in kidney}},
  doi          = {10.1152/ajprenal.1994.266.5.F823},
  volume       = {266},
  year         = {1994},
}

@article{2554,
  abstract     = {The retinal bipolar cell receiving glutamate transmission from photoreceptors mediates a key process in segregating visual signals into ON center and OFF center pathways. This transmission involves a G protein- coupled metabotropic glutamate receptor (mGluR). Immunocytochemical and immunoelectron microscopic studies indicate the restricted localization of a specific mGluR subtype, mGluR6, at the postsynaptic site of the rat rod bipolar cell. This specialization is developmentally regulated: mGluR6 is initially distributed in both the soma and dendrites and is finally concentrated on the postsynaptic site. The mGluR6 localization is reversed when photoreceptors degenerate in the mutant rat with retinal dystrophy. Evidence is thus presented indicating specialized, developmentally regulated receptor distribution in the central nervous system and the crucial role of mGluR6 in photoreceptor-bipolar cell synaptic transmission.},
  author       = {Nomura, Akinori and Shigemoto, Ryuichi and Nakamura, Yasuhisa and Okamoto, Naoyuki and Mizuno, Noboru and Nakanishi, Shigetada},
  issn         = {0092-8674},
  journal      = {Cell},
  number       = {3},
  pages        = {361 -- 369},
  publisher    = {Cell Press},
  title        = {{Developmentally regulated postsynaptic localization of a metabotropic glutamate receptor in rat rod bipolar cells}},
  doi          = {10.1016/0092-8674(94)90151-1},
  volume       = {77},
  year         = {1994},
}

@article{2555,
  abstract     = {Antibodies were raised against two distinct extracellular sequences of the rat mGluR1 metabotropic glutamate receptor expressed as bacterial fusion proteins. Both antibodies specifically reacted with mGluR1 in the rat cerebellum and inhibited the mGluR1 activity as assessed by the analysis of glutamate-stimulated inositol phosphate formation in CHO cells expressing mGluR1. Using these antibodies, we examined the role of mGluR1 in the induction of long-term depression in cultured Purkinje cells. In voltage- clamped Purkinje cells, current induced by iontophoretically applied glutamate was persistently depressed by depolarization of the Purkinje cells in conjunction with the glutamate application. The mGluR1 antibodies completely blocked the depression of glutamate-induced current. The results indicate that activation of mGluR1 is necessary for the induction of cerebellar long-term depression and that these mGluR1 antibodies can be used as selective antagonists.},
  author       = {Shigemoto, Ryuichi and Abe, Takaaki and Nomura, Sakashi and Nakanishi, Shigetada and Hirano, Tomoo},
  issn         = {0896-6273},
  journal      = {Neuron},
  number       = {6},
  pages        = {1245 -- 1255},
  publisher    = {Elsevier},
  title        = {{Antibodies inactivating mGluR1 metabotropic glutamate receptor block long-term depression in cultured Purkinje cells}},
  doi          = {10.1016/0896-6273(94)90441-3},
  volume       = {12},
  year         = {1994},
}

@article{2557,
  abstract     = {The distribution of the metabotropic glutamate receptors mGluR2 and mGluR3 was immunohistochemically examined in the rat cerebellar cortex at both light and electron microscope levels. An antibody was raised against a fusion protein containing a C-terminal portion of mGluR2. On immunoblot, the antibody reacted with both mGluR2 and mGluR3 in rat brain. mGluR2/3 immunoreactivity was expressed in cell bodies, dendrites, and axon terminals of Golgi cells, as well as in presumed glial processes. Golgi axon terminals with mGluR2/3 immunoreactivity were often encountered in the vicinity of glutamatergic mossy fiber terminals. The results suggest that transmitter glutamate may exert control influences upon Golgi cells not only through dendritic mGluR2/3, but also through axonal mGluR2/3.},
  author       = {Ohishi, Hitoshi and Ogawa Meguro, Reiko and Shigemoto, Ryuichi and Kaneko, Takeshi and Nakanishi, Shigetada and Mizuno, Noboru},
  issn         = {0896-6273},
  journal      = {Neuron},
  number       = {1},
  pages        = {55 -- 66},
  publisher    = {Elsevier},
  title        = {{Immunohistochemical localization of metabotropic glutamate receptors, mGluR2 and mGluR3, in rat cerebellar cortex}},
  doi          = {10.1016/0896-6273(94)90459-6},
  volume       = {13},
  year         = {1994},
}

@article{2713,
  author       = {Erdös, László},
  issn         = {0012-7094},
  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       = {Sazanov, Leonid A and Jackson, Julie},
  issn         = {0014-5793},
  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 &lt; 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 and Koshkin, Aleksei and Sazanov, Leonid A and Borodulina, O I and Varfolomeev, Sergei and Zaǐtsev, Sergei},
  issn         = {0014-5793},
  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},
}

@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 Henzinger, Thomas A},
  booktitle    = {Proceedings 9th Annual IEEE Symposium on Logic in Computer Science},
  issn         = {0018-9162},
  location     = {Paris, France},
  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 &quot;freeze&quot; 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 Henzinger, Thomas A},
  booktitle    = {Theories and Experiences for Real-Time System Development},
  editor       = {Rus, Teodor and Rattray, Charles},
  isbn         = { 9789810219239},
  keywords     = {real-time systems, clock variables},
  pages        = {1 -- 29},
  publisher    = {World Scientific Publishing},
  title        = {{Real-time system = discrete system + clock variables}},
  doi          = {10.1142/9789812831583_0001},
  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 Henzinger, Thomas A},
  issn         = {0004-5411},
  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 Henzinger, Thomas A},
  booktitle    = {5th International Conference on Concurrency Theory},
  isbn         = {3540583297},
  location     = {Uppsala, Sweden},
  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 Henzinger, Thomas A},
  booktitle    = {International Conference on Computer Aided Verification},
  isbn         = {9783540484691},
  location     = {Stanford, CA, United States of America},
  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,
  abstract     = {We extend the timed-automaton model for real-time systems [AD90] to a formal model for hybrid systems: while the continuous variables of a timed automaton are clocks that measure time, the continuous variables of a hybrid system are governed by arbitrary differential equations. We then adopt the verification methodology for timed automata [ACD90, ACD+92, HNSY92] to analyze hybrid systems: while the verification problem is decidable for timed automata, we obtain semidecision procedures for the class of hybrid systems whose continuous variables change in a piecewise linear fashion. },
  author       = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A and Ho, Pei and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio},
  booktitle    = {11th International Conference on Analysis and Optimization of Systems Discrete Event Systems},
  isbn         = {978-3-540-19896-3},
  location     = {Sophia-Antipolis, France},
  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},
}

