{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:19:14Z","timestamp":1742635154255},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_11","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"125-141","source":"Crossref","is-referenced-by-count":25,"title":["Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"11_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":"11_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/BFb0031988","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1992","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":"11_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0020948","volume-title":"Hybrid Systems III","author":"R. Alur","year":"1996","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."},{"key":"11_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Proc. HART\u201997","author":"E. Asarin","year":"1997","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\u201997, LNCS 1201, 346\u2013360, Springer, 1997."},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/BFb0055642","volume-title":"Proc. Concur\u201998","author":"E. Asarin","year":"1998","unstructured":"E. Asarin, O. Maler and A. Pnueli, On the Discretization of Delays in Timed Automata and Digital Circuits, in R. de Simone and D. Sangiorgi (Eds), Proc. Concur\u201998, LNCS 1466, 470\u2013484, Springer, 1998."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"F. Balarin, Approximate Reachability Analysis of Timed Automata, Proc. RTSS\u201996, 52\u201361, IEEE, 1996.","DOI":"10.1109\/REAL.1996.563700"},{"key":"11_CR7","unstructured":"M. Bozga, SMI: An Open Toolbox for Symbolic Protocol Verification, Technical Report 97-10, Verimag, 1997. http:\/\/www.imag.fr\/VERIMAG\/DIST_SYS\/SMI\/"},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","first-page":"403","volume-title":"Proc. CAV\u201998","author":"W. Belluomini","year":"1997","unstructured":"W. Belluomini and C. J. Myers, Verification of Timed Systems Using POSETs, in A. J. Hu and M. Y. Vardi (Eds.), Proc. CAV\u201998, 403\u2013415, LNCS 1427, Springer, 1997."},{"key":"11_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-63166-6_19","volume-title":"Proc. CAV\u201997","author":"M. Bozga","year":"1997","unstructured":"M. Bozga, O. Maler, A. Pnueli, S. Yovine, Some Progress in the Symbolic Verification of Timed Automata, in O. Grumberg (Ed.) Proc. CAV\u201997, 179\u2013190, LNCS 1254, Springer, 1997."},{"key":"11_CR10","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":"11_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C. Daws","year":"1996","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."},{"key":"11_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS\u201998","author":"C. Daws","year":"1998","unstructured":"C. Daws and S. Tripakis, Model checking of Real-time Reachability Properties using Abstractions, Proc. TACAS\u201998, LNCS 1384, 1998."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine, Reducing the Number of Clock Variables of Timed Automata, Proc. RTSS\u201996, 73\u201381, IEEE, 1996.","DOI":"10.1109\/REAL.1996.563702"},{"key":"11_CR14","series-title":"Lect Notes Comput Sci","first-page":"197","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D. L. Dill","year":"1989","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."},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201993","author":"J. C. Fernandez","year":"1993","unstructured":"J. C. Fernandez, A. Kerbrat, and L. Mounier, Symbolic Equivalence Checking, In C. Courcoubetis (Ed.), Proc. CAV\u201993, LNCS 697, Springer, 1993."},{"key":"11_CR16","unstructured":"M. R. Greenstreet, STARI: Skew Tolerant Communication, to appear in IEEE Transactions on Computers, 1997."},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Proc. CAV\u201993","author":"N. Halbwachs","year":"1993","unstructured":"N. Halbwachs, Delay Analysis in Synchronous Programs, in C. Courcoubetis (Ed.), Proc. CAV\u201993, LNCS 697, 333\u2013346, Springer, 1993."},{"key":"11_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Proc. ICALP\u201992","author":"T. Henzinger","year":"1992","unstructured":"T. Henzinger, Z. Manna, and A. Pnueli. What Good are Digital Clocks?, in W. Kuich (Ed.), Proc. ICALP\u201992, LNCS 623, 545\u2013558, Springer, 1992."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"K. Larsen, F. Larsson, P. Pettersson and W. Yi, Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction, Proc. RTSS\u201998, 14\u201324, 1997.","DOI":"10.1109\/REAL.1997.641265"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"K. G. Larsen, P. Pettersson and W. Yi, UPPAAL in a Nutshell, Software Tools for Technology Transfer 1\/2, 1997.","DOI":"10.1007\/s100090050010"},{"key":"11_CR21","unstructured":"H. R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989."},{"key":"11_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-60385-9_12","volume-title":"Proc. CHARME\u201995","author":"O. Maler","year":"1995","unstructured":"O. Maler and A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, in P. E. Camurati, H. Eveking (Eds.), Proc. CHARME\u201995, LNCS 987, 189\u2013205, Springer, 1995."},{"key":"11_CR23","unstructured":"F. Somenzi, CUDD: CU Decision Diagram Package, 1995."},{"key":"11_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/3-540-61648-9_38","volume-title":"Proc. FTRTFT\u201996","author":"J. Springintveld","year":"1996","unstructured":"J. Springintveld and F. W. Vaandrager, Minimizable Timed Automata, in B. Jonsson and J. Parrow (Eds.), Proc. FTRTFT\u201996, LNCS 1135, 130\u2013147, Springer, 1996."},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"S. Tasiran R. Alur, R. P. Kurshan and R. Brayton, Verifying Abstractions of Timed Systems, in Proc. CONCUR\u201996, 546\u2013562, Springer, 1996.","DOI":"10.1007\/3-540-61604-7_75"},{"key":"11_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/3-540-63166-6_20","volume-title":"Proc. CAV\u201997","author":"S. Tasiran","year":"1997","unstructured":"S. Tasiran and R. K. Brayton, STARI: A Case Study in Compositional and Hierarchical Timing Verification, in O. Grumberg (Ed.) Proc. CAV\u201997, 191\u2013201, LNCS 1254, Springer, 1997."},{"key":"11_CR27","unstructured":"S. Tasiran, Y. Kukimoto and R. K. Brayton, Computing Delay with Coupling using Timed Automata, Proc. TAU\u201997, 1997."},{"key":"11_CR28","unstructured":"R. J. van Glabbeek and W. P. Weijland, Branching-Time and Abstraction in Bisimulation Semantics (extended abstract), CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989."},{"key":"11_CR29","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"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"T. Yoneda and H. Ryu, Timed Trace Theoretic Verification Using Partial Order Reductions, in Proc. Async\u201999, 108\u2013121, IEEE Press, 1999.","DOI":"10.1109\/ASYNC.1999.761527"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:00:54Z","timestamp":1558983654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}