{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:08:30Z","timestamp":1761620910835},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,5]]},"DOI":"10.1007\/s10703-005-1632-8","type":"journal-article","created":{"date-parts":[[2005,8,31]],"date-time":"2005-08-31T09:22:44Z","timestamp":1125480164000},"page":"267-292","source":"Crossref","is-referenced-by-count":47,"title":["Checking Timed B\u00fcchi Automata Emptiness Efficiently"],"prefix":"10.1007","volume":"26","author":[{"given":"Stavros","family":"Tripakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1632_CR1","doi-asserted-by":"crossref","unstructured":"K. Altisen, G. Goessler, A. Pnueli, J. Sifakis, and S. Tripakis, \u201cA framework for scheduler synthesis,\u201d in IEEE Real-Time Systems Symposium, RTSS\u201999, 1999.","DOI":"10.1109\/REAL.1999.818838"},{"key":"1632_CR2","unstructured":"Rajeev Alur, \u201cTechniques for automatic verification of real-time systems\u201d, PhD thesis, Department of Computer Science, Stanford University, 1991."},{"issue":"1","key":"1632_CR3","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, \u201cModel checking in dense real time,\u201d Information and Computation, Vol. 104, No. 1, pp. 2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"1632_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D.L. Dill, and H. Wong-Toi, \u201cMinimization of timed transition systems,\u201d in 3rd Conference on Concurrency Theory CONCUR \u201892, volume 630 of Lecture Notes in Computer Science, Springer-Verlag, 1992, pp. 340\u2013354.","DOI":"10.1007\/BFb0084802"},{"key":"1632_CR5","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, \u201cA theory of timed automata,\u201d Theoretical Computer Science, Vol. 126, pp. 183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"1632_CR6","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, S. Tripakis, and S. Yovine, \u201cOn-the-fly symbolic model checking for real-time systems,\u201d in Proc. of the 18th IEEE Real-Time Systems Symposium, San Francisco, CA, IEEE, December 1997, pp. 25\u201334.","DOI":"10.1109\/REAL.1997.641266"},{"key":"1632_CR7","unstructured":"M. Bozga, \u201cSmi: An open toolbox for symbolic protocol verification,\u201d Technical report, VERIMAG, 1997."},{"issue":"3","key":"1632_CR8","first-page":"315","volume":"E80-D","author":"J. Cortadella","year":"1997","unstructured":"J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev, \u201cPetrify: A tool for manipulating concurrent specifications and synthesis of asynchronous controllers,\u201d IEICE Transactions on Information and Systems, Vol. E80-D, No. 3, pp. 315\u2013325, 1997.","journal-title":"IEICE Transactions on Information and Systems"},{"key":"1632_CR9","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, \u201cMemory efficient algorithms for the verification of temporal properties,\u201d Formal Methods in System Design, Vol. 1, pp. 275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"1632_CR10","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis, \u201cMinimum and maximum delay problems in real-time systems,\u201d in Computer-Aided Verification, LNCS 575, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-55179-4_37"},{"key":"1632_CR11","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine, \u201cThe tool KRONOS,\u201d in Hybrid Systems III, Verification and Control, volume 1066 of LNCS, Springer-Verlag, 1996, pp. 208\u2013219.","DOI":"10.1007\/BFb0020947"},{"key":"1632_CR12","doi-asserted-by":"crossref","unstructured":"D.L. Dill, \u201cTiming assumptions and verification of finite-state concurrent systems,\u201d in J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag, 1989, pp. 197\u2013212.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"1632_CR13","doi-asserted-by":"crossref","unstructured":"T. Henzinger, O. Kupferman, and M. Vardi, \u201cA space-efficient on-the-fly algorithm for real-time model-checking,\u201d in CONCUR\u201996. LNCS 1119, 1996.","DOI":"10.1007\/3-540-61604-7_73"},{"issue":"2","key":"1632_CR14","doi-asserted-by":"crossref","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, \u201cSymbolic model checking for real-time systems,\u201d Information and Computation, Vol. 111, No. 2, pp. 193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"1632_CR15","doi-asserted-by":"crossref","unstructured":"L. Lamport, \u201cSometimes is sometimes \u201cnot never\u201d\u2014on the temporal logic of programs,\u201d in 7th ACM Symp. POPL, 1980, pp. 174\u2013185.","DOI":"10.1145\/567446.567463"},{"key":"1632_CR16","doi-asserted-by":"crossref","unstructured":"K. Larsen, P. Petterson, and W. Yi, \u201cUppaal in a nutshell,\u201d Software Tools for Technology Transfer, Vol. 1, Nos. (1\/2), 1997.","DOI":"10.1007\/s100090050010"},{"key":"1632_CR17","doi-asserted-by":"crossref","unstructured":"D. Lee and M. Yannakakis, \u201cOnline minimization of transition systems,\u201d in ACM Symp. on Theory of Computing, 1992.","DOI":"10.1145\/129712.129738"},{"key":"1632_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification,\u201d in 12th ACM Symp. POPL, New Orleans, January 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"1632_CR19","doi-asserted-by":"crossref","unstructured":"O. Maler and A. Pnueli, \u201cTiming analysis of asynchronous circuits using timed automata,\u201d in P.E. Camurati, H. Eveking (Eds.), Proc. CHARME\u201995. LNCS 987, Springer Verlag, 1995.","DOI":"10.1007\/3-540-60385-9_12"},{"key":"1632_CR20","doi-asserted-by":"crossref","unstructured":"R. Paige and R. Tarjan, \u201cThree partition refinement algorithms,\u201d SIAM Journal on Computing, Vol. 16, No. 6, 1987.","DOI":"10.1137\/0216062"},{"key":"1632_CR21","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli, \u201cA temporal logic of concurrent programs,\u201d Theoretical Computer Science, Vol. 13, pp. 45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"1632_CR22","doi-asserted-by":"crossref","unstructured":"O. Sokolsky and S. Smolka, \u201cLocal model checking for real-time systems,\u201d in CAV\u201995. LNCS 939, 1995.","DOI":"10.1007\/3-540-60045-0_52"},{"key":"1632_CR23","unstructured":"K.S. Stevens, S.V. Robinson, and A.L. Davis, \u201cThe post office\u2014communication support for distributed ensemble architectures,\u201d in Sixth International Conference on Distributed Computing Systems, 1986."},{"issue":"2","key":"1632_CR24","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"R. Tarjan, \u201cDepth first search and linear graph algorithms,\u201d SIAM Journal on Computing, Vol. 1, No. 2, pp. 146\u2013170, 1972.","journal-title":"SIAM Journal on Computing"},{"key":"1632_CR25","unstructured":"S. Tripakis, \u201cThe formal analysis of timed systems in practice,\u201d PhD thesis, Universit\u00e9 Joseph Fourrier de Grenoble, 1998."},{"key":"1632_CR26","doi-asserted-by":"crossref","unstructured":"S. Tripakis, \u201cVerifying progress in timed systems,\u201d in 5th Intl. AMAST Workshop on Real-Time and Probabilistic Systems (ARTS), LNCS 1601, 1999.","DOI":"10.1007\/3-540-48778-6_18"},{"key":"1632_CR27","doi-asserted-by":"crossref","unstructured":"S. Tripakis, \u201cDescription and schedulability analysis of the software architecture of an automated vehicle control system,\u201d in EMSOFT\u201902, 2002. To appear in LNCS.","DOI":"10.1007\/3-540-45828-X_10"},{"issue":"1","key":"1632_CR28","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S. Tripakis","year":"2001","unstructured":"S. Tripakis and S. Yovine, \u201cAnalysis of timed systems using time-abstracting bisimulations,\u201d Formal Methods in System Design, Vol. 18, No. 1, pp. 25\u201368, 2001.","journal-title":"Formal Methods in System Design"},{"key":"1632_CR29","doi-asserted-by":"crossref","unstructured":"S. Tripakis and S. Yovine, \u201cTiming analysis and code generation of vehicle control software using Taxys,\u201d in Workshop on Runtime Verification (RV\u201901). Volume 55, Issue 2 of ENTCS, Elsevier, 2001.","DOI":"10.1016\/S1571-0661(04)00257-9"},{"key":"1632_CR30","doi-asserted-by":"crossref","unstructured":"S. Yovine, \u201cKRONOS: A verification tool for real-time systems,\u201d Software Tools for Technology Transfer, 1997.","DOI":"10.1007\/s100090050009"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1632-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-1632-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1632-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T09:41:52Z","timestamp":1683193312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-1632-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["1632"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-1632-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}