[{"month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"Proceedings of the 10th International Conference on Computer Aided Verification","publisher":"Springer","doi":"10.1007/BFb0028745","date_updated":"2022-08-24T09:19:53Z","oa_version":"None","volume":1427,"type":"conference","date_published":"1998-01-01T00:00:00Z","year":"1998","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:07Z","publication_status":"published","publist_id":"240","day":"01","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"}],"alternative_title":["LNCS"],"page":"195 - 206","conference":{"location":"Vancouver, Canada","end_date":"1998-07-02","start_date":"1998-06-28","name":"CAV: Computer Aided Verification"},"acknowledgement":"This work is supported in part by ONR YIP award N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","abstract":[{"lang":"eng","text":"Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating with expressions that represent state sets. Traditionally, symbolic model-checking tools arc based on backward state traversal; their basic operation is the function pre, which given a set of states, returns the set of all predecessor states. This is because specifiers usally employ formalisms with future-time modalities. which are naturally evaluated by iterating applications of pre. It has been recently shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only those parts of the state space are explored which are reachable from an initial state and relevant for satisfaction or violation of the specification; that is, errors can be detected as soon as possible.\r\nIn this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation; the post- calculus, on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4489","title":"From pre-historic to post-modern symbolic model checking","citation":{"ieee":"T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern symbolic model checking,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 195–206.","short":"T.A. Henzinger, O. Kupferman, S. Qadeer, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 195–206.","ista":"Henzinger TA, Kupferman O, Qadeer S. 1998. From pre-historic to post-modern symbolic model checking. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 195–206.","apa":"Henzinger, T. A., Kupferman, O., &#38; Qadeer, S. (1998). From pre-historic to post-modern symbolic model checking. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 195–206). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028745\">https://doi.org/10.1007/BFb0028745</a>","chicago":"Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic to Post-Modern Symbolic Model Checking.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:195–206. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028745\">https://doi.org/10.1007/BFb0028745</a>.","ama":"Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic model checking. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:195-206. doi:<a href=\"https://doi.org/10.1007/BFb0028745\">10.1007/BFb0028745</a>","mla":"Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model Checking.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 195–206, doi:<a href=\"https://doi.org/10.1007/BFb0028745\">10.1007/BFb0028745</a>."},"intvolume":"      1427","status":"public","scopus_import":"1","publication_identifier":{"isbn":["9783540646082"]}},{"acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, the NSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the ARO MURI grant DAAH-04-96-1-0341, the SRC contract 97-DC-324.041, the Belgian National Fund for Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks, the Portuguese FCT, and by Belgacom.","abstract":[{"lang":"eng","text":"A specification formalism for reactive systems defines a class of Ω-languages. We call a specification formalism fully decidable if it is constructively closed under boolean operations and has a decidable satisfiability (nonemptiness) problem. There are two important, robust classes of Ω-languages that are definable by fully decidable formalisms. The Ω -reqular languages are definable by finite automata, or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages are definable by temporal logic, or equivalcntly, by the first-order fragment of the Sequential Calculus. The gap between both classes can be closed by finite counting (using automata connectives), or equivalently, by projection (existential second-order quantification over letters).\r\nA specification formalism for real-time systems defines a class of timed Ω-langnages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed Ω-languages are robust, and we explain their relationship.\r\nFirst, we show that temporal logic with event clocks defines the same class of timed Ω-languages as temporal logic with nonsingular time bounds, and we identify a first-order monadic theory that also defines this class. Second, we show that if the ability of finite counting is added to these formalisms, we obtain the class of timed Ω-languages that are definable by finite automata with event clocks, or equivalently, by a restricted second-order extension of the monadic theory. Third, we show that if projection is added, we obtain the class of timed Ω-languages that are definable by timed automata, or equivalently, by a richer second-order extension of the monadic theory. These results identify three robust classes of timed Ω-languages, of which the third, while popular, is not definable by a, fully decidable formalism. By contrast, the first two classes are definable by fully decidable formalisms from temporal logic, from automata theory, and from monadic logic. Since the gap between these two classes can be closed by finite counting, we dub them the timed Ω-regular languages and the timed counter-free Ω-rcgular languages, respectively."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4490","title":"The regular real-time languages","intvolume":"      1443","citation":{"apa":"Henzinger, T. A., Raskin, J., &#38; Schobbens, P. (1998). The regular real-time languages. In <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i> (Vol. 1443, pp. 580–591). Aalborg, Denmark: Springer. <a href=\"https://doi.org/10.1007/BFb0055086\">https://doi.org/10.1007/BFb0055086</a>","ista":"Henzinger TA, Raskin J, Schobbens P. 1998. The regular real-time languages. Proceedings of the 25th International Colloqium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 1443, 580–591.","ieee":"T. A. Henzinger, J. Raskin, and P. Schobbens, “The regular real-time languages,” in <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, Aalborg, Denmark, 1998, vol. 1443, pp. 580–591.","short":"T.A. Henzinger, J. Raskin, P. Schobbens, in:, Proceedings of the 25th International Colloqium on Automata, Languages and Programming, Springer, 1998, pp. 580–591.","mla":"Henzinger, Thomas A., et al. “The Regular Real-Time Languages.” <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, vol. 1443, Springer, 1998, pp. 580–91, doi:<a href=\"https://doi.org/10.1007/BFb0055086\">10.1007/BFb0055086</a>.","ama":"Henzinger TA, Raskin J, Schobbens P. The regular real-time languages. In: <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>. Vol 1443. Springer; 1998:580-591. doi:<a href=\"https://doi.org/10.1007/BFb0055086\">10.1007/BFb0055086</a>","chicago":"Henzinger, Thomas A, Jean Raskin, and Pierre Schobbens. “The Regular Real-Time Languages.” In <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, 1443:580–91. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0055086\">https://doi.org/10.1007/BFb0055086</a>."},"status":"public","scopus_import":"1","publication_identifier":{"isbn":["9783540647812"]},"month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"Proceedings of the 25th International Colloqium on Automata, Languages and Programming","publisher":"Springer","date_updated":"2022-08-24T09:30:11Z","doi":"10.1007/BFb0055086","oa_version":"None","volume":1443,"type":"conference","date_published":"1998-01-01T00:00:00Z","language":[{"iso":"eng"}],"year":"1998","date_created":"2018-12-11T12:09:07Z","publication_status":"published","publist_id":"241","day":"01","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"},{"last_name":"Schobbens","first_name":"Pierre","full_name":"Schobbens, Pierre"}],"page":"580 - 591","alternative_title":["LNCS"],"conference":{"end_date":"1998-07-17","location":"Aalborg, Denmark","name":"ICALP: Automata, Languages and Programming","start_date":"1998-07-13"}},{"volume":43,"type":"journal_article","date_published":"1998-01-01T00:00:00Z","status":"public","article_type":"original","oa_version":"None","intvolume":"        43","citation":{"ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “Algorithmic analysis of nonlinear hybrid systems,” <i>IEEE Transactions on Automatic Control</i>, vol. 43, no. 4. IEEE, pp. 540–554, 1998.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, IEEE Transactions on Automatic Control 43 (1998) 540–554.","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1998). Algorithmic analysis of nonlinear hybrid systems. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/9.664156 \">https://doi.org/10.1109/9.664156 </a>","ista":"Henzinger TA, Ho P, Wong Toi H. 1998. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control. 43(4), 540–554.","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 1998. <a href=\"https://doi.org/10.1109/9.664156 \">https://doi.org/10.1109/9.664156 </a>.","mla":"Henzinger, Thomas A., et al. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>IEEE Transactions on Automatic Control</i>, vol. 43, no. 4, IEEE, 1998, pp. 540–54, doi:<a href=\"https://doi.org/10.1109/9.664156 \">10.1109/9.664156 </a>.","ama":"Henzinger TA, Ho P, Wong Toi H. Algorithmic analysis of nonlinear hybrid systems. <i>IEEE Transactions on Automatic Control</i>. 1998;43(4):540-554. doi:<a href=\"https://doi.org/10.1109/9.664156 \">10.1109/9.664156 </a>"},"abstract":[{"text":"We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","_id":"4491","publication":"IEEE Transactions on Automatic Control","date_updated":"2022-08-23T14:34:35Z","title":"Algorithmic analysis of nonlinear hybrid systems","publisher":"IEEE","doi":"10.1109/9.664156 ","month":"01","extern":"1","quality_controlled":"1","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"},{"last_name":"Wong Toi","full_name":"Wong Toi, Howard","first_name":"Howard"}],"issue":"4","page":"540 - 554","publication_identifier":{"issn":["0018-9162"]},"date_created":"2018-12-11T12:09:07Z","publist_id":"238","publication_status":"published","day":"01","language":[{"iso":"eng"}],"year":"1998"},{"year":"1998","language":[{"iso":"eng"}],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"first_name":"Peter","full_name":"Kopke, Peter","last_name":"Kopke"},{"full_name":"Puri, Anuj","first_name":"Anuj","last_name":"Puri"},{"first_name":"P.","full_name":"Varaiya, P.","last_name":"Varaiya"}],"page":"94 - 124","date_created":"2018-12-11T12:09:08Z","publication_status":"published","publist_id":"237","day":"01","article_processing_charge":"No","publication":"Journal of Computer and System Sciences","date_updated":"2022-08-23T14:29:15Z","doi":"10.1006/jcss.1998.1581","publisher":"Elsevier","month":"01","extern":"1","oa":1,"quality_controlled":"1","volume":57,"date_published":"1998-01-01T00:00:00Z","type":"journal_article","oa_version":"Published Version","article_type":"original","issue":"1","publication_identifier":{"isbn":["0022-0000"]},"abstract":[{"text":"Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves theω-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4492","title":"What's decidable about hybrid automata?","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator Award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation Grant CCR-9504469, by the Air Force Office of Scientific Research Contract F49620-93-1-0056, by the Army Research Office MURI Grant DAAH-04-96-1-0341, by the Army Research Office Contract DAAH-04-94-G-0026, by the Defense Advanced Research Projects Agency Grant NAG2-892, and by the California PATH program.","status":"public","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0022000098915811","open_access":"1"}],"citation":{"apa":"Henzinger, T. A., Kopke, P., Puri, A., &#38; Varaiya, P. (1998). What’s decidable about hybrid automata? <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1006/jcss.1998.1581\">https://doi.org/10.1006/jcss.1998.1581</a>","ista":"Henzinger TA, Kopke P, Puri A, Varaiya P. 1998. What’s decidable about hybrid automata? Journal of Computer and System Sciences. 57(1), 94–124.","short":"T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, Journal of Computer and System Sciences 57 (1998) 94–124.","ieee":"T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” <i>Journal of Computer and System Sciences</i>, vol. 57, no. 1. Elsevier, pp. 94–124, 1998.","mla":"Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>, vol. 57, no. 1, Elsevier, 1998, pp. 94–124, doi:<a href=\"https://doi.org/10.1006/jcss.1998.1581\">10.1006/jcss.1998.1581</a>.","ama":"Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? <i>Journal of Computer and System Sciences</i>. 1998;57(1):94-124. doi:<a href=\"https://doi.org/10.1006/jcss.1998.1581\">10.1006/jcss.1998.1581</a>","chicago":"Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>. Elsevier, 1998. <a href=\"https://doi.org/10.1006/jcss.1998.1581\">https://doi.org/10.1006/jcss.1998.1581</a>."},"intvolume":"        57"},{"month":"01","quality_controlled":"1","extern":"1","article_processing_charge":"No","doi":"10.1007/BFb0055640","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2022-08-23T14:24:08Z","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","oa_version":"None","type":"conference","date_published":"1998-01-01T00:00:00Z","volume":1466,"language":[{"iso":"eng"}],"year":"1998","date_created":"2018-12-11T12:09:15Z","day":"01","publist_id":"214","publication_status":"published","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"conference":{"name":"CONCUR: Concurrency Theory","start_date":"1998-09-08","end_date":"1998-09-11","location":"Nice, France"},"alternative_title":["LNCS"],"page":"439 - 454","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.","lang":"eng"}],"title":"It's about time: Real-time logics reviewed","_id":"4515","citation":{"ama":"Henzinger TA. It’s about time: Real-time logics reviewed. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:439-454. doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>","mla":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–54, doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>.","chicago":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:439–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>.","ista":"Henzinger TA. 1998. It’s about time: Real-time logics reviewed. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 439–454.","apa":"Henzinger, T. A. (1998). It’s about time: Real-time logics reviewed. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 439–454). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>","short":"T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–454.","ieee":"T. A. Henzinger, “It’s about time: Real-time logics reviewed,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 439–454."},"intvolume":"      1466","status":"public","scopus_import":"1","publication_identifier":{"isbn":["978-3-540-64896-3"]}},{"page":"163 - 178","alternative_title":["LNCS"],"conference":{"end_date":"1998-09-11","location":"Nice, France","name":"CONCUR: Concurrency Theory","start_date":"1998-09-08"},"author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"},{"first_name":"Moshe","full_name":"Vardi, Moshe","last_name":"Vardi"}],"publist_id":"104","publication_status":"published","day":"01","date_created":"2018-12-11T12:09:42Z","language":[{"iso":"eng"}],"year":"1998","volume":1466,"date_published":"1998-01-01T00:00:00Z","type":"conference","oa_version":"None","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","doi":"10.1007/BFb0055622","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2022-08-23T09:50:34Z","article_processing_charge":"No","extern":"1","quality_controlled":"1","month":"01","publication_identifier":{"isbn":["978-3-540-64896-3"]},"scopus_import":"1","status":"public","intvolume":"      1466","citation":{"ieee":"R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi, “Alternating refinement relations,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 163–178.","short":"R. Alur, T.A. Henzinger, O. Kupferman, M. Vardi, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–178.","ista":"Alur R, Henzinger TA, Kupferman O, Vardi M. 1998. Alternating refinement relations. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 163–178.","apa":"Alur, R., Henzinger, T. A., Kupferman, O., &#38; Vardi, M. (1998). Alternating refinement relations. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 163–178). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055622\">https://doi.org/10.1007/BFb0055622</a>","chicago":"Alur, Rajeev, Thomas A Henzinger, Orna Kupferman, and Moshe Vardi. “Alternating Refinement Relations.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:163–78. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055622\">https://doi.org/10.1007/BFb0055622</a>.","ama":"Alur R, Henzinger TA, Kupferman O, Vardi M. Alternating refinement relations. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:163-178. doi:<a href=\"https://doi.org/10.1007/BFb0055622\">10.1007/BFb0055622</a>","mla":"Alur, Rajeev, et al. “Alternating Refinement Relations.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–78, doi:<a href=\"https://doi.org/10.1007/BFb0055622\">10.1007/BFb0055622</a>."},"_id":"4603","title":"Alternating refinement relations","abstract":[{"lang":"eng","text":"Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as “Does the implementation refine the set A of specification components without constraining the components not in A?” In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9504469, CCR-9628400, and CCR-9700061, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, by the SRC contract 97-DC-324.041, and by a grant from the Intel Corporation."},{"year":"1998","language":[{"iso":"eng"}],"day":"01","publist_id":"103","publication_status":"published","date_created":"2018-12-11T12:09:42Z","conference":{"name":"CAV: Computer Aided Verification","start_date":"1998-06-28","end_date":"1998-07-02","location":"Vancouver, Canada"},"alternative_title":["LNCS"],"page":"521 - 525","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"},{"last_name":"Rajamani","first_name":"Sriram","full_name":"Rajamani, Sriram"},{"last_name":"Tasiran","full_name":"Tasiran, Serdar","first_name":"Serdar"}],"quality_controlled":"1","extern":"1","month":"01","publisher":"Springer","date_updated":"2022-08-23T09:06:21Z","doi":"10.1007/BFb0028774","publication":"Proceedings of the 10th International Conference on Computer Aided Verification","article_processing_charge":"No","oa_version":"None","date_published":"1998-01-01T00:00:00Z","type":"conference","volume":1427,"scopus_import":"1","publication_identifier":{"isbn":["9783540646082"]},"acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","title":"Mocha: Modularity in model checking","_id":"4604","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"apa":"Alur, R., Henzinger, T. A., Mang, F., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (1998). Mocha: Modularity in model checking. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 521–525). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028774\">https://doi.org/10.1007/BFb0028774</a>","ista":"Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. 1998. Mocha: Modularity in model checking. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 521–525.","short":"R. Alur, T.A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, S. Tasiran, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 521–525.","ieee":"R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran, “Mocha: Modularity in model checking,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 521–525.","mla":"Alur, Rajeev, et al. “Mocha: Modularity in Model Checking.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 521–25, doi:<a href=\"https://doi.org/10.1007/BFb0028774\">10.1007/BFb0028774</a>.","ama":"Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. Mocha: Modularity in model checking. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:521-525. doi:<a href=\"https://doi.org/10.1007/BFb0028774\">10.1007/BFb0028774</a>","chicago":"Alur, Rajeev, Thomas A Henzinger, Freddy Mang, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “Mocha: Modularity in Model Checking.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:521–25. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028774\">https://doi.org/10.1007/BFb0028774</a>."},"intvolume":"      1427","status":"public"},{"year":"1998","language":[{"iso":"eng"}],"day":"01","publication_status":"published","publist_id":"102","date_created":"2018-12-11T12:09:43Z","conference":{"location":"Lisbon, Portugal","end_date":"1998-04-04","start_date":"1998-03-28","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"page":"330 - 344","alternative_title":["LNCS"],"author":[{"last_name":"Alur","full_name":"Alur, Rajeev","first_name":"Rajeev"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Rajamani","full_name":"Rajamani, Sriram","first_name":"Sriram"}],"quality_controlled":"1","extern":"1","month":"01","doi":"10.1007/BFb0054181","date_updated":"2022-08-23T08:44:36Z","publisher":"Springer","publication":"Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","article_processing_charge":"No","oa_version":"None","type":"conference","date_published":"1998-01-01T00:00:00Z","volume":1384,"scopus_import":"1","publication_identifier":{"isbn":["9783540643562"]},"acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Air Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant NAG2-892, and by the Semiconductor Research Corporation contract 95-DC-324.036.\r\n","title":"Symbolic exploration of transition hierarchies","_id":"4606","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"In formal design verification, successful model checking is typically preceded by a laborious manual process of constructing design abstractions. We present a methodology for partially—and in some cases, fully—bypassing the abstraction process. For this purpose, we provide to the designer abstraction operators which, if used judiciously in the description of a design, structure the corresponding state space hierarchically. This structure can then be exploited by verification tools, and makes possible the automatic and exhaustive exploration of state spaces that would otherwise be out of scope for existing model checkers.\r\nSpecifically, we present the following contributions:\r\n- \t A temporal abstraction operator that aggregates transitions and hides intermediate steps. Mathematically, our abstraction operator is a function that maps a flat transition system into a two-level hierarchy where each atomic upper-level transition expands into an entire lower-level transition system. For example, an arithmetic operation may expand into a sequence of bit operations.\r\n- \t A BDD-based algorithm for the symbolic exploration of multi-level hierarchies of transition systems. The algorithm traverses a level-n transition by expanding the corresponding level-(n − 1) transition system on-the-fly. The level-n successors of a state are determined by computing a level-(n − 1) reach set, which is then immediately released from memory. In this fashion, we can exhaustively explore hierarchically structured state spaces whose flat counterparts cause memory overflows.\r\n- \t We experimentally demonstrate the efficiency of our method with three examples—a multiplier, a cache coherence protocol, and a multiprocessor system. In the first two examples, we obtain significant improvements in run times and peak BDD sizes over traditional state-space search. The third example cannot be model checked at all using conventional methods (without manual abstractions), but can be analyzed fully automatically using transition hierarchies.","lang":"eng"}],"intvolume":"      1384","citation":{"short":"R. Alur, T.A. Henzinger, S. Rajamani, in:, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1998, pp. 330–344.","ieee":"R. Alur, T. A. Henzinger, and S. Rajamani, “Symbolic exploration of transition hierarchies,” in <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Lisbon, Portugal, 1998, vol. 1384, pp. 330–344.","ista":"Alur R, Henzinger TA, Rajamani S. 1998. Symbolic exploration of transition hierarchies. Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1384, 330–344.","apa":"Alur, R., Henzinger, T. A., &#38; Rajamani, S. (1998). Symbolic exploration of transition hierarchies. In <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 1384, pp. 330–344). Lisbon, Portugal: Springer. <a href=\"https://doi.org/10.1007/BFb0054181\">https://doi.org/10.1007/BFb0054181</a>","chicago":"Alur, Rajeev, Thomas A Henzinger, and Sriram Rajamani. “Symbolic Exploration of Transition Hierarchies.” In <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 1384:330–44. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0054181\">https://doi.org/10.1007/BFb0054181</a>.","ama":"Alur R, Henzinger TA, Rajamani S. Symbolic exploration of transition hierarchies. In: <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 1384. Springer; 1998:330-344. doi:<a href=\"https://doi.org/10.1007/BFb0054181\">10.1007/BFb0054181</a>","mla":"Alur, Rajeev, et al. “Symbolic Exploration of Transition Hierarchies.” <i>Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 1384, Springer, 1998, pp. 330–44, doi:<a href=\"https://doi.org/10.1007/BFb0054181\">10.1007/BFb0054181</a>."},"status":"public"},{"abstract":[{"lang":"eng","text":"An open system can be modeled as a two-player game between the system and its environment. At each round of the game, player 1 (the system) and player 2 (the environment) independently and simultaneously choose moves, and the two choices determine the next state of the game. Properties of open systems can be modeled as objectives of these two-player games. For the basic objective of reachability-can player 1 force the game to a given set of target states?-there are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε&gt;0 a randomized strategy to reach the target with probability greater than 1-ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies. Finally, we apply our results by introducing a temporal logic in which all three kinds of winning conditions can be specified, and which can be model checked in polynomial time. This logic, called Randomized ATL, is suitable for reasoning about randomized behavior in open (two-agent) as well as multi-agent systems"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","publication":" Proceedings 39th Annual Symposium on Foundations of Computer Science","_id":"4639","date_updated":"2022-08-22T14:09:02Z","title":"Concurrent reachability games","publisher":"IEEE","doi":"10.1109/SFCS.1998.743507  ","month":"01","extern":"1","quality_controlled":"1","date_published":"1998-01-01T00:00:00Z","type":"conference","status":"public","oa_version":"None","citation":{"ama":"De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. In: <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>. IEEE; 1998:564-575. doi:<a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">10.1109/SFCS.1998.743507  </a>","mla":"De Alfaro, Luca, et al. “Concurrent Reachability Games.” <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, IEEE, 1998, pp. 564–75, doi:<a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">10.1109/SFCS.1998.743507  </a>.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability Games.” In <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, 564–75. IEEE, 1998. <a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">https://doi.org/10.1109/SFCS.1998.743507  </a>.","ista":"De Alfaro L, Henzinger TA, Kupferman O. 1998. Concurrent reachability games.  Proceedings 39th Annual Symposium on Foundations of Computer Science. FOCS: Foundations of Computer Science, 564–575.","apa":"De Alfaro, L., Henzinger, T. A., &#38; Kupferman, O. (1998). Concurrent reachability games. In <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i> (pp. 564–575). Palo Alto, CA, United States of America: IEEE. <a href=\"https://doi.org/10.1109/SFCS.1998.743507  \">https://doi.org/10.1109/SFCS.1998.743507  </a>","short":"L. De Alfaro, T.A. Henzinger, O. Kupferman, in:,  Proceedings 39th Annual Symposium on Foundations of Computer Science, IEEE, 1998, pp. 564–575.","ieee":"L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability games,” in <i> Proceedings 39th Annual Symposium on Foundations of Computer Science</i>, Palo Alto, CA, United States of America, 1998, pp. 564–575."},"language":[{"iso":"eng"}],"year":"1998","author":[{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Orna","full_name":"Kupferman, Orna","last_name":"Kupferman"}],"page":"564 - 575","conference":{"end_date":"1998-11-11","location":"Palo Alto, CA, United States of America","name":"FOCS: Foundations of Computer Science","start_date":"1998-11-08"},"date_created":"2018-12-11T12:09:53Z","publication_identifier":{"isbn":["0818691727"]},"publication_status":"published","publist_id":"68","day":"01"},{"status":"public","volume":10,"date_published":"1997-06-19T00:00:00Z","type":"journal_article","citation":{"apa":"Hunt, B. R., &#38; Kaloshin, V. (1997). How projections affect the dimension spectrum of fractal measures. <i>Nonlinearity</i>. IOP Publishing. <a href=\"https://doi.org/10.1088/0951-7715/10/5/002\">https://doi.org/10.1088/0951-7715/10/5/002</a>","ista":"Hunt BR, Kaloshin V. 1997. How projections affect the dimension spectrum of fractal measures. Nonlinearity. 10(5), 1031–1046.","ieee":"B. R. Hunt and V. Kaloshin, “How projections affect the dimension spectrum of fractal measures,” <i>Nonlinearity</i>, vol. 10, no. 5. IOP Publishing, pp. 1031–1046, 1997.","short":"B.R. Hunt, V. Kaloshin, Nonlinearity 10 (1997) 1031–1046.","mla":"Hunt, Brian R., and Vadim Kaloshin. “How Projections Affect the Dimension Spectrum of Fractal Measures.” <i>Nonlinearity</i>, vol. 10, no. 5, IOP Publishing, 1997, pp. 1031–46, doi:<a href=\"https://doi.org/10.1088/0951-7715/10/5/002\">10.1088/0951-7715/10/5/002</a>.","ama":"Hunt BR, Kaloshin V. How projections affect the dimension spectrum of fractal measures. <i>Nonlinearity</i>. 1997;10(5):1031-1046. doi:<a href=\"https://doi.org/10.1088/0951-7715/10/5/002\">10.1088/0951-7715/10/5/002</a>","chicago":"Hunt, Brian R, and Vadim Kaloshin. “How Projections Affect the Dimension Spectrum of Fractal Measures.” <i>Nonlinearity</i>. IOP Publishing, 1997. <a href=\"https://doi.org/10.1088/0951-7715/10/5/002\">https://doi.org/10.1088/0951-7715/10/5/002</a>."},"intvolume":"        10","oa_version":"None","article_type":"original","publication":"Nonlinearity","_id":"8527","doi":"10.1088/0951-7715/10/5/002","date_updated":"2021-01-12T08:19:53Z","publisher":"IOP Publishing","title":"How projections affect the dimension spectrum of fractal measures","abstract":[{"lang":"eng","text":"We introduce a new potential-theoretic definition of the dimension spectrum  of a probability measure for q > 1 and explain its relation to prior definitions. We apply this definition to prove that if  and  is a Borel probability measure with compact support in , then under almost every linear transformation from  to , the q-dimension of the image of  is ; in particular, the q-dimension of  is preserved provided . We also present results on the preservation of information dimension  and pointwise dimension. Finally, for  and q > 2 we give examples for which  is not preserved by any linear transformation into . All results for typical linear transformations are also proved for typical (in the sense of prevalence) continuously differentiable functions."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","extern":"1","quality_controlled":"1","month":"06","page":"1031-1046","issue":"5","author":[{"first_name":"Brian R","full_name":"Hunt, Brian R","last_name":"Hunt"},{"full_name":"Kaloshin, Vadim","first_name":"Vadim","id":"FE553552-CDE8-11E9-B324-C0EBE5697425","last_name":"Kaloshin","orcid":"0000-0002-6051-2628"}],"keyword":["Mathematical Physics","General Physics and Astronomy","Applied Mathematics","Statistical and Nonlinear Physics"],"publication_status":"published","day":"19","publication_identifier":{"issn":["0951-7715","1361-6544"]},"date_created":"2020-09-18T10:50:41Z","year":"1997","language":[{"iso":"eng"}]},{"year":"1997","language":[{"iso":"eng"}],"publication_status":"published","day":"30","date_created":"2020-09-18T10:50:54Z","publication_identifier":{"issn":["0016-2663","1573-8485"]},"page":"95-99","keyword":["Applied Mathematics","Analysis"],"author":[{"last_name":"Kaloshin","orcid":"0000-0002-6051-2628","id":"FE553552-CDE8-11E9-B324-C0EBE5697425","first_name":"Vadim","full_name":"Kaloshin, Vadim"}],"issue":"2","extern":"1","quality_controlled":"1","month":"03","_id":"8528","publication":"Functional Analysis and Its Applications","publisher":"Springer Nature","doi":"10.1007/bf02466014","title":"Prevalence in the space of finitely smooth maps","date_updated":"2021-01-12T08:19:54Z","abstract":[{"text":"In the present paper, we give a definition of prevalent (\"metrically prevalent\" ) sets in nonlinear function\r\nspaces. A subset of a Euclidean space is said to be metrically prevalent if its complement has measure zero.\r\nThere is no natural way to generalize the definition of a set of measure zero in a finite-dimensional space\r\nto the infinite-dimensional case [6]. Therefore, it is necessary to give a special definition of a metrically\r\nprevalent set (set of full measure) in an infinite-dimensional space. There are various ways to do so. We\r\nsuggest one of the possible ways to define the class of metrically prevalent sets in the space of smooth maps\r\nof one smooth manifold into another. It is shown in this paper that the class of metrically prevalent sets\r\nhas natural properties; in particular, the intersection of finitely many metrically prevalent sets is metrically\r\nprevalent. The main result of the paper is a prevalent version of Thorn's transversality theorem.\r\nIt is common practice in singularity theory and the theory of dynamical systems to say that a property\r\nholds for \"almost every\" map (or flow) if it holds for a residual set, i.e., a set that contains a countable\r\nintersection of open dense sets in the corresponding function space. However, even in finite-dimensional\r\nspaces such a set can have arbitrarily small (say, zero) Lebesgue measure. We prove that Thorn's transversality theorem holds for an essentially \"thicker\" set than a residual set. It seems reasonable to revise from\r\nthe prevalent point of view the classical results of singularity theory and theory of dynamical systems,\r\nincluding the multijet transversality theorem, Mather's stability theorem, Kupka-Smale's theorem for dynamical systems, etc. We shall do this elsewhere. The notion of prevalence in linear Banach spaces was\r\nintroduced and investigated in [8]. One of the possible ways to define a class of prevalent sets in the space\r\nof smooth maps of manifolds, which essentially differs from that presented in this paper, is given in [7].\r\nDefinitions of typicalness based on the Lebesgue measure in a finite-dimensional space were suggested\r\nby Kolmogorov [10] and Arnold [11]. These definitions were cited and discussed in [9]. Here we only point\r\nout that the finite-dimensional analog of Arnold's definition allows prevalent sets to have arbitrarily small\r\nmeasure, whereas the prevalent sets in the sense of the finite-dimensional analog of the definition given in\r\nthe present paper are necessarily of full measure. Our definition is a modification of that due to Arnold.\r\nI wish to thank Yu. S. Illyashenko for constant attention to this work and useful discussions and\r\nR. I. Bogdanov for help in the preparation of this paper. ","lang":"eng"}],"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Kaloshin, Vadim. “Prevalence in the Space of Finitely Smooth Maps.” <i>Functional Analysis and Its Applications</i>. Springer Nature, 1997. <a href=\"https://doi.org/10.1007/bf02466014\">https://doi.org/10.1007/bf02466014</a>.","mla":"Kaloshin, Vadim. “Prevalence in the Space of Finitely Smooth Maps.” <i>Functional Analysis and Its Applications</i>, vol. 31, no. 2, Springer Nature, 1997, pp. 95–99, doi:<a href=\"https://doi.org/10.1007/bf02466014\">10.1007/bf02466014</a>.","ama":"Kaloshin V. Prevalence in the space of finitely smooth maps. <i>Functional Analysis and Its Applications</i>. 1997;31(2):95-99. doi:<a href=\"https://doi.org/10.1007/bf02466014\">10.1007/bf02466014</a>","short":"V. Kaloshin, Functional Analysis and Its Applications 31 (1997) 95–99.","ieee":"V. Kaloshin, “Prevalence in the space of finitely smooth maps,” <i>Functional Analysis and Its Applications</i>, vol. 31, no. 2. Springer Nature, pp. 95–99, 1997.","apa":"Kaloshin, V. (1997). Prevalence in the space of finitely smooth maps. <i>Functional Analysis and Its Applications</i>. Springer Nature. <a href=\"https://doi.org/10.1007/bf02466014\">https://doi.org/10.1007/bf02466014</a>","ista":"Kaloshin V. 1997. Prevalence in the space of finitely smooth maps. Functional Analysis and Its Applications. 31(2), 95–99."},"intvolume":"        31","article_type":"original","oa_version":"None","status":"public","volume":31,"date_published":"1997-03-30T00:00:00Z","type":"journal_article"},{"title":"Continuous profiling: Where have all the cycles gone?","_id":"11666","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"This article describes the Digital Continuous Profiling Infrastructure, a sampling-based profiling system designed to run continuously on production systems. The system supports multiprocessors, works on unmodified executables, and collects profiles for entire systems, including user programs, shared libraries, and the operating system kernel. Samples are collected at a high rate (over 5200 samples/sec. per 333MHz processor), yet with low overhead (1–3% slowdown for most workloads). Analysis tools supplied with the profiling system use the sample data to produce a precise and accurate accounting, down to the level of pipeline stalls incurred by individual instructions, of where time is bring spent. When instructions incur stalls, the tools identify possible reasons, such as cache misses, branch mispredictions, and functional unit contention. The fine-grained instruction-level analysis guides users and automated optimizers to the causes of performance problems and provides important insights for fixing them.","lang":"eng"}],"acknowledgement":"We would like to thank Mike Burrows, Allan Heydon, Hal Murray, Sharon Perl, and Sharon Smith for helpful comments that greatly improved the content and presentation of this article; the anonymous referees for SOSP and TOCS also provided numerous helpful comments. We would also like to thank Dawson Engler for initially suggesting the use of interprocessor interrupts to avoid expensive synchronization operations in the interrupt handler, Mitch Lichtenberg for his work on the Alpha/NT version of our system and in general for his help and suggestions on the project, and the developers of iprobe for supplying us with source code that helped us get off the ground in building the early versions of our data collection system. Finally, we would like to thank Gary Carleton and Bob Davies of Intel for answering our questions about VTune and Marty Itzkowitz of SGI for answering our questions about SpeedShop.","status":"public","citation":{"ista":"Anderson JM, Berc LM, Dean J, Ghemawat S, Henzinger MH, Leung S-TA, Sites RL, Vandevoorde MT, Waldspurger CA, Weihl WE. 1997. Continuous profiling: Where have all the cycles gone? ACM Transactions on Computer Systems. 15(4), 357–390.","apa":"Anderson, J. M., Berc, L. M., Dean, J., Ghemawat, S., Henzinger, M. H., Leung, S.-T. A., … Weihl, W. E. (1997). Continuous profiling: Where have all the cycles gone? <i>ACM Transactions on Computer Systems</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/265924.265925\">https://doi.org/10.1145/265924.265925</a>","short":"J.M. Anderson, L.M. Berc, J. Dean, S. Ghemawat, M.H. Henzinger, S.-T.A. Leung, R.L. Sites, M.T. Vandevoorde, C.A. Waldspurger, W.E. Weihl, ACM Transactions on Computer Systems 15 (1997) 357–390.","ieee":"J. M. Anderson <i>et al.</i>, “Continuous profiling: Where have all the cycles gone?,” <i>ACM Transactions on Computer Systems</i>, vol. 15, no. 4. Association for Computing Machinery, pp. 357–390, 1997.","ama":"Anderson JM, Berc LM, Dean J, et al. Continuous profiling: Where have all the cycles gone? <i>ACM Transactions on Computer Systems</i>. 1997;15(4):357-390. doi:<a href=\"https://doi.org/10.1145/265924.265925\">10.1145/265924.265925</a>","mla":"Anderson, Jennifer M., et al. “Continuous Profiling: Where Have All the Cycles Gone?” <i>ACM Transactions on Computer Systems</i>, vol. 15, no. 4, Association for Computing Machinery, 1997, pp. 357–90, doi:<a href=\"https://doi.org/10.1145/265924.265925\">10.1145/265924.265925</a>.","chicago":"Anderson, Jennifer M., Lance M. Berc, Jeffrey Dean, Sanjay Ghemawat, Monika H Henzinger, Shun-Tak A. Leung, Richard L. Sites, Mark T. Vandevoorde, Carl A. Waldspurger, and William E. Weihl. “Continuous Profiling: Where Have All the Cycles Gone?” <i>ACM Transactions on Computer Systems</i>. Association for Computing Machinery, 1997. <a href=\"https://doi.org/10.1145/265924.265925\">https://doi.org/10.1145/265924.265925</a>."},"intvolume":"        15","scopus_import":"1","issue":"4","publication_identifier":{"issn":["0734-2071"],"eissn":["1557-7333"]},"date_updated":"2022-09-09T12:00:13Z","publisher":"Association for Computing Machinery","doi":"10.1145/265924.265925","publication":"ACM Transactions on Computer Systems","article_processing_charge":"No","quality_controlled":"1","extern":"1","month":"11","type":"journal_article","date_published":"1997-11-01T00:00:00Z","volume":15,"article_type":"original","oa_version":"None","year":"1997","language":[{"iso":"eng"}],"page":"357-390","author":[{"last_name":"Anderson","full_name":"Anderson, Jennifer M.","first_name":"Jennifer M."},{"last_name":"Berc","first_name":"Lance M.","full_name":"Berc, Lance M."},{"first_name":"Jeffrey","full_name":"Dean, Jeffrey","last_name":"Dean"},{"last_name":"Ghemawat","first_name":"Sanjay","full_name":"Ghemawat, Sanjay"},{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"},{"first_name":"Shun-Tak A.","full_name":"Leung, Shun-Tak A.","last_name":"Leung"},{"last_name":"Sites","first_name":"Richard L.","full_name":"Sites, Richard L."},{"last_name":"Vandevoorde","full_name":"Vandevoorde, Mark T.","first_name":"Mark T."},{"last_name":"Waldspurger","full_name":"Waldspurger, Carl A.","first_name":"Carl A."},{"full_name":"Weihl, William E.","first_name":"William E.","last_name":"Weihl"}],"day":"01","publication_status":"published","date_created":"2022-07-27T11:42:25Z"},{"abstract":[{"lang":"eng","text":"This paper presents insertions-only algorithms for maintaining the exact and/or approximate size of the minimum edge cut and the minimum vertex cut of a graph. The algorithms output the approximate or exact sizekin timeO(1) and a cut of sizekin time linear in its size. For the minimum edge cut problem and for any 0 < ε ≤ 1, the amortized time per insertion isO(1/ε2) for a (2 + ε)-approximation,O((log λ)((log n)/ε)2) for a (1 + ε)-approximation, andO(λ log n) for the exact size, wherenis the number of nodes in the graph and λ is the size of the minimum cut. The (2 + ε)-approximation algorithm and the exact algorithm are deterministic; the (1 + ε)-approximation algorithm is randomized. We also present a static 2-approximation algorithm for the size κ of the minimum vertex cut in a graph, which takes time. This is a factor of κ faster than the best algorithm for computing the exact size, which takes time. We give an insertions-only algorithm for maintaining a (2 + ε)-approximation of the minimum vertex cut with amortized insertion timeO(n/ε)."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","_id":"11765","publication":"Journal of Algorithms","title":"A static 2-approximation algorithm for vertex connectivity and incremental approximation algorithms for edge and vertex connectivity","date_updated":"2022-09-12T09:15:38Z","doi":"10.1006/jagm.1997.0855","publisher":"Elsevier","month":"07","extern":"1","quality_controlled":"1","volume":24,"type":"journal_article","date_published":"1997-07-01T00:00:00Z","status":"public","article_type":"original","oa_version":"None","citation":{"ama":"Henzinger MH. A static 2-approximation algorithm for vertex connectivity and incremental approximation algorithms for edge and vertex connectivity. <i>Journal of Algorithms</i>. 1997;24(1):194-220. doi:<a href=\"https://doi.org/10.1006/jagm.1997.0855\">10.1006/jagm.1997.0855</a>","mla":"Henzinger, Monika H. “A Static 2-Approximation Algorithm for Vertex Connectivity and Incremental Approximation Algorithms for Edge and Vertex Connectivity.” <i>Journal of Algorithms</i>, vol. 24, no. 1, Elsevier, 1997, pp. 194–220, doi:<a href=\"https://doi.org/10.1006/jagm.1997.0855\">10.1006/jagm.1997.0855</a>.","chicago":"Henzinger, Monika H. “A Static 2-Approximation Algorithm for Vertex Connectivity and Incremental Approximation Algorithms for Edge and Vertex Connectivity.” <i>Journal of Algorithms</i>. Elsevier, 1997. <a href=\"https://doi.org/10.1006/jagm.1997.0855\">https://doi.org/10.1006/jagm.1997.0855</a>.","ista":"Henzinger MH. 1997. A static 2-approximation algorithm for vertex connectivity and incremental approximation algorithms for edge and vertex connectivity. Journal of Algorithms. 24(1), 194–220.","apa":"Henzinger, M. H. (1997). A static 2-approximation algorithm for vertex connectivity and incremental approximation algorithms for edge and vertex connectivity. <i>Journal of Algorithms</i>. Elsevier. <a href=\"https://doi.org/10.1006/jagm.1997.0855\">https://doi.org/10.1006/jagm.1997.0855</a>","short":"M.H. Henzinger, Journal of Algorithms 24 (1997) 194–220.","ieee":"M. H. Henzinger, “A static 2-approximation algorithm for vertex connectivity and incremental approximation algorithms for edge and vertex connectivity,” <i>Journal of Algorithms</i>, vol. 24, no. 1. Elsevier, pp. 194–220, 1997."},"intvolume":"        24","scopus_import":"1","language":[{"iso":"eng"}],"year":"1997","author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger"}],"issue":"1","page":"194-220","date_created":"2022-08-08T12:18:38Z","publication_identifier":{"issn":["0196-6774"]},"publication_status":"published","day":"01"},{"oa_version":"Published Version","article_type":"original","type":"journal_article","date_published":"1997-08-01T00:00:00Z","volume":55,"month":"08","oa":1,"quality_controlled":"1","extern":"1","article_processing_charge":"No","publisher":"Elsevier","date_updated":"2022-09-12T10:46:21Z","doi":"10.1006/jcss.1997.1493","publication":"Journal of Computer and System Sciences","date_created":"2022-08-08T12:28:45Z","day":"01","publication_status":"published","author":[{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"},{"last_name":"Klein","full_name":"Klein, Philip","first_name":"Philip"},{"first_name":"Satish","full_name":"Rao, Satish","last_name":"Rao"},{"full_name":"Subramanian, Sairam","first_name":"Sairam","last_name":"Subramanian"}],"page":"3-23","year":"1997","language":[{"iso":"eng"}],"citation":{"ista":"Henzinger MH, Klein P, Rao S, Subramanian S. 1997. Faster shortest-path algorithms for planar graphs. Journal of Computer and System Sciences. 55(1), 3–23.","apa":"Henzinger, M. H., Klein, P., Rao, S., &#38; Subramanian, S. (1997). Faster shortest-path algorithms for planar graphs. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1006/jcss.1997.1493\">https://doi.org/10.1006/jcss.1997.1493</a>","ieee":"M. H. Henzinger, P. Klein, S. Rao, and S. Subramanian, “Faster shortest-path algorithms for planar graphs,” <i>Journal of Computer and System Sciences</i>, vol. 55, no. 1. Elsevier, pp. 3–23, 1997.","short":"M.H. Henzinger, P. Klein, S. Rao, S. Subramanian, Journal of Computer and System Sciences 55 (1997) 3–23.","ama":"Henzinger MH, Klein P, Rao S, Subramanian S. Faster shortest-path algorithms for planar graphs. <i>Journal of Computer and System Sciences</i>. 1997;55(1):3-23. doi:<a href=\"https://doi.org/10.1006/jcss.1997.1493\">10.1006/jcss.1997.1493</a>","mla":"Henzinger, Monika H., et al. “Faster Shortest-Path Algorithms for Planar Graphs.” <i>Journal of Computer and System Sciences</i>, vol. 55, no. 1, Elsevier, 1997, pp. 3–23, doi:<a href=\"https://doi.org/10.1006/jcss.1997.1493\">10.1006/jcss.1997.1493</a>.","chicago":"Henzinger, Monika H, Philip Klein, Satish Rao, and Sairam Subramanian. “Faster Shortest-Path Algorithms for Planar Graphs.” <i>Journal of Computer and System Sciences</i>. Elsevier, 1997. <a href=\"https://doi.org/10.1006/jcss.1997.1493\">https://doi.org/10.1006/jcss.1997.1493</a>."},"intvolume":"        55","main_file_link":[{"url":"https://doi.org/10.1006/jcss.1997.1493","open_access":"1"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"We give a linear-time algorithm for single-source shortest paths in planar graphs with nonnegative edge-lengths. Our algorithm also yields a linear-time algorithm for maximum flow in a planar graph with the source and sink on the same face. For the case where negative edge-lengths are allowed, we give an algorithm requiringO(n4/3 log(nL)) time, whereLis the absolute value of the most negative length. This algorithm can be used to obtain similar bounds for computing a feasible flow in a planar network, for finding a perfect matching in a planar bipartite graph, and for finding a maximum flow in a planar graph when the source and sink are not on the same face. We also give parallel and dynamic versions of these algorithms.","lang":"eng"}],"title":"Faster shortest-path algorithms for planar graphs","_id":"11767","publication_identifier":{"issn":["0022-0000"]},"issue":"1","scopus_import":"1"},{"language":[{"iso":"eng"}],"year":"1997","scopus_import":"1","conference":{"end_date":"1997-07-11","location":"Bologna, Italy","name":"ICALP: International Colloquium on Automata, Languages, and Programming","start_date":"1997-07-07"},"page":"594–604","alternative_title":["LNCS"],"author":[{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"King","first_name":"Valerie","full_name":"King, Valerie"}],"day":"01","publication_status":"published","date_created":"2022-08-11T13:35:06Z","publication_identifier":{"eisbn":["9783540691945"],"isbn":["9783540631651"],"issn":["0302-9743"],"eissn":["1611-3349"]},"title":"Maintaining minimum spanning trees in dynamic graphs","date_updated":"2023-02-14T07:49:03Z","doi":"10.1007/3-540-63165-8_214","publisher":"Springer Nature","_id":"11803","publication":"24th International Colloquium on Automata, Languages and Programming","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","abstract":[{"lang":"eng","text":"We present the first fully dynamic algorithm for maintaining a minimum spanning tree in time o(√n) per operation. To be precise, the algorithm uses O(n 1/3 log n) amortized time per update operation. The algorithm is fairly simple and deterministic. An immediate consequence is the first fully dynamic deterministic algorithm for maintaining connectivity and, bipartiteness in amortized time O(n 1/3 log n) per update, with O(1) worst case time per query."}],"quality_controlled":"1","extern":"1","month":"07","status":"public","type":"conference","date_published":"1997-07-01T00:00:00Z","volume":1256,"citation":{"apa":"Henzinger, M. H., &#38; King, V. (1997). Maintaining minimum spanning trees in dynamic graphs. In <i>24th International Colloquium on Automata, Languages and Programming</i> (Vol. 1256, pp. 594–604). Bologna, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-63165-8_214\">https://doi.org/10.1007/3-540-63165-8_214</a>","ista":"Henzinger MH, King V. 1997. Maintaining minimum spanning trees in dynamic graphs. 24th International Colloquium on Automata, Languages and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 1256, 594–604.","short":"M.H. Henzinger, V. King, in:, 24th International Colloquium on Automata, Languages and Programming, Springer Nature, 1997, pp. 594–604.","ieee":"M. H. Henzinger and V. King, “Maintaining minimum spanning trees in dynamic graphs,” in <i>24th International Colloquium on Automata, Languages and Programming</i>, Bologna, Italy, 1997, vol. 1256, pp. 594–604.","mla":"Henzinger, Monika H., and Valerie King. “Maintaining Minimum Spanning Trees in Dynamic Graphs.” <i>24th International Colloquium on Automata, Languages and Programming</i>, vol. 1256, Springer Nature, 1997, pp. 594–604, doi:<a href=\"https://doi.org/10.1007/3-540-63165-8_214\">10.1007/3-540-63165-8_214</a>.","ama":"Henzinger MH, King V. Maintaining minimum spanning trees in dynamic graphs. In: <i>24th International Colloquium on Automata, Languages and Programming</i>. Vol 1256. Springer Nature; 1997:594–604. doi:<a href=\"https://doi.org/10.1007/3-540-63165-8_214\">10.1007/3-540-63165-8_214</a>","chicago":"Henzinger, Monika H, and Valerie King. “Maintaining Minimum Spanning Trees in Dynamic Graphs.” In <i>24th International Colloquium on Automata, Languages and Programming</i>, 1256:594–604. Springer Nature, 1997. <a href=\"https://doi.org/10.1007/3-540-63165-8_214\">https://doi.org/10.1007/3-540-63165-8_214</a>."},"intvolume":"      1256","oa_version":"None"},{"publication":"ACM SIGOPS Operating Systems Review","doi":"10.1145/269005.266637","publisher":"Association for Computing Machinery","date_updated":"2023-02-21T16:30:27Z","article_processing_charge":"No","extern":"1","quality_controlled":"1","oa":1,"month":"12","volume":31,"type":"journal_article","date_published":"1997-12-01T00:00:00Z","article_type":"original","oa_version":"Published Version","year":"1997","language":[{"iso":"eng"}],"related_material":{"record":[{"id":"11849","relation":"earlier_version","status":"public"}]},"page":"1-14","author":[{"full_name":"Anderson, Jennifer M.","first_name":"Jennifer M.","last_name":"Anderson"},{"first_name":"Lance M.","full_name":"Berc, Lance M.","last_name":"Berc"},{"last_name":"Dean","first_name":"Jeffrey","full_name":"Dean, Jeffrey"},{"last_name":"Ghemawat","full_name":"Ghemawat, Sanjay","first_name":"Sanjay"},{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"},{"last_name":"Leung","first_name":"Shun-Tak A.","full_name":"Leung, Shun-Tak A."},{"last_name":"Sites","full_name":"Sites, Richard L.","first_name":"Richard L."},{"first_name":"Mark T.","full_name":"Vandevoorde, Mark T.","last_name":"Vandevoorde"},{"last_name":"Waldspurger","first_name":"Carl A.","full_name":"Waldspurger, Carl A."},{"last_name":"Weihl","first_name":"William E.","full_name":"Weihl, William E."}],"publication_status":"published","day":"01","date_created":"2022-08-16T07:07:03Z","_id":"11849","title":"Continuous profiling: Where have all the cycles gone?","abstract":[{"text":"This paper describes the DIGlTAL Continuous Profiling Infrastmcture, a sampling-based profiling system designed to run continuously on production systems. The system supports multiprocessors, works on unmodified executable& and collects profiles for entire systems, including user programs, shared libraries, and the operating system kernel. Samples are collected at a high rate (over 5200 samples/secper333-MHz processor), yet with low overhead (l-3% slowdown for most workloads). Analysis tools supplied with the profiling system use the sample data to produce an accurate accounting, down to the level of pipeline stalls incurred by individual instructions, of where time is being spent. When instructions incur stalls, the tools identify possible reasons, such as cache misses, branch mispredictions, and functional unit contention. The fine-grained instruction-level analysis guides users and automated optimizers to the causes of performance\r\nproblems and provides important insights for fixing them. ","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/269005.266637"}],"citation":{"short":"J.M. Anderson, L.M. Berc, J. Dean, S. Ghemawat, M.H. Henzinger, S.-T.A. Leung, R.L. Sites, M.T. Vandevoorde, C.A. Waldspurger, W.E. Weihl, ACM SIGOPS Operating Systems Review 31 (1997) 1–14.","ieee":"J. M. Anderson <i>et al.</i>, “Continuous profiling: Where have all the cycles gone?,” <i>ACM SIGOPS Operating Systems Review</i>, vol. 31, no. 5. Association for Computing Machinery, pp. 1–14, 1997.","ista":"Anderson JM, Berc LM, Dean J, Ghemawat S, Henzinger MH, Leung S-TA, Sites RL, Vandevoorde MT, Waldspurger CA, Weihl WE. 1997. Continuous profiling: Where have all the cycles gone? ACM SIGOPS Operating Systems Review. 31(5), 1–14.","apa":"Anderson, J. M., Berc, L. M., Dean, J., Ghemawat, S., Henzinger, M. H., Leung, S.-T. A., … Weihl, W. E. (1997). Continuous profiling: Where have all the cycles gone? <i>ACM SIGOPS Operating Systems Review</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/269005.266637\">https://doi.org/10.1145/269005.266637</a>","chicago":"Anderson, Jennifer M., Lance M. Berc, Jeffrey Dean, Sanjay Ghemawat, Monika H Henzinger, Shun-Tak A. Leung, Richard L. Sites, Mark T. Vandevoorde, Carl A. Waldspurger, and William E. Weihl. “Continuous Profiling: Where Have All the Cycles Gone?” <i>ACM SIGOPS Operating Systems Review</i>. Association for Computing Machinery, 1997. <a href=\"https://doi.org/10.1145/269005.266637\">https://doi.org/10.1145/269005.266637</a>.","ama":"Anderson JM, Berc LM, Dean J, et al. Continuous profiling: Where have all the cycles gone? <i>ACM SIGOPS Operating Systems Review</i>. 1997;31(5):1-14. doi:<a href=\"https://doi.org/10.1145/269005.266637\">10.1145/269005.266637</a>","mla":"Anderson, Jennifer M., et al. “Continuous Profiling: Where Have All the Cycles Gone?” <i>ACM SIGOPS Operating Systems Review</i>, vol. 31, no. 5, Association for Computing Machinery, 1997, pp. 1–14, doi:<a href=\"https://doi.org/10.1145/269005.266637\">10.1145/269005.266637</a>."},"intvolume":"        31","scopus_import":"1","issue":"5","publication_identifier":{"issn":["0163-5980"]}},{"extern":"1","quality_controlled":"1","month":"12","_id":"11883","publication":"Random Structures and Algorithms","doi":"10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x","date_updated":"2023-02-17T14:05:02Z","title":"Sampling to provide or to bound: With applications to fully dynamic graph algorithms","publisher":"Wiley","abstract":[{"text":"In dynamic graph algorithms the following provide-or-bound problem has to be solved quickly: Given a set S containing a subset R and a way of generating random elements from S testing for membership in R, either (i) provide an element of R, or (ii) give a (small) upper bound on the size of R that holds with high probability. We give an optimal algorithm for this problem. This algorithm improves the time per operation for various dynamic graph algorithms by a factor of O(log n). For example, it improves the time per update for fully dynamic connectivity from O(log3n) to O(log2n).","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","citation":{"short":"M.H. Henzinger, M. Thorup, Random Structures and Algorithms 11 (1997) 369–379.","ieee":"M. H. Henzinger and M. Thorup, “Sampling to provide or to bound: With applications to fully dynamic graph algorithms,” <i>Random Structures and Algorithms</i>, vol. 11, no. 4. Wiley, pp. 369–379, 1997.","ista":"Henzinger MH, Thorup M. 1997. Sampling to provide or to bound: With applications to fully dynamic graph algorithms. Random Structures and Algorithms. 11(4), 369–379.","apa":"Henzinger, M. H., &#38; Thorup, M. (1997). Sampling to provide or to bound: With applications to fully dynamic graph algorithms. <i>Random Structures and Algorithms</i>. Wiley. <a href=\"https://doi.org/10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x\">https://doi.org/10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x</a>","chicago":"Henzinger, Monika H, and Mikkel Thorup. “Sampling to Provide or to Bound: With Applications to Fully Dynamic Graph Algorithms.” <i>Random Structures and Algorithms</i>. Wiley, 1997. <a href=\"https://doi.org/10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x\">https://doi.org/10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x</a>.","ama":"Henzinger MH, Thorup M. Sampling to provide or to bound: With applications to fully dynamic graph algorithms. <i>Random Structures and Algorithms</i>. 1997;11(4):369-379. doi:<a href=\"https://doi.org/10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x\">10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x</a>","mla":"Henzinger, Monika H., and Mikkel Thorup. “Sampling to Provide or to Bound: With Applications to Fully Dynamic Graph Algorithms.” <i>Random Structures and Algorithms</i>, vol. 11, no. 4, Wiley, 1997, pp. 369–79, doi:<a href=\"https://doi.org/10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x\">10.1002/(sici)1098-2418(199712)11:4&#60;369::aid-rsa5&#62;3.0.co;2-x</a>."},"intvolume":"        11","oa_version":"None","article_type":"original","status":"public","volume":11,"type":"journal_article","date_published":"1997-12-07T00:00:00Z","language":[{"iso":"eng"}],"year":"1997","scopus_import":"1","publication_status":"published","day":"07","date_created":"2022-08-17T07:21:55Z","publication_identifier":{"issn":["1042-9832"],"eissn":["1098-2418"]},"page":"369-379","author":[{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Thorup","first_name":"Mikkel","full_name":"Thorup, Mikkel"}],"issue":"4"},{"issue":"3","publication_identifier":{"issn":["0021-9967"]},"scopus_import":"1","status":"public","intvolume":"       378","citation":{"chicago":"Acsády, László, István Katona, Attila Gulyás, Ryuichi Shigemoto, and Tamás Freund. “Immunostaining for Substance P Receptor Labels GABAergic Cells with Distinct Termination Patterns in the Hippocampus.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 1997. <a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>.","ama":"Acsády L, Katona I, Gulyás A, Shigemoto R, Freund T. Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus. <i>Journal of Comparative Neurology</i>. 1997;378(3):320-336. doi:<a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>","mla":"Acsády, László, et al. “Immunostaining for Substance P Receptor Labels GABAergic Cells with Distinct Termination Patterns in the Hippocampus.” <i>Journal of Comparative Neurology</i>, vol. 378, no. 3, Wiley-Blackwell, 1997, pp. 320–36, doi:<a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>.","short":"L. Acsády, I. Katona, A. Gulyás, R. Shigemoto, T. Freund, Journal of Comparative Neurology 378 (1997) 320–336.","ieee":"L. Acsády, I. Katona, A. Gulyás, R. Shigemoto, and T. Freund, “Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus,” <i>Journal of Comparative Neurology</i>, vol. 378, no. 3. Wiley-Blackwell, pp. 320–336, 1997.","ista":"Acsády L, Katona I, Gulyás A, Shigemoto R, Freund T. 1997. Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus. Journal of Comparative Neurology. 378(3), 320–336.","apa":"Acsády, L., Katona, I., Gulyás, A., Shigemoto, R., &#38; Freund, T. (1997). Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>"},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"A specific antiserum against substance P receptor (SPR) labels nonprincipal neurons in the cerebral cortex of the rat (T. Kaneko et al. [1994], Neuroscience 60:199-211; Y. Nakaya et al. [1994], J. Comp. Neurol. 347:249-274). In the present study, we aimed to identify the types of SPR- immunoreactive neurons in the hippocampus according to their content of neurochemical markers, which label interneuron populations with distinct termination patterns. Markers for perisomatic inhibitory cells, parvalbumin and cholecystokinin (CCK), colocalized with SPR in pyramidallike basket cells in the dentate gyrus and in large multipolar or bitufted cells within all hippocampal subfields respectively. A dense meshwork of SPR-immunoreactive spiny dendrites in the hilus and stratum lucidum of the CA3 region belonged largely to inhibitory cells terminating in the distal dendritic region of granule cells, as indicated by the somatostatin and neuropeptide Y (NPY) content. In addition, SPR and NPY were colocalized in numerous multipolar interneurons with dendrites branching close to the soma. Twenty-five percent of the SPR-immunoreactive cells overlapped with calretinin-positive neurons in all hippocampal subfields, showing that interneurons specialized to contact other gamma-aminobutyric acid-ergic cells may also contain SPR. On the basis of the known termination pattern of the colocalized markers, we conclude that SPR-positive interneurons are functionally heterogeneous and participate in different inhibitory processes: (1) perisomatic inhibition of principal cells (CCK-containing cells, and parvalbumin-positive cells in the dentate gyrus), (2) feedback dendritic inhibition in the entorhinal termination zone (somatostatin and NPY-containing cells), and (3) innervation of other interneurons (calretinin-containing cells).","lang":"eng"}],"title":"Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus","_id":"2493","pmid":1,"acknowledgement":"This sudy was supported by grants from the Human Frontier Science Program Organisation, the Howard Hughes Medical Institute, and OTKA (T 16942) Hungary.We are grateful to Dr. K.G. Baimbridge and to Dr. M.R.Celio (calbindin and parvalbumin), Dr. T. Go ̈rcs (CCK, VIP,NPY, and somatostatin), Dr. J.H. Rogers (calretinin), andDr. C.G. Beaulieau (GABA) for kind gifts of antisera. The excellent technical assistance of Mrs. E. Borok, Mrs. A.Z.Szabo, and Mr. G. Terstyanszky is also acknowledged","author":[{"last_name":"Acsády","first_name":"László","full_name":"Acsády, László"},{"first_name":"István","full_name":"Katona, István","last_name":"Katona"},{"last_name":"Gulyás","full_name":"Gulyás, Attila","first_name":"Attila"},{"orcid":"0000-0001-8761-9444","last_name":"Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi","full_name":"Shigemoto, Ryuichi"},{"first_name":"Tamás","full_name":"Freund, Tamás","last_name":"Freund"}],"page":"320 - 336","date_created":"2018-12-11T11:57:59Z","day":"17","publist_id":"4408","publication_status":"published","year":"1997","language":[{"iso":"eng"}],"type":"journal_article","date_published":"1997-02-17T00:00:00Z","volume":378,"oa_version":"None","external_id":{"pmid":["9034894"]},"article_type":"original","article_processing_charge":"No","date_updated":"2022-08-22T13:43:18Z","doi":"10.1002/(SICI)1096-9861(19970217)378:3&lt;320::AID-CNE2&gt;3.0.CO;2-5","publisher":"Wiley-Blackwell","publication":"Journal of Comparative Neurology","month":"02","quality_controlled":"1","extern":"1"},{"citation":{"ama":"Li H, Ohishi H, Kinoshita A, Shigemoto R, Nomura S, Mizuno N. Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat. <i>Neuroscience Letters</i>. 1997;223(3):153-156. doi:<a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">10.1016/S0304-3940(97)13429-2</a>","mla":"Li, He, et al. “Localization of a Metabotropic Glutamate Receptor, MGluR7, in Axon Terminals of Presumed Nociceptive, Primary Afferent Fibers in the Superficial Layers of the Spinal Dorsal Horn: An Electron Microscope Study in the Rat.” <i>Neuroscience Letters</i>, vol. 223, no. 3, Elsevier, 1997, pp. 153–56, doi:<a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">10.1016/S0304-3940(97)13429-2</a>.","chicago":"Li, He, Hitoshi Ohishi, Ayae Kinoshita, Ryuichi Shigemoto, Sakashi Nomura, and Noboru Mizuno. “Localization of a Metabotropic Glutamate Receptor, MGluR7, in Axon Terminals of Presumed Nociceptive, Primary Afferent Fibers in the Superficial Layers of the Spinal Dorsal Horn: An Electron Microscope Study in the Rat.” <i>Neuroscience Letters</i>. Elsevier, 1997. <a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">https://doi.org/10.1016/S0304-3940(97)13429-2</a>.","ista":"Li H, Ohishi H, Kinoshita A, Shigemoto R, Nomura S, Mizuno N. 1997. Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat. Neuroscience Letters. 223(3), 153–156.","apa":"Li, H., Ohishi, H., Kinoshita, A., Shigemoto, R., Nomura, S., &#38; Mizuno, N. (1997). Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat. <i>Neuroscience Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">https://doi.org/10.1016/S0304-3940(97)13429-2</a>","short":"H. Li, H. Ohishi, A. Kinoshita, R. Shigemoto, S. Nomura, N. Mizuno, Neuroscience Letters 223 (1997) 153–156.","ieee":"H. Li, H. Ohishi, A. Kinoshita, R. Shigemoto, S. Nomura, and N. Mizuno, “Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat,” <i>Neuroscience Letters</i>, vol. 223, no. 3. Elsevier, pp. 153–156, 1997."},"intvolume":"       223","status":"public","pmid":1,"acknowledgement":"We are grateful for photographic help of Mr. Akira Uesugi. We also express our gratitude for the support of Drs. Satoru Fukuchi, Ritsu Hayashi, Sohzaburo Hayashi, Mizuho Katsurada, Hitoshi Kawai, Yutaka Kitani, Toshihiko Kuroda, Keiko Kumagai, Hiroshi Matsubara, Hiroshi Matsushima, Chisato Minakuchi, Gonpei Niwa, Hajime Oda, Masahiko Ohbayashi, Sei-ichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki, Eizo Watanabe, Kazuo Yoshino, and Toshiaki Yoshino. This work was supported in part by Grant-in-Aid from Ministry of Education, Science, Culture and Sports of Japan.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"It was examined electron microscopically in the rat if a metabotropic glutamate receptor, mGluR7, might be localized in axon terminals of nociceptive, primary afferent fibers in laminae I and II of the spinal dorsal horn. Nociceptive nature of axon terminals showing mGluR7-like immunoreactivity (mGluR7-LI) was indicated by binding to the isolectin I-B4 from Griffonia simplicifolia (I-B4), or by substance P-like immunoreactivity (SP-LI). Axon terminals labeled with immunogold particles indicating mGluR7-LI were usually filled with round synaptic vesicles and were in asymmetric synaptic contact with dendritic or somatic profiles; occasionally they contained pleomorphic vesicles and were in symmetric synaptic contact with somatic profiles in lamina II. The double-labeling studies revealed that most of axon terminals with I-B4 labeling as well as a small population of axon terminals with SP-LI, showed mGluR7-LI. About one-third or much smaller population of axon terminals with mGluR7-LI in laminae I and II were labeled, respectively, with I-B4 or SP-LI; these were in asymmetric synaptic contact with dendritic profiles."}],"title":"Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat","_id":"2575","publication_identifier":{"issn":["0304-3940"]},"issue":"3","scopus_import":"1","article_type":"original","external_id":{"pmid":["9080455"]},"oa_version":"None","type":"journal_article","date_published":"1997-02-28T00:00:00Z","volume":223,"month":"02","quality_controlled":"1","extern":"1","article_processing_charge":"No","publisher":"Elsevier","date_updated":"2022-08-22T13:06:30Z","doi":"10.1016/S0304-3940(97)13429-2","publication":"Neuroscience Letters","date_created":"2018-12-11T11:58:28Z","day":"28","publication_status":"published","publist_id":"4322","author":[{"full_name":"Li, He","first_name":"He","last_name":"Li"},{"first_name":"Hitoshi","full_name":"Ohishi, Hitoshi","last_name":"Ohishi"},{"first_name":"Ayae","full_name":"Kinoshita, Ayae","last_name":"Kinoshita"},{"last_name":"Shigemoto","orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi"},{"first_name":"Sakashi","full_name":"Nomura, Sakashi","last_name":"Nomura"},{"first_name":"Noboru","full_name":"Mizuno, Noboru","last_name":"Mizuno"}],"page":"153 - 156","language":[{"iso":"eng"}],"year":"1997"},{"status":"public","intvolume":"       378","citation":{"apa":"Li, J., Kaneko, T., Shigemoto, R., &#38; Mizuno, N. (1997). Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6\">https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6</a>","ista":"Li J, Kaneko T, Shigemoto R, Mizuno N. 1997. Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat. Journal of Comparative Neurology. 378(4), 508–521.","short":"J. Li, T. Kaneko, R. Shigemoto, N. Mizuno, Journal of Comparative Neurology 378 (1997) 508–521.","ieee":"J. Li, T. Kaneko, R. Shigemoto, and N. Mizuno, “Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat,” <i>Journal of Comparative Neurology</i>, vol. 378, no. 4. Wiley-Blackwell, pp. 508–521, 1997.","mla":"Li, Jin, et al. “Distribution of Trigeminohypothalamic and Spinohypothalamic Tract Neurons Displaying Substance P Receptor-like Immunoreactivity in the Rat.” <i>Journal of Comparative Neurology</i>, vol. 378, no. 4, Wiley-Blackwell, 1997, pp. 508–21, doi:<a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6\">10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6</a>.","ama":"Li J, Kaneko T, Shigemoto R, Mizuno N. Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat. <i>Journal of Comparative Neurology</i>. 1997;378(4):508-521. doi:<a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6\">10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6</a>","chicago":"Li, Jin, Takeshi Kaneko, Ryuichi Shigemoto, and Noboru Mizuno. “Distribution of Trigeminohypothalamic and Spinohypothalamic Tract Neurons Displaying Substance P Receptor-like Immunoreactivity in the Rat.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 1997. <a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6\">https://doi.org/10.1002/(SICI)1096-9861(19970224)378:4&#38;lt;508::AID-CNE6&#38;gt;3.0.CO;2-6</a>."},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"Primary afferent neurons containing substance P (SP) are apparently implicated in the transmission of noxious information from the periphery to the central nervous system, and SP released from primary afferent neurons acts on second-order neurons with the SP receptor (SPR). In the rat, nociceptive information reached the hypothalamus not only through indirect pathways but also directly through trigeminohypothalamic and spinohypothalamic pathways. Thus, in the present study, the distribution pattern of trigeminohypothalamic and spinohypothalamic tract neurons showing SPR-like immunoreactivity (SPR-LI) was examined in the rat by a retrograde tract-tracing method combined with immunofluorescence histochemistry for SPR. A substantial number of trigeminal and spinal neurons with SPR-LI were retrogradely labeled with Fluore-Gold (FG) injected into the hypothalamic regions. These neurons were distributed mainly in lamina I of the medullary and spinal dorsal horns, lateral spinal nucleus, regions around the central canal of the spinal cord, and the lateral aspect of the deep part of the spinal dorsal horn. A number of SPR-LI neurons in the spinal parasympathetic nucleus were labeled with FG injected into the area around the paraventricular hypothalamic nucleus. Some SPR-LI neurons in the lateral spinal nucleus and the lateral aspect of the deep part of the spinal dorsal horn were also labeled with FG injected into the septal region. On the basis of the distribution areas of SPR-LI trigeminal and spinal neurons projecting to the hypothalamic and septal regions, it is likely that these neurons are involved in the transmission of somatic and/or visceral noxious information."}],"title":"Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat","_id":"2576","pmid":1,"acknowledgement":"This study was supported by grants 08279106 and 08458245 from the Ministry of Education, Science, Sportsand Culture of Japan. We are grateful for the photographic help of Mr. Akira Uesugi and the support of Dr. Kajitaro Morita in Morita Clinic of Internal Medicine and Pediatrics, Kadoma, Osaka, Japan. We also express our gratitude for the support of Drs. Satoru Fukuchi, Ritsu Hayashi,Sohzaburo Hayashi, Mizuho Katsurada, Hitoski Kawai,Yutaka Kitani, Toshihiko Kuroda, Keiko Kumagai, Hiroshi Matsubara, Hiroshi Matsushima, Chisato Minakuchi,Gonpei Niwa, Hajime Oda, Mashiko Ohbayashi, Seiichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki, EizoWatanabe, Kazuo Yoshino, and Toshiaki Yoshino.","issue":"4","publication_identifier":{"issn":["0021-9967"]},"scopus_import":"1","type":"journal_article","date_published":"1997-02-24T00:00:00Z","volume":378,"oa_version":"None","external_id":{"pmid":["9034907"]},"article_type":"original","article_processing_charge":"No","publisher":"Wiley-Blackwell","date_updated":"2022-08-22T13:34:53Z","doi":"10.1002/(SICI)1096-9861(19970224)378:4&lt;508::AID-CNE6&gt;3.0.CO;2-6","publication":"Journal of Comparative Neurology","month":"02","quality_controlled":"1","extern":"1","author":[{"full_name":"Li, Jin","first_name":"Jin","last_name":"Li"},{"last_name":"Kaneko","first_name":"Takeshi","full_name":"Kaneko, Takeshi"},{"orcid":"0000-0001-8761-9444","last_name":"Shigemoto","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","full_name":"Shigemoto, Ryuichi"},{"first_name":"Noboru","full_name":"Mizuno, Noboru","last_name":"Mizuno"}],"page":"508 - 521","date_created":"2018-12-11T11:58:28Z","day":"24","publist_id":"4323","publication_status":"published","year":"1997","language":[{"iso":"eng"}]}]