{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:29Z","timestamp":1761597329669},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631668"},{"type":"electronic","value":"9783540691952"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:13:14Z","timestamp":1330279994000},"page":"179-190","source":"Crossref","is-referenced-by-count":41,"title":["Some progress in the symbolic verification of timed automata"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","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":"Sergio","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"19_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"},{"key":"19_CR2","doi-asserted-by":"crossref","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, 2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"19_CR3","unstructured":"R. Alur and T.A. Henzinger, Logics and Models for Real-Time: A survey, J.W. de Bakker et al (Eds.), Real-Time: Theory in Practice, LNCS 600, 74\u2013106, Springer, 1992."},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1995.1059","volume":"118","author":"R. Alur","year":"1995","unstructured":"R. Alur, A. Itai, R.P. Kurshan and M. Yanakakis, Timing Verification by Successive Approximation, Information and Computation 118, 142\u2013157, 1995.","journal-title":"Information and Computation"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur, and R.P. Kurshan, Timing Analysis in COSPAN, in R. Alur, T.A. Henzinger and E. Sontag (Eds.), Hybrid Systems III, LNCS 1066, 220\u2013231, Springer, 1996.","DOI":"10.1007\/BFb0020948"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli and A. Rasse, Data-Structures for the Verification of Timed Automata, in O. Maler (Ed.), Proc. HART'97, LNCS 1201, 346\u2013360, Springer, 1997.","DOI":"10.1007\/BFb0014737"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"E. Asarin, P. Caspi and O. Maler, A Kleene Theorem for Timed Automata, Proc. LICS'97, 1997.","DOI":"10.1109\/LICS.1997.614944"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"E. Asarin, O. Maler and A. Pnueli, Symbolic Controller Synthesis for Discrete and Timed Systems, in P. Antsaklis et al (Eds.), Hybrid Systems II, LNCS 999, 1\u201320, Springer, 1995.","DOI":"10.1007\/3-540-60472-3_1"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"F. Balarin, Approximate Reachability Analysis of Timed Automata, Proc. RTSS'96, 52\u201361, IEEE, 1996.","DOI":"10.1109\/REAL.1996.563700"},{"key":"19_CR10","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"B. Berthomieu and M. Diaz, Modeling and Verification of Time Dependent Systems using Time Petri Nets, IEEE Trans. on Software Engineering 17, 259\u2013273, 1991.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"19_CR11","unstructured":"M. Bozga, J.-C. Fernandez and A. Kerbrat, A Symbolic \u03bc-calculus Model Checker for Automata with Variables, Unpublished Manuscript, Verimag, 1996. http:\/\/www.imag.fr\/VERIMAG\/DIST_SYS\/SMI\/"},{"key":"19_CR12","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"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"J.A. Brzozowski and C-J.H. Seger, Asynchronous Circuits, Springer, 1994.","DOI":"10.1007\/978-1-4612-4210-9"},{"key":"19_CR14","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":"19_CR15","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.), Theories and Experiences for Real-Time System Development, World Scientific, 1995.","DOI":"10.1142\/9789812831583_0005"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine, The Tool KRONOS, in R. Alur, T.A. Henzinger and E. Sontag (Eds.), Hybrid Systems III, LNCS 1066, 208\u2013219, Springer, 1996.","DOI":"10.1007\/BFb0020947"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero and S. Yovine, Verifying et-lotos Programs with kronos, Proc. FORTE'94, Bern, 1994.","DOI":"10.1007\/978-0-387-34878-0_17"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine, Two Examples of Verification of Multirate Timed Automata with KRONOS, Proc. RTSS'95, 66\u201375, IEEE, 1995.","DOI":"10.1109\/REAL.1995.495197"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine, Reducing the Number of Clock Variables of Timed Automata, Proc. RTSS'96, 73\u201381, IEEE, 1996.","DOI":"10.1109\/REAL.1996.563702"},{"key":"19_CR20","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, 197\u2013212, Springer, 1989.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"19_CR21","unstructured":"A. G\u00f6ll\u00fc, A. Puri and P. Varaiya, Discretization of Timed Automata, Proc. 33rd CDC, 1994."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, Delay Analysis in Synchronous Programs, in C. Courcoubetis (Ed.), Proc. CAV'93, LNCS 697, 333\u2013346, Springer, 1993.","DOI":"10.1007\/3-540-56922-7_28"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"T. Henzinger, Z. Manna, and A. Pnueli, Timed Transition Systems, in J.W. de Bakker et al (Eds.), Real-Time: Theory in Practice, LNCS 600, 226\u2013251, Springer, 1992.","DOI":"10.1007\/BFb0031995"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"T. Henzinger, Z. Manna, and A. Pnueli. What Good are Digital Clocks?, in W. Kuich (Ed.), Proc. ICALP'92, LNCS 623, 545\u2013558, Springer, 1992.","DOI":"10.1007\/3-540-55719-9_103"},{"key":"19_CR25","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 Modelchecking for Real-time Systems, Information and Computation 111, 193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, P. Pettersson and W. Yi, Compositional and Symbolic Model-Checking of Real-time Systems, Proc. RTSS'95, 76\u201387, IEEE, 1995.","DOI":"10.1109\/REAL.1995.495198"},{"key":"19_CR27","unstructured":"H.R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989."},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"O. Maler and A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, in P.E. Camurati, H. Eveking (Eds.), Proc. CHARME'95, LNCS 987, 189\u2013205, Springer, 1995.","DOI":"10.1007\/3-540-60385-9_12"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"O. Maler and S. Yovine. Hardware Timing Verification using KRONOS, In Proc. 7th Israeli Conference on Computer Systems and Software Engineering, Herzliya, Israel, June 1996.","DOI":"10.1109\/ICCSSE.1996.554845"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model-Checking: an Approach to the State-Explosion problem, Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"X. Nicollin and J. Sifakis, An Overview and Synthesis of Timed Process Algebra, in J.W. de Bakker et al (Eds.), Real-Time.: Theory in Practice, LNCS 600, 526\u2013548, Springer, 1992.","DOI":"10.1007\/BFb0032006"},{"key":"19_CR32","unstructured":"F. Somenzi, CUDD: CU Decision Diagram Package, 1995."},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi and D.L. Dill, Approximations for Verifying Timing Properties, in T. Rus and C. Rattray (Eds.), Theories and Experiences for Real-Time System Development, World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0007"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:16:40Z","timestamp":1605629800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}