{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T04:10:08Z","timestamp":1739851808320,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540424949"},{"type":"electronic","value":"9783540446798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44679-6_59","type":"book-chapter","created":{"date-parts":[[2010,2,9]],"date-time":"2010-02-09T17:00:37Z","timestamp":1265734837000},"page":"529-539","source":"Crossref","is-referenced-by-count":3,"title":["Decidable Approximations on Generalized and Parameterized Discrete Timed Automata"],"prefix":"10.1007","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":"297","published-online":{"date-parts":[[2001,7,31]]},"reference":[{"key":"59_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"CAV\u201999","author":"R. Alur","year":"1999","unstructured":"R. Alur, \u201cTimed automata\u201d, CAV\u201999, LNCS 1633, pp. 8\u201322"},{"key":"59_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis and D. Dill, \u201cModel-checking in dense real time,\u201d Information and Computation, 104 (1993) 2\u201334","journal-title":"Information and Computation"},{"key":"59_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill, \u201cA theory of timed automata,\u201d TCS, 126 (1994) 183\u2013236","journal-title":"TCS"},{"key":"59_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur, T.A. Henzinger, \u201cA really temporal logic,\u201d J. ACM, 41 (1994) 181\u2013204","journal-title":"J. ACM"},{"key":"59_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger and M.Y. Vardi, \u201cParametric real-time reasoning,\u201d STOC\u201993, pp. 592\u2013601","DOI":"10.1145\/167088.167242"},{"key":"59_CR6","first-page":"572","volume":"23","author":"A. Coen-Porisini","year":"1997","unstructured":"A. Coen-Porisini, C. Ghezzi and R.A. Kemmerer, \u201cSpecification of real-time systems using ASTRAL,\u201d TSE, 23 (1997) 572\u2013598","journal-title":"TSE"},{"key":"59_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/3-540-48320-9_18","volume-title":"CONCUR\u201999","author":"H. Comon","year":"1999","unstructured":"H. Comon and Y. Jurski, \u201cTimed automata and the theory of real numbers,\u201d CONCUR\u201999, LNCS 1664, pp. 242\u2013257"},{"key":"59_CR8","first-page":"548","volume":"20","author":"A. Coen-Porisini","year":"1994","unstructured":"A. Coen-Porisini, R.A. Kemmerer and D. Mandrioli, \u201cA formal framework for ASTRAL intralevel proof obligations,\u201d TSE, 20 (1994) 548\u2013561","journal-title":"TSE"},{"key":"59_CR9","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"Z. Dang","year":"2001","unstructured":"Z. Dang, \u201cA decidable binary reachability characterization of timed pushdown automata with dense clocks,\u201d To appear in CAV\u201901, LNCS"},{"key":"59_CR10","doi-asserted-by":"crossref","unstructured":"Z. Dang and R.A. Kemmerer, \u201cUsing the ASTRAL model checker to analyze Mobile IP,\u201d ICSE\u201999, pp. 132\u2013141","DOI":"10.1145\/302405.302459"},{"key":"59_CR11","doi-asserted-by":"crossref","unstructured":"Z. Dang and R.A. Kemmerer, \u201cA symbolic model checker for testing ASTRAL real-time specifications,\u201d RTCSA\u201999, pp. 174\u2013181","DOI":"10.1109\/RTCSA.1999.811215"},{"key":"59_CR12","unstructured":"Z. Dang and R.A. Kemmerer, \u201cUsing the ASTRAL symbolic model checker as a specification debugger: three approximation techniques,\u201d ICSE\u201900, pp. 345\u2013354"},{"key":"59_CR13","unstructured":"Z. Dang, O.H. Ibarra and R.A. Kemmerer, http:\/\/www.eecs.wsu.edu\/~zdang , the full version of this paper"},{"key":"59_CR14","series-title":"Lect Notes Comput Sci","first-page":"132","volume-title":"STACS\u201901","author":"Z. Dang","year":"2001","unstructured":"Z. Dang, P. San Pietro and R.A. Kemmerer, \u201cOn Presburger liveness of discrete timed automata,\u201d STACS\u201901, LNCS 2010, pp. 132\u2013143"},{"key":"59_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/10722167_9","volume-title":"CAV\u201900","author":"Z. Dang","year":"2000","unstructured":"Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer and J. Su, \u201cBinary reachability analysis of discrete pushdown timed automata,\u201d CAV\u201900, LNCS 1855, pp. 69\u201384"},{"key":"59_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"T.A. Henzinger and Pei-Hsin Ho, \u201cHyTech: the Cornell hybrid technology tool,\u201d Hybrid Systems II, LNCS 999, 1995, pp. 265\u2013294"},{"key":"59_CR17","doi-asserted-by":"publisher","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, 111 (1994) 193\u2013244","journal-title":"Information and Computation"},{"key":"59_CR18","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer and N. Lynch, \u201cThe generalized railroad crossing: a case study in formal verification of real-time systems,\u201d RTSS\u201994, pp. 120\u2013131","DOI":"10.1109\/REAL.1994.342724"},{"key":"59_CR19","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O.H. Ibarra","year":"1978","unstructured":"O.H. Ibarra, \u201cReversal-bounded multicounter machines and their decision problems,\u201d J. ACM, 25 (1978) 116\u2013133","journal-title":"J. ACM"},{"key":"59_CR20","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1137\/S0097539792240625","volume":"24","author":"O.H. Ibarra","year":"1995","unstructured":"O.H. Ibarra, T. Jiang, N. Tran and H. Wang, \u201cNew decidability results concerning two-way counter machines,\u201d SIAM J. Comput., 24 (1995) 123\u2013137","journal-title":"SIAM J. Comput."},{"key":"59_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-44612-5_38","volume-title":"MFCS\u201900","author":"O.H. Ibarra","year":"2000","unstructured":"O.H. Ibarra, J. Su, Z. Dang, T. Bultan and R.A. Kemmerer, \u201cCounter machines: decidable properties and applications to verification problems,\u201d, MFCS\u201900, LNCS 1893, pp. 426\u2013435"},{"key":"59_CR22","unstructured":"P. Kolano, \u201cTools and techniques for the design and systematic analysis of real-Time systems,\u201d Ph.D. Thesis, University of California, Santa Barbara, 1999"},{"key":"59_CR23","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1018934104631","volume":"7","author":"P.Z. Kolano","year":"1999","unstructured":"P.Z. Kolano, Z. Dang and R.A. Kemmerer, \u201cThe design and analysis of realtime systems using the ASTRAL software development environment,\u201d Annals of Software Engineering, 7 (1999) 177\u2013210","journal-title":"Annals of Software Engineering"},{"key":"59_CR24","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"K.G. Larsen, P. Pattersson and W. Yi, \u201cUPPAAL in a nutshell,\u201d International Journal on Software Tools for Technology Transfer, 1 (1997) 134\u2013152","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"59_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/3-540-60246-1_158","volume-title":"MFCS\u201995","author":"F. Laroussinie","year":"1995","unstructured":"F. Laroussinie, K.G. Larsen and C. Weise, \u201cFrom timed automata to logic-and back,\u201d MFCS\u201995, LNCS 969, pp. 529\u2013539"},{"key":"59_CR26","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"W. Pugh, \u201cThe Omega test: a fast and practical integer programming algorithm for dependence analysis,\u201d CACM, 8 (1992) 102\u2013104","journal-title":"CACM"},{"key":"59_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0014711","volume-title":"HART\u201997","author":"J. Raskin","year":"1997","unstructured":"J. Raskin and P. Schobben, \u201cState clock logic: a decidable real-time logic,\u201d HART\u201997, LNCS 1201, pp. 33\u201347"},{"key":"59_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-58468-4_191","volume-title":"\u201cSpecifying timed state sequences in powerful decidable logics and timed automata","author":"T. Wilke","year":"1994","unstructured":"T. Wilke, \u201cSpecifying timed state sequences in powerful decidable logics and timed automata,\u201d LNCS 863, pp. 694\u2013715, 1994"},{"key":"59_CR29","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"S. Yovine, \u201cA verification tool for real-time systems,\u201d International Journal on Software Tools for Technology Transfer, 1 (1997): 123\u2013133","journal-title":"International Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44679-6_59","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T03:34:11Z","timestamp":1739849651000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44679-6_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424949","9783540446798"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-44679-6_59","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}