{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,11]],"date-time":"2024-12-11T19:43:05Z","timestamp":1733946185085,"version":"3.30.2"},"reference-count":28,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3791,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1016\/s0304-3975(02)00432-2","type":"journal-article","created":{"date-parts":[[2003,2,12]],"date-time":"2003-02-12T17:35:20Z","timestamp":1045071320000},"page":"59-74","source":"Crossref","is-referenced-by-count":6,"title":["Generalized discrete timed automata: decidable approximations for safety verification"],"prefix":"10.1016","volume":"296","author":[{"given":"Zhe","family":"Dang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oscar H.","family":"Ibarra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard A.","family":"Kemmerer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(02)00432-2_BIB1","unstructured":"R. Alur, Timed automata, CAV\u201999, Lecture Notes in Computer Science, vol. 1633, Springer, Berlin, pp. 8\u201322."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model-checking in dense real time","volume":"104","author":"Alur","year":"1993","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","article-title":"A really temporal logic","volume":"41","author":"Alur","year":"1994","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB5","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, M.Y. Vardi, Parametric real-time reasoning, STOC\u201993, ACM Press, New York, pp. 592\u2013601.","DOI":"10.1145\/167088.167242"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB6","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1109\/32.629494","article-title":"Specification of real-time systems using ASTRAL","volume":"23","author":"Coen-Porisini","year":"1997","journal-title":"IEEE Tran. Soft. Eng."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB7","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1109\/32.310665","article-title":"A formal framework for ASTRAL intralevel proof obligations","volume":"20","author":"Coen-Porisini","year":"1994","journal-title":"IEEE Tran. Soft. Eng."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB8","unstructured":"H. Comon, Y. Jurski, Timed automata and the theory of real numbers, CONCUR\u201999, Lecture Notes in Computer Science, vol. 1664, Springer, Berlin, pp. 242\u2013257."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB9","unstructured":"Z. Dang, Binary reachability analysis of timed pushdown automata with dense clocks, CAV\u201901, Lecture Notes in Computer Science, vol. 2102, Springer, Berlin, pp. 506\u2013517."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB10","unstructured":"Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer, J. Su, Binary reachability analysis of discrete pushdown timed automata, CAV\u201900, Lecture Notes in Computer Science, vol. 1855, Springer, Berlin, pp. 69\u201384."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB11","doi-asserted-by":"crossref","unstructured":"Z. Dang, R.A. Kemmerer, Using the ASTRAL model checker to analyze Mobile IP, ICSE\u201999, ACM Press, New York, pp. 132\u2013141.","DOI":"10.1145\/302405.302459"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB12","doi-asserted-by":"crossref","unstructured":"Z. Dang, R.A. Kemmerer, A symbolic model checker for testing ASTRAL real-time specifications, RTCSA\u201999, IEEE Computer Society, Los Alamitos, pp. 174\u2013181.","DOI":"10.1109\/RTCSA.1999.811215"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB13","unstructured":"Z. Dang, R.A. Kemmerer, Using the ASTRAL symbolic model checker as a specification debugger: three approximation techniques, ICSE\u201900, ACM Press, New York, pp. 345\u2013354."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB14","unstructured":"Z. Dang, P. San Pietro, R.A. Kemmerer, On Presburger liveness of discrete timed automata, STACS\u201901, Lecture Notes in Computer Science, vol. 2010, Springer, Berlin, pp. 132\u2013143."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB15","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer, N. Lynch, The generalized railroad crossing: a case study in formal verification of real-time systems, RTSS\u201994, pp. 120\u2013131.","DOI":"10.1109\/REAL.1994.342724"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB16","first-page":"265","volume":"vol. 999","author":"Henzinger","year":"1995"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB17","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB18","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/322047.322058","article-title":"Reversal-bounded multicounter machines and their decision problems","volume":"25","author":"Ibarra","year":"1978","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB19","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1137\/S0097539792240625","article-title":"New decidability results concerning two-way counter machines","volume":"24","author":"Ibarra","year":"1995","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB20","unstructured":"O.H. Ibarra, J. Su, Z. Dang, T. Bultan, R.A. Kemmerer, Counter machines: decidable properties and applications to verification problems, MFCS\u201900, Lecture Notes in Computer Science, vol. 1893, Springer, Berlin, pp. 426\u2013435."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB21","unstructured":"P. Kolano, Tools and techniques for the design and systematic analysis of real-time systems, Ph.D. Thesis, University of California, Santa Barbara, 1999."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB22","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1018934104631","article-title":"The design and analysis of real-time systems using the ASTRAL software development environment","volume":"7","author":"Kolano","year":"1999","journal-title":"Ann. Software Eng."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB23","doi-asserted-by":"crossref","unstructured":"F. Laroussinie, K.G. Larsen, C. Weise, From timed automata to logic\u2014and back, MFCS\u201995, Lecture Notes in Computer Science, vol. 969, Springer, Berlin, pp. 529\u2013539.","DOI":"10.1007\/3-540-60246-1_158"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB24","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":"Internat. J. Software Tools Tech. Transfer"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB25","first-page":"102","article-title":"The Omega test","volume":"8","author":"Pugh","year":"1992","journal-title":"Comm. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB26","unstructured":"J. Raskin, P. Schobben, State clock logic: a decidable real-time logic, HART\u201997, Lecture Notes in Computer Science, vol. 1201, Springer, Berlin, pp. 33\u201347."},{"key":"10.1016\/S0304-3975(02)00432-2_BIB27","first-page":"694","volume":"vol. 863","author":"Wilke","year":"1994"},{"key":"10.1016\/S0304-3975(02)00432-2_BIB28","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","article-title":"A verification tool for real-time systems","volume":"1","author":"Yovine","year":"1997","journal-title":"Internat. J. Software Tools Tech. Transfer"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502004322?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502004322?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,11]],"date-time":"2024-12-11T18:31:01Z","timestamp":1733941861000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397502004322"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S0304397502004322"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(02)00432-2","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}