{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:00Z","timestamp":1760202540753},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429852"},{"type":"electronic","value":"9783540456780"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45678-3_22","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T16:12:14Z","timestamp":1195143134000},"page":"244-256","source":"Crossref","is-referenced-by-count":3,"title":["On Removing the Pushdown Stack in Reachability Constructions"],"prefix":"10.1007","author":[{"given":"Oscar H.","family":"Ibarra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhe","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,12,4]]},"reference":[{"issue":"2","key":"22_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. Dill. \u201cThe theory of timed automata,\u201d TCS, 126(2):183\u2013236, 1994","journal-title":"TCS"},{"issue":"2","key":"22_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P. Abdulla","year":"1996","unstructured":"P. Abdulla and B. Jonsson. \u201cVerifying programs with unreliable channels,\u201d Information and Computation, 127(2): 91\u2013101, 1996","journal-title":"Information and Computation"},{"key":"22_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. \u201cReachability analysis of pushdown automata: application to model-Checking,\u201d CONCUR\u201997, LNCS 1243, pp. 135\u2013150"},{"key":"22_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/3-540-63166-6_31","volume-title":"CAV\u201997","author":"G. Cece","year":"1997","unstructured":"G. Cece and A. Finkel. \u201cPrograms with Quasi-Stable Channels are Effectively Recognizable,\u201d CAV\u201997, LNCS 1254, pp. 304\u2013315 244"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"H. Comon and V. Cortier. \u201cFlatness is not a weakness,\u201d Proc. Computer Science Logic, 2000","DOI":"10.1007\/3-540-44622-2_17"},{"key":"22_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"CAV\u201998","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. \u201cMultiple counters automata, safety analysis and Presburger arithmetic,\u201d CAV\u201998, LNCS 1427, pp. 268\u2013279"},{"key":"22_CR7","series-title":"Lect Notes Comput Sci","first-page":"242","volume-title":"CONCUR\u201999","author":"H. Comon","year":"1664","unstructured":"H. Comon and Y. Jurski. \u201cTimed automata and the theory of real numbers,\u201d CONCUR\u201999, LNCS 1664, pp. 242\u2013257"},{"key":"22_CR8","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":"Z. Dang. \u201cBinary reachability analysis of timed pushdown automata with dense clocks,\u201d CAV\u201901, LNCS 2102, pp. 506\u2013517"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Z. Dang and O. H. Ibarra. \u201cLiveness verification of reversal-bounded counter machines with a free counter,\u201d submitted, 2001","DOI":"10.1007\/3-540-45294-X_12"},{"key":"22_CR10","series-title":"Lect Notes Comput Sci","first-page":"69","volume-title":"CAV\u201900","author":"Z. Dang","year":"1855","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":"22_CR11","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":"22_CR12","series-title":"Lect Notes Comput Sci","first-page":"232","volume-title":"CAV\u201900","author":"J. Esparza","year":"1855","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. \u201cEffcient Algorithms for Model Checking Pushdown Systems,\u201d CAV\u201900, LNCS 1855, pp. 232\u2013247"},{"key":"22_CR13","series-title":"Lect Notes Comput Sci","first-page":"346","volume-title":"STACS\u201900","author":"A. Finkel","year":"1997","unstructured":"A. Finkel and G. Sutre. \u201cDecidability of Reachability Problems for Classes of Two Counter Automata,\u201d STACS\u201900, LNCS 1770, pp. 346\u2013357 244"},{"key":"22_CR14","unstructured":"A. Finkel, B. Willems, and P. Wolper. \u201cA direct symbolic approach to model checking pushdown systems,\u201d INFINITY\u201997"},{"key":"22_CR15","first-page":"333","volume":"113","author":"S. Ginsburg","year":"1964","unstructured":"S. Ginsburg and E. Spanier. \u201cBounded Algol-like languages,\u201d Transactions of American Mathematical Society, 113, pp. 333\u2013368, 1964.","journal-title":"Transactions of American Mathematical Society"},{"key":"22_CR16","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":"22_CR17","unstructured":"O. H. Ibarra. \u201cReachability and safety in queue systems with counters and pushdown stack,\u201d Proceedings of the International Conference on Implementation and Application of Automata, pp. 120\u2013129, 2000."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"O. H. Ibarra, T. Bultan, and J. Su. \u201cReachability analysis for some models of infinite-state transition systems,\u201d CONCUR\u201900, pp. 183\u2013198, 2000.","DOI":"10.1007\/3-540-44618-4_15"},{"key":"22_CR19","unstructured":"O. H. Ibarra. \u201cReachability and safety in queue systems with counters and pushdown stack,\u201d Proceedings of the International Conference on Implementation and Application of Automata, pp. 120\u2013129, 2000"},{"key":"22_CR20","unstructured":"O. H. Ibarra, Z. Dang, and P. San Pietro, \u201cVerification in Loosely Synchronous Queue-Connected Discrete Timed Automata,\u201d submitted. 2001"},{"key":"22_CR21","unstructured":"O. H. Ibarra and J. Su. \u201cGeneralizing the discrete timed automaton,\u201d Proceedings of the International Conference on Implementation and Application of Automata, 206\u2013215, 2000."},{"key":"22_CR22","series-title":"Lect Notes Comput Sci","first-page":"426","volume-title":"MFCS\u201900","author":"O. H. Ibarra","year":"1893","unstructured":"O. H. Ibarra, J. Su, T. Bultan, Z. Dang, and R. A. Kemmerer. \u201cCounter Machines: Decidable Properties and Applications to Verification Problems,\u201d, MFCS\u201900, LNCS 1893, pp. 426\u2013435"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. \u201cSymbolic model-checking \u2014 an approach to the state explosion problem,\u201d PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992","DOI":"10.1007\/978-1-4615-3190-6_3"},{"issue":"6\/7","key":"22_CR24","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/BF01185558","volume":"29","author":"W. Peng","year":"1992","unstructured":"W. Peng and S. Purushothaman. \u201cAnalysis of a Class of Communicating Finite State Machines,\u201d Acta Informatica, 29(6\/7): 499\u2013522, 1992","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45678-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T13:18:27Z","timestamp":1556975907000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45678-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429852","9783540456780"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45678-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}