{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:59:15Z","timestamp":1740131955937,"version":"3.37.3"},"reference-count":37,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation Program","doi-asserted-by":"publisher","award":["61103032"],"award-info":[{"award-number":["61103032"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Key Technology Support Program","award":["2014BAH24F02"],"award-info":[{"award-number":["2014BAH24F02"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2015,1,1]]},"DOI":"10.1109\/tse.2014.2359893","type":"journal-article","created":{"date-parts":[[2014,9,23]],"date-time":"2014-09-23T19:05:15Z","timestamp":1411499115000},"page":"3-18","source":"Crossref","is-referenced-by-count":7,"title":["A Systematic Study on Explicit-State Non-Zenoness Checking for Timed Automata"],"prefix":"10.1109","volume":"41","author":[{"given":"Ting","family":"Wang","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Xinyu","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Yuanjie","family":"Si","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Xiaohu","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Xiaohong","family":"Li","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_9"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967734"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-011-9122-0"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00334-1"},{"key":"ref36","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/3-540-61042-1_53","article-title":"Extending promela and spin for real time","volume":"1055","author":"tripakis","year":"0","journal-title":"Proc 2nd Int Workshop Tools Algorithms Construction Anal Systems"},{"key":"ref35","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-540-75454-1_15","article-title":"Efficient detection of zeno runs in timed automata","volume":"4763","author":"g\u00f3mez","year":"0","journal-title":"Proc 5th Int Conf Formal Model Anal Timed Syst"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0010-7"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15643-4_29"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.52"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0133-1"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48778-6_18"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1632-8"},{"key":"ref15","first-page":"218","article-title":"Efficient on-the-fly emptiness check for timed Büchi automata","author":"herbreteau","year":"0","journal-title":"Proc 8th Int Conf Automated Technol Verification Anal"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430537"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80369-X"},{"key":"ref18","first-page":"709","article-title":"Pat: Towards flexible verification under fairness","volume":"5643","author":"sun","year":"0","journal-title":"Proc 21st Int Conf Comput Aided Verification"},{"key":"ref19","first-page":"223","article-title":"Automatic verification of real-time communicating systems by constraint-solving","author":"yi","year":"0","journal-title":"Proc 7th Int Conf Formal Description Techn"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.71"},{"key":"ref4","first-page":"546","article-title":"Kronos: A model-checking tool for real-time systems","volume":"1427","author":"bozga","year":"0","journal-title":"Proc 23rd Int Conf Comput Aided Verification"},{"key":"ref27","first-page":"189","article-title":"Efficient verification of timed automata with BDD-like data-structures","author":"wang","year":"0","journal-title":"Proc Int Conf Verification Model Checking Abstract Interpretation"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"larsen","year":"1997","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref6","first-page":"122","article-title":"Rabbit: A tool for BDD-based verification of real-time systems","author":"beyer","year":"0","journal-title":"Proc 15th Int Conf Comput Aided Verification"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.53"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/0-306-47003-9_15"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00173-4"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0064-y"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319600"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref20","first-page":"417","article-title":"The expressive power of clocks","author":"henzinger","year":"0","journal-title":"Proc 22nd Int Colloq Automata Languages Program"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","article-title":"Efficient timed reachability analysis using clock difference diagrams","volume":"1633","author":"behrmann","year":"0","journal-title":"Proc 11th Int Conf Comput Aided Verification"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","article-title":"Timing assumptions and verification of finite-state concurrent systems","volume":"407","author":"dill","year":"0","journal-title":"Automatic Verification Methods for Finite State Systems International Workshop"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000026093.21513.31"},{"article-title":"Representing and modeling digital circuits","year":"1993","author":"rokicki","key":"ref23"},{"key":"ref26","first-page":"174","article-title":"A note on on-the-fly verification algorithms","author":"schwoon","year":"0","journal-title":"Proc 11th Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507245"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/7004098\/06908008.pdf?arnumber=6908008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:04:26Z","timestamp":1642003466000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6908008\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,1]]},"references-count":37,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tse.2014.2359893","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"}],"subject":[],"published":{"date-parts":[[2015,1,1]]}}}