{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:46:26Z","timestamp":1725493586058},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405610"},{"type":"electronic","value":"9783540450894"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45089-0_16","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T03:27:35Z","timestamp":1193455655000},"page":"163-175","source":"Crossref","is-referenced-by-count":0,"title":["New Complexity Results for Some Linear Counting Problems Using Minimal Solutions to Linear Diophantine Equations"],"prefix":"10.1007","author":[{"given":"Gaoyan","family":"Xie","sequence":"first","affiliation":[]},{"given":"Cheng","family":"Li","sequence":"additional","affiliation":[]},{"given":"Zhe","family":"Dang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"issue":"2","key":"16_CR1","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"},{"issue":"1","key":"16_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur and T. A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181\u2013204, January 1994.","journal-title":"Journal of the ACM"},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"TACAS\u201999","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS\u201999, volume 1579 of LNCS, pages 193\u2013207. Springer-Verlag, 1999."},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/0012-365X(86)90138-X","volume":"58","author":"I. Borosh","year":"1986","unstructured":"I. Borosh, M. Flahive, and B. Treybig. Small solutions of linear diophantine equations. Discrete Mathematics, 58:215\u2013220, 1986.","journal-title":"Discrete Mathematics"},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"299","DOI":"10.2307\/2041711","volume":"55","author":"I. Borosh","year":"1976","unstructured":"I. Borosh and B. Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55:299\u2013304, 1976.","journal-title":"Proceedings of the American Mathematical Society"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In LICS\u201995, pages 123\u2013133. IEEE CS Press, 1995.","DOI":"10.1109\/LICS.1995.523250"},{"issue":"2","key":"16_CR7","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. TOPLAS, 8(2):244\u2013263, 1986.","journal-title":"TOPLAS"},{"key":"16_CR8","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. Timed automata and the theory of real numbers. In CONCUR\u201999, volume 1664 of LNCS, pages 242\u2013257. Springer, 1999."},{"key":"16_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."},{"key":"16_CR10","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":"Zhe Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. In CAV\u201900, volume 1855 of LNCS, pages 69\u201384. Springer, 2000."},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","first-page":"132","volume-title":"FSTTCS\u201901","author":"Z. Dang","year":"2001","unstructured":"Zhe Dang, O. H. Ibarra, and P. San Pietro. Liveness Verification of Reversal-bounded Multicounter Machines with a Free Counter. In FSTTCS\u201901, volume 2245 of LNCS, pages 132\u2013143. Springer, 2001."},{"key":"16_CR12","series-title":"Lect Notes Comput Sci","first-page":"132","volume-title":"STACS\u201901","author":"Z. Dang","year":"2001","unstructured":"Zhe Dang, P. San Pietro, and R. A. Kemmerer. On Presburger Liveness of Discrete Timed Automata. In STACS\u201901, volume 2010 of LNCS, pages 132\u2013143. Springer, 2001."},{"key":"16_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-54345-7_57","volume-title":"MFCS\u201991","author":"E. Domenjoud","year":"1991","unstructured":"E. Domenjoud. Solving systems of linear diophantine equations: an algebraic approach. In MFCS\u201991, volume 520 of LNCS, pages 141\u2013150. Springer-Verlag, 1991."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In ICSE\u201999, pages 411\u2013421. ACM Press, 1999.","DOI":"10.1145\/302405.302672"},{"issue":"5","key":"16_CR15","first-page":"279","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. TSE, 23(5):279\u2013295, May 1997.","journal-title":"TSE"},{"key":"16_CR16","unstructured":"J. Hopcroft and J. Ullman. Introduction to Automata theory, Languages, and Computation. Addison-Wesley Publishing Company, 1979."},{"key":"16_CR17","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."},{"issue":"4","key":"16_CR18","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541\u2013580, 1989.","journal-title":"Proceedings of the IEEE"},{"key":"16_CR19","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. JACM, 13:570\u2013581, 1966.","journal-title":"JACM"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In FOCS\u201977, pages 46\u201357. IEEE CS Press, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-53904-2_94","volume-title":"Rewriting Techniques and Applications","author":"L. Pottier","year":"1991","unstructured":"L. Pottier. Minimal solutions of linear diophantine equations: Bounds and algorithms. In Rewriting Techniques and Applications, volume 488 of LNCS, pages 162\u2013173. Springer-Verlag, 1991."},{"key":"16_CR22","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In LICS\u201986, pages 332\u2013344. IEEE CS Press, 1986."}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45089-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:08:05Z","timestamp":1556921285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45089-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405610","9783540450894"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45089-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}