{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T14:38:44Z","timestamp":1761662324539,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626008"},{"type":"electronic","value":"9783540683308"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":[[1997]]},"DOI":"10.1007\/bfb0014737","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:12:52Z","timestamp":1132737172000},"page":"346-360","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":46,"title":["Data-structures for the verification of timed automata"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Asarin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Kerbrat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anne","family":"Rasse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","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"},{"doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. In IEEE Real-time Systems Symposium, pages 2\u201311, 1993.","key":"31_CR2","DOI":"10.1109\/REAL.1993.393520"},{"doi-asserted-by":"crossref","unstructured":"J. Bengtsson, W.O.D. Griffioen, K.J. Kristoffersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an audio protocol with bus collision using UPPAAL. In R. Alur and T.A. Henzinger (Eds. Proc. CAV'96, LNCS 1102, 244\u2013256, Springer, 1996.","key":"31_CR3","DOI":"10.1007\/3-540-61474-5_73"},{"key":"31_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. on Computers C-35, 677\u2013691, 1986.","journal-title":"IEEE Trans. on Computers"},{"unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, Symbolic Model-Checking: 1020 States and Beyond, Proc. LICS'90, Philadelphia, 1990.","key":"31_CR5"},{"doi-asserted-by":"crossref","unstructured":"S.V. Campos and E.M. Clarke. Real-time symbolic model checking for discrete time models, in T. Rus and C. Rattray (Eds.), AMAST Series in Computing: Theories and Experiences for Real-Time System Development, World Scientific, 1995.","key":"31_CR6","DOI":"10.21236\/ADA282878"},{"doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero and S. Yovine, Verifying et-lotos Programs with Kronos, Proc. FORTE'94, Bern, 1994.","key":"31_CR7","DOI":"10.1007\/978-0-387-34878-0_17"},{"doi-asserted-by":"crossref","unstructured":"D.L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, in J. Sifakis (Ed.), Automatic Verification Methods for Finite State Systems, LNCS 407, Springer, 1989.","key":"31_CR8","DOI":"10.1007\/3-540-52148-8_17"},{"unstructured":"M. Bozga, J.-C. Fernandez, A. Kerbrat, A Symbolic \u03bc-calculus Model Checker for Automata with Variables, Unpublished Manuscript, Verimag, 1996.","key":"31_CR9"},{"unstructured":"A. G\u00f6ll\u00fc, A. Puri and P. Varaiya, Discretization of Timed Automata, Proc. 33rd CDC, 1994.","key":"31_CR10"},{"key":"31_CR11","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Model-checking for Real-time Systems, Information and Computation 111, 193\u2013244, 1994.","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"O. Maler and A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, in P.E. Camurati and H. Eveking (Eds.), Proc. CHARME'95, 189\u2013205, LNCS 987, Springer, 1995.","key":"31_CR12","DOI":"10.1007\/3-540-60385-9_12"},{"doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model-Checking: an Approach to the State-Explosion problem, Kluwer, 1993.","key":"31_CR13","DOI":"10.1007\/978-1-4615-3190-6"},{"unstructured":"F. Somenzi, CUDD: CU Decision Diagram Package, 1995.","key":"31_CR14"},{"doi-asserted-by":"crossref","unstructured":"A. Rauzy, Toupie=\u03bc-calculus + constraints. In P. Wolper, editor, Proc. CAV'95, LNCS 939, 114\u2013126, Springer, 1995.","key":"31_CR15","DOI":"10.1007\/3-540-60045-0_44"},{"doi-asserted-by":"crossref","unstructured":"P. Wolper and B. Boigelot. An automata-theoretic approach to presburger arithmetic constraints. In Proc. Static Analysis Symposium, LNCS 983, 21\u201332, Springer, 1995.","key":"31_CR16","DOI":"10.1007\/3-540-60360-3_30"}],"container-title":["Lecture Notes in Computer Science","Hybrid and Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014737","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T21:49:24Z","timestamp":1736113764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626008","9783540683308"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0014737","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}