{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T04:37:58Z","timestamp":1776487078581,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028779","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"546-550","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":132,"title":["Kronos: A model-checking tool for real-time systems"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Conrado","family":"Daws","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfredo","family":"Olivero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"issue":"1","key":"54_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"54_CR2","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.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"54_CR3","unstructured":"A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of the 18th IEEE Real-Time Systems Symposium, 1997."},{"key":"54_CR4","doi-asserted-by":"crossref","unstructured":"M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In CAV'97, 1997.","DOI":"10.1007\/3-540-63166-6_19"},{"key":"54_CR5","doi-asserted-by":"crossref","unstructured":"S. Bradley, W. Henderson, D. Kendall, and A. Robson. Validation, verification and implementation of timed protocols using AORTA. In Proc. 15th PSTV, 1995.","DOI":"10.1007\/978-0-387-34892-6_13"},{"key":"54_CR6","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. Technical report, Carnegie Mellon University, 1992.","DOI":"10.1145\/136035.136043"},{"key":"54_CR7","doi-asserted-by":"crossref","unstructured":"C. Daws. Optikron: a tool suite for enhancing model-checking of real-time systems. 1998. TO appear in CAV'98.","DOI":"10.1007\/BFb0028778"},{"key":"54_CR8","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, 1996.","DOI":"10.1007\/BFb0020947"},{"key":"54_CR9","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, and S. Yovine. Verifying ET-LOTOS programs with KRONOS. In FORTE'94, 1994.","DOI":"10.1007\/978-0-387-34878-0_17"},{"key":"54_CR10","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In TACAS'98, 1998.","DOI":"10.1007\/BFb0054180"},{"key":"54_CR11","unstructured":"C. Daws and S. Yovine. Two examples of verification of multirate timed automata with KRONOS. In RTSS'95, 1995."},{"key":"54_CR12","unstructured":"C. Daws and S. Yovine. Reducing the number of clock variables of timed automata. In RTSS'96, 1996."},{"key":"54_CR13","doi-asserted-by":"crossref","unstructured":"D. Dill. Timing assumptions and verification of finite-state concurrent systems. In CAV'89, 1989.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"54_CR14","doi-asserted-by":"crossref","unstructured":"J.Cl. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A tool box for the verification of lotos programs. In 14th International Conference on Software Engineering, 1992.","DOI":"10.1145\/143062.143124"},{"issue":"2","key":"54_CR15","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"54_CR16","doi-asserted-by":"crossref","unstructured":"M. Jourdan, F. Maraninchi, and A. Olivero. Verifying quantitative real-time properties of synchronous programs. In CAV'93, 1993.","DOI":"10.1007\/3-540-56922-7_29"},{"key":"54_CR17","unstructured":"O. Maler and S. Yovine. Hardware timing verification using KRONOS. In Proc. 7th Israeli Conference on Computer Systems and Software Engineering, 1996."},{"issue":"9","key":"54_CR18","first-page":"794","volume":"18","author":"X. Nicollin","year":"1992","unstructured":"X. Nicollin, J. Sifakis, and S. Yovine. Compiling real-time specifications into extended automata. IEEE TSE Special Issue on Real-Time Systems, 18(9):794\u2013804, September 1992.","journal-title":"IEEE TSE Special Issue on Real-Time Systems"},{"key":"54_CR19","doi-asserted-by":"crossref","unstructured":"A. Olivero, J. Sifakis, and S. Yovine. Using abstractions for the verification of linear hybrid systems. In CAV'94, 1994.","DOI":"10.1007\/3-540-58179-0_45"},{"key":"54_CR20","unstructured":"S. Tripakis and S Yovine. Verification of the fast-reservation protocol with delayed transmission using Kronos. Technical Report 95-23, Verimag, 1995."},{"key":"54_CR21","doi-asserted-by":"crossref","unstructured":"S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In CAV'96, 1996.","DOI":"10.1007\/3-540-61474-5_72"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028779","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:00:17Z","timestamp":1558270817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028779"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0028779","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"18 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}