{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:31Z","timestamp":1761597331895,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651932"},{"type":"electronic","value":"9783540494980"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-65193-4_20","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:42:24Z","timestamp":1330299744000},"page":"114-152","source":"Crossref","is-referenced-by-count":53,"title":["Model checking timed automata"],"prefix":"10.1007","author":[{"given":"Sergio","family":"Yovine","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"4_CR1","unstructured":"A.V. Aho, J. E. Hopcroft and J. D. Ullman. The design and analysis of computer algorithms, Addison-Wesley, 1974."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"A. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. 13th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, 1992.","DOI":"10.1109\/REAL.1992.242667"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"A. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In W.R. Cleaveland, editor, CONCUR 92: Theories of Concurrency, pages 340\u2013354. Lecture Notes in Computer Science 630, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0084802"},{"issue":"1","key":"4_CR4","first-page":"414","volume":"104","author":"R. Alur","year":"1990","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th Symp. on Logics in Computer Science, pages 414\u2013425. IEEE Computer Society Press, 1990. See also \u201cModel checking in dense real time\u201d, Information and Computation, 104(1):2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"4_CR5","first-page":"322","volume":"126","author":"R. Alur","year":"1990","unstructured":"R. Alur and D. Dill. Automata for modeling real-time systems. In Proc. 17th ICALP, pages 322\u2013335. Lecture Notes in Computer Science 443, Springer-Verlag, 1990. See also \u201cA theory of timed automata\u201d, Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Logics and models of real-time: a survey","author":"R. Alur","year":"1991","unstructured":"R. Alur and T. Henzinger. Logics and models of real-time: a survey. In Netherlands, June 1991. Lecture Notes in Computer Science 600, Springer-Verlag."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"R. Alur, A. Itai, R. Kurshan, and M. Yannakakis. Timing verification by successive approximation. In Proc. 4th Workshop on Computer-Aided Verification. Lecture Notes in Computer Science 663, Springer-Verlag, 1992. Also in Information and Computation, 118(1):142\u2013157, 1995.","DOI":"10.1006\/inco.1995.1059"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"R. Alur and R.P. Kurshan. Timing analysis in COSPAN. In T.A. Henzinger R. Alur and E. Sontag, editors, Hybrid Systems III, pages 220\u2013231. LNCS 1066, Springer-Verlag, 1996.","DOI":"10.1007\/BFb0020948"},{"key":"4_CR9","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, editor, Proc. ] HART'97, pages 346\u2013360. LNCS 1201, Springer-Verlag, 1997.","DOI":"10.1007\/BFb0014737"},{"key":"4_CR10","volume-title":"Proc. 1996 IEEE Real-Time Systems Symposium, RTSS'96","author":"F. Balarin","year":"1996","unstructured":"F. Balarin. Approximate reachability analysis of timed automata. In Proc. 1996 IEEE Real-Time Systems Symposium, RTSS'96, Washington, DC, USA, December 1996. IEEE Computer Society Press."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61474-5_73","volume-title":"Proc. 8th Conference Computer-Aided Verification, CA V'96","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, W. Griffioen, K. Kristorffersen, K. Larsen, F. Larsson, P. Pettersson, and Wang Yi. Verification of an audio protocol with bus using Uppaal. In Proc. 8th Conference Computer-Aided Verification, CA V'96, pages 244\u2013256, Rutgers, NJ, July 1996. Lecture Notes in Computer Science 1102, Springer-Verlag."},{"key":"4_CR12","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247\u2013269, 1992.","journal-title":"Science of Computer Programming"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, Y. Lakhnech, and S. Yovine. Model checking for extended timed temporal logics. In Proc. 4th Intl. Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT'96, Uppsala, Sweden, September 1996.","DOI":"10.1007\/3-540-61648-9_48"},{"key":"4_CR14","volume-title":"Proc. 18th IEEE Real-Time Systems Symposium, RTSS'97","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model-checking for real-time systems. In Proc. 18th IEEE Real-Time Systems Symposium, RTSS'97, San Francisco, USA, December 1997. IEEE Computer Society Press."},{"key":"4_CR15","volume-title":"Proc. 1997 Computer-Aided Verification, CAV'97","author":"M. Bozga","year":"1997","unstructured":"M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In Proc. 1997 Computer-Aided Verification, CAV'97, Israel, June 1997. to appear in LNCS, Springer-Verlag."},{"issue":"8","key":"4_CR16","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677\u2013692, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"J.B. Burch, E.M. Clarke, D.Dill, L.J. Hwang, and K.L. McMillan. Symbolic model checking: 1020 states and beyond. In Proc. 5th Symp. on Logics in Computer Science, pages 428\u2013439. IEEE Computer Society Press, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"K. \u010cerans. Decidability of bisimulation equivalences for parallel timer processes. In Proc. 4th Workshop on Computer-Aided Verification. Lecture Notes in Computer Science 663, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56496-9_24"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"K. Cerans, J. C. Godskesen, and K. G. Larsen. Timed modal specifications-theory and tools. In C. Courcoubetis, editor, Proc. 5th Computer-Aided Verification, pages 253\u2013267. LNCS 697, Springer-Verlag, June 1993.","DOI":"10.1007\/3-540-56922-7_21"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis, D. Dill, M. Chatzaki, and P. Tsounakis. Verification with realtime COSPAN. In Proc. 4th Workshop on Computer-Aided Verification. Lecture Notes in Computer Science 663, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56496-9_22"},{"key":"4_CR21","volume-title":"Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95","author":"C. Daws","year":"1995","unstructured":"C. Daws and S. Yovine. Two examples of verification of multirate timed automata with KRONOS. In Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95, Pisa, Italy, December 1995. IEEE Computer Society Press."},{"key":"4_CR22","volume-title":"Proc. 1996 IEEE Real-Time Systems Symposium, RTSS'96","author":"C. Daws","year":"1996","unstructured":"C. Daws and S. Yovine. Reducing the number of clock variables of timed automata. In Proc. 1996 IEEE Real-Time Systems Symposium, RTSS'96, Washington, DC, USA, December 1996. IEEE Computer Society Press."},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. ist Workshop on Computer-Aided Verification","author":"D. Dill","year":"1989","unstructured":"D. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Proc. ist Workshop on Computer-Aided Verification, France, 1989. Lecture Notes in Computer Science 407, Springer-Verlag."},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-60045-0_66","volume-title":"Proceedings of the Seventh Conference on Computer-Aided Verification, CAV'95","author":"D. L. Dill","year":"1995","unstructured":"D. L. Dill and H. Wong-Toi. Verification of real-time systems by successive over and under approximation. In Pierre Wolper, editor, Proceedings of the Seventh Conference on Computer-Aided Verification, CAV'95, Lecture Notes in Computer Science 939, pages 409\u2013422, Liege, Belgium, 1995. Springer-Verlag."},{"key":"4_CR25","unstructured":"E.A. Emerson and E. Clarke. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Workshop on Logic of Programs. Lecture Notes in Computer Science 131, Springer-Verlag, 1981."},{"key":"4_CR26","unstructured":"J.C. Fernandez and L. Mounier. On the fly verification of behavioural equivalences and preorders. In Proc. CAV'91. LNCS 757, Springer-Verlag, 1991."},{"key":"4_CR27","unstructured":"A. G\u00f6ll\u00fc, A. Puri, and P. Varaiya. Discretization of timed automata. In Proc. 33rd CDC, 1994."},{"key":"4_CR28","unstructured":"Z. Har'El and R. Kurshan. Automatic verification of coordinating systems. In J. Sifakis, editor, Proc. 1st Workshop on Computer-Aided Verification. Lecture Notes in Computer Science 407, Springer-Verlag, 1989."},{"key":"4_CR29","volume-title":"Proc. 18th IEEE Real-Time Systems Symposium, RTSS'95","author":"K. Havelund","year":"1997","unstructured":"K. Havelund, A. Skou, K. G. Larsen, and K. Lund. Formal modelling and analysis of an audio\/video protocol: an industrial case study using uppaal. In Proc. 18th IEEE Real-Time Systems Symposium, RTSS'95, San Francisco, California, USA, December 1997. IEEE Computer Society Press."},{"key":"4_CR30","volume-title":"Proc. REX Workshop \u201cReal-Time: Theory in Practice","author":"T.A. Henzinger","year":"1992","unstructured":"T.A. Henzinger, Z. Manna, and A. Pnueli. What good are digital clocks? In Proc. REX Workshop \u201cReal-Time: Theory in Practice\u201d, New York, 1992. Springer-Verlag."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In Proc. 7th Symp, on Logics in Computer Science, pages 394\u2013406. IEEE Computer Society Press, 1992. Also in Information and Computation, 111(2):193\u2013244, 1994.","DOI":"10.1006\/inco.1994.1045"},{"key":"4_CR32","unstructured":"R. Jain. FDDI handbook: high-speed networking using fiber and other media. Addison-Wesley, 1994."},{"key":"4_CR33","volume-title":"Proc. 18th IEEE Real-Time Systems Symposium, RTSS'95","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, F. Larsson, P. Pettersson, and Wang Yi. Efficient verification of real-time systems: compact data structure and state-space reduction. In Proc. 18th IEEE Real-Time Systems Symposium, RTSS'95, San Francisco, California, USA, December 1997. IEEE Computer Society Press."},{"key":"4_CR34","volume-title":"Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95","author":"K. G. Larsen","year":"1995","unstructured":"K. G. Larsen, P. Petterson, and Wang Yi. Compositional and symbolic model-checking of real-time systems. In Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95, Pisa, Italy, December 1995. IEEE Computer Society Press."},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"K. G. Larsen and Y. Wang. Timed abstracted bisimulation: implicit specification and decidability. In Proc. MFPS'93, 1993.","DOI":"10.1007\/3-540-58027-1_8"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"D. Lee and M. Yannakakis. Online minimization of transition systems. In ACM Symp. on Theory of Computing. ACM Press, 1992.","DOI":"10.1145\/129712.129738"},{"key":"4_CR37","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":"4_CR38","volume-title":"Protocol Specification, Testing and Verification, III","author":"M. Measche","year":"1983","unstructured":"M. Measche and B. Berthomieu. Time petri-nets for analyzing and verifying time dependent communication protocols. In H. Rudin and C.H. West, editors, Protocol Specification, Testing and Verification, III. IFIP, North-Holland, 1983."},{"key":"4_CR39","unstructured":"A. Olivero. Mod\u00e9lisation et analyse de syst\u00e8mes temporises et hybrides. Th\u00e8se, Institut National Polytechnique de Grenoble, Grenoble, France, September 1994."},{"key":"4_CR40","first-page":"130","volume-title":"Proc. FTRTFT'96","author":"J.G. Springintveld","year":"1996","unstructured":"J.G. Springintveld and F.W. Vaandrager. Minimizable timed automata. In B. Jonsson and J. Parrow, editors, Proc. FTRTFT'96, Uppsala, Sweden, 1996. LNCS 1135, 130\u2013147, Springer-Verlag."},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"S. Tripakis and C. Courcoubetis. Extending promela and spin for real time. In TACAS'96, Passau, Germany, 1996. Lecture Notes in Computer Science 1055, Springer-Verlag.","DOI":"10.1007\/3-540-61042-1_53"},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-61474-5_72","volume-title":"Proc. 8th Conference Computer-Aided Verification, CAV'96","author":"S. Tripakis","year":"1996","unstructured":"S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Proc. 8th Conference Computer-Aided Verification, CAV'96, pages 232\u2013243, Rutgers, NJ, July 1996. Lecture Notes in Computer Science 1102, Springer-Verlag."},{"key":"4_CR43","unstructured":"VERIMAG. School on Methods and Tools for the Verification of Infinite-State Systems. http:\/\/www.imag.fr\/VERIMAG. Grenoble, France, March 1997."},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"C. Weise and D. Lenzkes. Efficient scaling invariant checking of timed bisimulation. In STACS'97. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0023458"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Howard Wong-Toi and David L. Dill. Approximations for verifying timing properties. In Teo Rus and Charles Rattray, editors, Theories and Experiences for Real-Time System Development (Proceedings First AMAST Workshop on Real Time System Development, chapter 7, pages 177\u2013204. World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0007"},{"key":"4_CR46","unstructured":"S. Yovine. M\u00e9thodes et outils pour la verification symbolique de syst\u00e8mes temporis\u00e9s. Th\u00e8se, Institut National Polytechnique de Grenoble, Grenoble, France, May 1993."}],"container-title":["Lecture Notes in Computer Science","Lectures on Embedded Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-65193-4_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:48:08Z","timestamp":1742600888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-65193-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651932","9783540494980"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/3-540-65193-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}