{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T16:08:23Z","timestamp":1770912503227,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540602491","type":"print"},{"value":"9783540447702","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60249-6_41","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:58:30Z","timestamp":1330279110000},"page":"62-88","source":"Crossref","is-referenced-by-count":111,"title":["Model-checking for real-time systems"],"prefix":"10.1007","author":[{"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. An Old-Fashioned Recipe for Real Time. Lecture Notes in Computer Science, 600, 1993.","DOI":"10.1007\/BFb0031985"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for Real-Time Systems. In Proceedings of Logic in Computer Science, pages 414\u2013425. IEEE Computer Society Press, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"issue":"2","key":"4_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. Automata for Modelling Real-Time Systems. Theoretical Computer Science, 126(2): 183\u2013236, April 1994.","journal-title":"Theoretical Computer Science"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. Partial Model Checking. To appear in Proceedings of LICS'95, 1995.","DOI":"10.1109\/LICS.1995.523274"},{"key":"4_CR5","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 states and beyond. Logic in Computer Science, 1990."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"K. Cerans, J. C. Godskesen, and K. G. Larsen. Timed modal specifications \u2014 theory and tools. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV'93.","DOI":"10.1007\/3-540-56922-7_21"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV'93.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Gr\u00fcmberg, and D. E. Long. Model Checking and Abstraction. Principles of Programming Languages, 1992.","DOI":"10.1145\/143165.143235"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In Proceedings of 7th International Conference on Formal Description Techniques, 1994.","DOI":"10.1007\/978-0-387-34878-0_17"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. S. Jutla. Symmetry and Model Checking. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV'93.","DOI":"10.1007\/3-540-56922-7_38"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. A Partial Approach to Model Checking. Logic in Computer Science, 1991.","DOI":"10.1109\/LICS.1991.151664"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"J.C. Godskesen and K.G. Larsen. Synthesizing Distinghuishing Formulae for Real Time Systems \u2014 Extended Abstract. Lecture Notes in Computer Science, 1995. To occur in Proceedings of MFCS'95. Also BRICS report series RS-94-48.","DOI":"10.1007\/3-540-60246-1_157"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Nicolas Halbwachs. Delay Analysis in Synchronous Programs. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV'93.","DOI":"10.1007\/3-540-56922-7_28"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, Z. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Logic in Computer Science, 1992.","DOI":"10.1109\/LICS.1992.185551"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger and Pei-Hsin Ho. HyTech: The Cornell HYbrid TECH-nology Tool. To appear in the Proceedings of TACAS, Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995.","DOI":"10.1007\/3-540-60472-3_14"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"H. H\u00fcttel and K. G. Larsen. The use of static constructs in a modal process logic. Lecture Notes in Computer Science, Springer Verlag, 363, 1989.","DOI":"10.1007\/3-540-51237-3_14"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"F. Laroussinie, K. G. Larsen, and C. Weise. From Timed Automata to Logic \u2014 and Back. Lecture Notes in Computer Science, 1995. To occur in Proceedings of MFCS. Also BRICS report series RS-95-2.","DOI":"10.7146\/brics.v2i2.19504"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"F. Laroussinie and K.G. Larsen. Compositional Model Checking of Real Time Systems. Lecture Notes in Computer Science, 1995. To appear in Proceedings of CONCUR'95. Also BRICS report series RS-95-19.","DOI":"10.1007\/3-540-60218-6_3"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"N. Shankar. Verification of REal-Time Systems Using PVS. Lecture Notes in Computer Science, 697, 1993. In Proceedings of CAV'93.","DOI":"10.1007\/3-540-56922-7_23"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"A. Valmari. A Stubborn Attack on State Explosion. Theoretical Computer Science, 3, 1990.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"4_CR22","unstructured":"Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Systems By Constraint-Solving. In the Proceedings of the 7th International Conference on Formal Description Techniques, 1994."}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Computation Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60249-6_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T09:34:39Z","timestamp":1640943279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60249-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602491","9783540447702"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-60249-6_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}