{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:19Z","timestamp":1760202559242},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404934"},{"type":"electronic","value":"9783540450610"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45061-0_53","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:54:04Z","timestamp":1184601244000},"page":"668-680","source":"Crossref","is-referenced-by-count":11,"title":["A Solvable Class of Quadratic Diophantine Equations with Applications to Verification of Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Gaoyan","family":"Xie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhe","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oscar H.","family":"Ibarra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"53_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. Timed automata. In CAV\u201999, volume 1633 of LNCS, pages 8\u201322. Springer, 1999."},{"issue":"2","key":"53_CR2","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. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013235, April 1994.","journal-title":"Theoretical Computer Science"},{"key":"53_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: application to model-checking. In CONCUR\u201997, volume 1243 of LNCS, pages 135\u2013150. Springer, 1997."},{"issue":"4","key":"53_CR4","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747\u2013789, July 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"53_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"53_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027094","volume-title":"CAV\u201998","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Pres-burger arithmetic. In CAV\u201998, volume 1427 of LNCS, pages 268-279. Springer, 1998."},{"key":"53_CR7","unstructured":"Z. Dang. Verifying and debugging real-time infinite state systems (PhD. Dissertation). Department of Computer Science, University of California at Santa Barbara, 2000."},{"key":"53_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36159-6","volume-title":"ISAAC\u201902","author":"Z. Dang","year":"2002","unstructured":"Z. Dang, O. Ibarra, and Z. Sun. On the emptiness problems for two-way nondeterministic finite automata with one reversal-bounded counter. In ISAAC\u201902, volume 2518 of LNCS, pages 103-114. Springer, 2002."},{"key":"53_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1007\/3-540-44585-4_48","volume-title":"CAV\u201901","author":"Z. Dang","year":"2001","unstructured":"Zhe Dang. Binary reachability analysis of pushdown timed automata with dense clocks. In CAV\u201901, volume 2102 of LNCS, pages 506\u2013517. Springer, 2001."},{"issue":"5","key":"53_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997. Special Issue: Formal Methods in Software Practice.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"53_CR11","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. H. Ibarra","year":"1978","unstructured":"O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25(1):116\u2013133, January 1978.","journal-title":"Journal of the ACM"},{"key":"53_CR12","doi-asserted-by":"crossref","unstructured":"O. H. Ibarra and Z. Dang. Deterministic two-way finite automata augmented with monotonic counters. 2002 (submitted).","DOI":"10.1007\/3-540-45005-X_29"},{"key":"53_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"53_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/10722167_7","volume-title":"CAV\u201900","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman and M.Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In CAV\u201900, volume 1855 of LNCS, pages 36\u201352. Springer, 2000."},{"key":"53_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"CAV\u201901","author":"K. Larsen","year":"2001","unstructured":"K. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson, and J. Romijn. As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In CAV\u201901, volume 2102 of LNCS, pages 493\u2013505. Springer, 2001."},{"key":"53_CR16","unstructured":"Y. V. Matiyasevich. Hilbert\u2019s Tenth Problem. MIT Press, 1993."},{"key":"53_CR17","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M. Minsky","year":"1961","unstructured":"M. Minsky. Recursive unsolvability of Post\u2019s problem of Tag and other topics in the theory of Turing machines. Ann. of Math., 74:437\u2013455, 1961.","journal-title":"Ann. of Math."},{"key":"53_CR18","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R. Parikh","year":"1966","unstructured":"R. Parikh. On context-free languages. Journal of the ACM, 13:570\u2013581, 1966.","journal-title":"Journal of the ACM"},{"key":"53_CR19","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS\u201986, pages 332\u2013344. IEEE Computer Society Press, 1986."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45061-0_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T03:12:58Z","timestamp":1556680378000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45061-0_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404934","9783540450610"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45061-0_53","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}