{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T00:47:39Z","timestamp":1768438059654,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642333644","type":"print"},{"value":"9783642333651","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33365-1_16","type":"book-chapter","created":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T18:27:28Z","timestamp":1346524048000},"page":"220-235","source":"Crossref","is-referenced-by-count":2,"title":["Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics"],"prefix":"10.1007","author":[{"given":"Jonas","family":"Rinast","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sibylle","family":"Schupp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"16_CR1","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M. Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems\u00a016(5), 1543\u20131571 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bornot, S., Sifakis, J.: Relating time progress and deadlines in hybrid systems. In: Proc. of the Int. Work. on Hybrid and Real-Time Systems, pp. 286\u2013300 (1997)","DOI":"10.1007\/BFb0014733"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-64358-3_31","volume-title":"Hybrid Systems: Computation and Control","author":"S. Bornot","year":"1998","unstructured":"Bornot, S., Sifakis, J.: On the Composition of Hybrid Systems. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.\u00a01386, pp. 49\u201363. Springer, Heidelberg (1998)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: Int. Symp.: Compositionality - The Significant Difference, pp. 103\u2013129 (1997)","DOI":"10.1007\/3-540-49213-5_5"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Bowman, H.: Time and action lock freedom properties of timed automata. In: Formal Techniques for Networked and Distributed Systems, pp. 119\u2013134 (2001)","DOI":"10.1007\/0-306-47003-9_8"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/s001650050032","volume":"10","author":"H. Bowman","year":"1998","unstructured":"Bowman, H., Faconti, G., Katoen, J.-P., Latella, D., Massink, M.: Automatic verification of a lip-synchronisation protocol using UPPAAL. Formal Aspects of Computing\u00a010, 550\u2013575 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s00165-006-0010-7","volume":"18","author":"H. Bowman","year":"2006","unstructured":"Bowman, H., G\u00f3mez, R.: How to stop time stopping. Formal Aspects of Computing\u00a018, 459\u2013493 (2006)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 313\u2013329. Springer, Heidelberg (1998)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Gebremichael, B., Vaandrager, F.: Specifying urgency in timed I\/O automata. In: Proc. of the 3rd IEEE Int. Conf. on Software Engineering and Formal Methods, pp. 64\u201373 (2005)","DOI":"10.1109\/SEFM.2005.42"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Gebremichael, B., Vaandrager, F., Zhang, M.: Analysis of the zeroconf protocol using UPPAAL. In: Proc. of the 6th ACM & IEEE Int. Conf. on Embedded Software, pp. 242\u2013251 (2006)","DOI":"10.1145\/1176887.1176923"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-39979-7_12","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"R. G\u00f3mez","year":"2003","unstructured":"G\u00f3mez, R., Bowman, H.: Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream. In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol.\u00a02767, pp. 177\u2013192. Springer, Heidelberg (2003)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-75454-1_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"R. G\u00f3mez","year":"2007","unstructured":"G\u00f3mez, R., Bowman, H.: Efficient Detection of Zeno Runs in Timed Automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 195\u2013210. Springer, Heidelberg (2007)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio\/video protocol: an industrial case study using UPPAAL. In: Proc. of the 18th IEEE Real-Time Systems Symp., pp. 2\u201313 (1997)","DOI":"10.7146\/brics.v4i31.18957"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS: Logic in Computer Science. pp. 278\u2013292. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-14295-6_15","volume-title":"Computer Aided Verification","author":"F. Herbreteau","year":"2010","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient Emptiness Check for Timed B\u00fcchi Automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 148\u2013161. Springer, Heidelberg (2010)"},{"issue":"1","key":"16_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2200\/S00310ED1V01Y201011DCT005","volume":"1","author":"D.K. Kaynar","year":"2010","unstructured":"Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The theory of timed I\/O automata, 2nd ed. Synthesis Lectures on Dist. Comp. Theory\u00a01(1), 1\u2013137 (2010)","journal-title":"Synthesis Lectures on Dist. Comp. Theory"},{"issue":"1","key":"16_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst.\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Trans. Comput. Syst."},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BFb0054178","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Lindahl","year":"1998","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gear Controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 281\u2013297. Springer, Heidelberg (1998)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"L\u00f6nn, H., Pettersson, P.: Formal verification of a TDMA protocol start-up mechanism. In: Proc. of the 1997 Pacific Rim Int. Symp. on Fault-Tolerant Systems, pp. 235\u2013242 (1997)","DOI":"10.1109\/PRFTS.1997.640153"},{"key":"16_CR22","unstructured":"Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Ph.D. thesis, Cambridge, MA, USA (1974)"},{"key":"16_CR23","unstructured":"Rinast, J.: ZenoTool, A Zeno Run detection tool for UPPAAL, http:\/\/www.sts.tu-harburg.de\/research\/zenotool.html"},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/BF01931370","volume":"16","author":"J.L. Szwarcfiter","year":"1976","unstructured":"Szwarcfiter, J.L., Lauer, P.E.: A search strategy for the elementary cycles of a directed graph. BIT Numerical Mathematics\u00a016, 192\u2013204 (1976)","journal-title":"BIT Numerical Mathematics"},{"key":"16_CR25","unstructured":"Tarjan, R.E.: Enumeration of the elementary circuits of a directed graph. Tech. rep., Department of Computer Science, Cornell University, Ithaca, NY, USA (1972)"},{"key":"16_CR26","doi-asserted-by":"publisher","first-page":"722","DOI":"10.1145\/362814.362819","volume":"13","author":"J.C. Tiernan","year":"1970","unstructured":"Tiernan, J.C.: An efficient search algorithm to find the elementary circuits of a graph. Commun. ACM\u00a013, 722\u2013726 (1970)","journal-title":"Commun. ACM"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying Progress in Timed Systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 299\u2013314. Springer, Heidelberg (1999)"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s10703-005-1632-8","volume":"26","author":"S. Tripakis","year":"2005","unstructured":"Tripakis, S., Yovine, S., Bouajjani, A.: Checking Timed B\u00fcchi Automata Emptiness Efficiently. Formal Methods in System Design\u00a026, 267\u2013292 (2005)","journal-title":"Formal Methods in System Design"},{"key":"16_CR29","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s00165-006-0008-1","volume":"18","author":"F. Vaandrager","year":"2006","unstructured":"Vaandrager, F., de Groot, A.: Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Aspects of Computing\u00a018, 433\u2013458 (2006)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR30","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT)\u00a01, 123\u2013133 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33365-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T17:22:57Z","timestamp":1744046577000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33365-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642333644","9783642333651"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33365-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}