{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:16Z","timestamp":1760202676405},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319097039"},{"type":"electronic","value":"9783319097046"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09704-6_2","type":"book-chapter","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T05:43:21Z","timestamp":1405057401000},"page":"5-22","source":"Crossref","is-referenced-by-count":6,"title":["Automata with Reversal-Bounded Counters: A Survey"],"prefix":"10.1007","author":[{"given":"Oscar H.","family":"Ibarra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. of STOC 2004, pp. 202\u2013211 (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Cerny, P.: Expressiveness of streaming string transducers. In: Proc. 30th Annual Conf. on Foundations of Software Technology and Theoretical Computer Science, pp. 1\u201312 (2010)","DOI":"10.1007\/978-3-642-20920-8_1"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-22012-8_1","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2011","unstructured":"Alur, R., Deshmukh, J.: Nondeterministic streaming string transducers. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 1\u201320. Springer, Heidelberg (2011)"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/S0022-0000(74)80027-9","volume":"8","author":"B. Baker","year":"1974","unstructured":"Baker, B., Book, R.: Reversal-bounded multipushdown machines. J. Comput. System Sci.\u00a08, 315\u2013332 (1974)","journal-title":"J. Comput. System Sci."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bouchy, F., Finkel, A., San Pietro, P.: Dense-choice counter machines revisited. In: Proc. of INFINITY 2009, pp. 3\u201322 (2009)","DOI":"10.4204\/EPTCS.10.1"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/j.entcs.2009.05.038","volume":"239","author":"F. Bouchy","year":"2009","unstructured":"Bouchy, F., Finkel, A., Sangnier, A.: Reachability in timed counter systems. Electr. Notes Theor. Comput. Sci.\u00a0239, 167\u2013178 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"4","key":"2_CR7","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1051\/ita\/2012013","volume":"46","author":"M. Cadilhac","year":"2012","unstructured":"Cadilhac, M., Finkel, A., McKenzie, P.: Affine Parikh automata. RAIRO - Theor. Inf. and Applic.\u00a046(4), 511\u2013545 (2012)","journal-title":"RAIRO - Theor. Inf. and Applic."},{"issue":"7","key":"2_CR8","doi-asserted-by":"publisher","first-page":"1099","DOI":"10.1142\/S0129054113400339","volume":"24","author":"M. Cadilhac","year":"2013","unstructured":"Cadilhac, M., Finkel, A., McKenzie, P.: Unambiguous constrained Automata. Int. J. Found. Comput. Sci.\u00a024(7), 1099\u20131116 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(86)90134-9","volume":"47","author":"K. Culik","year":"1986","unstructured":"Culik, K., Karhumaki, J.: The equivalence of finite valued transducers (on HDTOL languages) is decidable. Theoret. Comput. Sci.\u00a047, 71\u201384 (1986)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/3-540-44585-4_48","volume-title":"Computer Aided Verification","author":"Z. Dang","year":"2001","unstructured":"Dang, Z.: Binary reachability analysis of pushdown timed automata with dense clocks. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 506\u2013517. Springer, Heidelberg (2001)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-36390-4_7","volume-title":"Implementation and Application of Automata","author":"Z. Dang","year":"2003","unstructured":"Dang, Z., Bultan, T., Ibarra, O.H., Kemmerer, R.A.: Past pushdown timed automata. In: Watson, B.W., Wood, D. (eds.) CIAA 2001. LNCS, vol.\u00a02494, pp. 74\u201386. Springer, Heidelberg (2003)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/10722167_9","volume-title":"Computer Aided Verification","author":"Z. Dang","year":"2000","unstructured":"Dang, Z., Ibarra, O.H., Bultan, T., Kemmerer, R.A., Su, J.: Binary reachability analysis of discrete pushdown timed automata. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 69\u201384. Springer, Heidelberg (2000)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","first-page":"132","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"Z. Dang","year":"2001","unstructured":"Dang, Z., Ibarra, O.H., Miltersen, P.B.: Liveness verification of reversal-bounded multicounter machines with a free counter. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 132\u2013143. Springer, Heidelberg (2001)"},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.tcs.2004.09.010","volume":"330","author":"Z. Dang","year":"2005","unstructured":"Dang, Z., Ibarra, O.H., Sun, Z.-W.: On two-way nondeterministic finite automata with one reversal-bounded counter. Theor. Comput. Sci.\u00a0330(1), 59\u201379 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-85238-4_26","volume-title":"Mathematical Foundations of Computer Science 2008","author":"A. Finkel","year":"2008","unstructured":"Finkel, A., Sangnier, A.: Reversal-bounded counter machines revisited. In: Ochma\u0144ski, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol.\u00a05162, pp. 323\u2013334. Springer, Heidelberg (2008)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-15155-2_32","volume-title":"Mathematical Foundations of Computer Science 2010","author":"E. Filiot","year":"2010","unstructured":"Filiot, E., Raskin, J.-F., Reynier, P.-A., Servais, F., Talbot, J.-M.: Properties of visibly pushdown transducers. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 355\u2013367. Springer, Heidelberg (2010)"},{"issue":"3","key":"2_CR17","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/S0022-0000(68)80009-1","volume":"2","author":"S. Ginsburg","year":"1968","unstructured":"Ginsburg, S., Spanier, E.H.: Derivation-bounded languages. J. Comput. System Sci.\u00a02(3), 228\u2013250 (1968)","journal-title":"J. Comput. System Sci."},{"key":"2_CR18","first-page":"333","volume":"113","author":"S. Ginsburg","year":"1964","unstructured":"Ginsburg, S., Spanier, E.H.: Bounded ALGOL-like languages. T. Am. Math. Soc.\u00a0113, 333\u2013368 (1964)","journal-title":"T. Am. Math. Soc."},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1145\/321466.321473","volume":"15","author":"T. Griffiths","year":"1968","unstructured":"Griffiths, T.: The unsolvability of the equivalence problem for \u039b-free nondeterministic generalized sequential machines. J. Assoc. Comput. Mach.\u00a015, 409\u2013413 (1968)","journal-title":"J. Assoc. Comput. Mach."},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/0022-0000(81)90028-3","volume":"22","author":"E. Gurari","year":"1981","unstructured":"Gurari, E., Ibarra, O.H.: The complexity of decision problems for finite-turn multicounter machines. J. Comput. Syst. Sci.\u00a022, 220\u2013229 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR21","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1137\/0211035","volume":"11","author":"E. Gurari","year":"1982","unstructured":"Gurari, E.: The equivalence problem for deterministic two-way sequential transducers is decidable. SIAM J. Comput.\u00a011, 448\u2013452 (1982)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1145\/322326.322340","volume":"29","author":"E. Gurari","year":"1982","unstructured":"Gurari, E., Ibarra, O.H.: Two-way counter machines and Diophantine equations. J. ACM\u00a029(3), 863\u2013873 (1982)","journal-title":"J. ACM"},{"key":"2_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BF01744569","volume":"16","author":"E. Gurari","year":"1983","unstructured":"Gurari, E., Ibarra, O.H.: A note on finite-valued and finitely ambiguous transducers. Math. Systems Theory\u00a016, 61\u201366 (1983)","journal-title":"Math. Systems Theory"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"743","DOI":"10.1007\/978-3-642-22110-1_60","volume-title":"Computer Aided Verification","author":"M. Hague","year":"2011","unstructured":"Hague, M., Lin, A.W.: Model checking recursive programs with numeric data types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 743\u2013759. Springer, Heidelberg (2011)"},{"issue":"2","key":"2_CR25","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1006\/jcss.2002.1836","volume":"65","author":"T. Harju","year":"2002","unstructured":"Harju, T., Ibarra, O.H., Karhumaski, J., Salomaa, A.: Some decision problems concerning semilinearity and commutation. J. Comput. Syst. Sci.\u00a065(2), 278\u2013294 (2002)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR26","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata, Languages and Computation. Addison-Wesley (1978)"},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O.H. Ibarra","year":"1978","unstructured":"Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. of the ACM\u00a025(1), 116\u2013133 (1978)","journal-title":"J. of the ACM"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1137\/0207042","volume":"7","author":"O.H. Ibarra","year":"1978","unstructured":"Ibarra, O.H.: The unsolvability of the equivalence problem for \u03b5-free NGSM\u2019s with unary input (output) alphabet and applications. SIAM J. Computing\u00a07, 524\u2013532 (1978)","journal-title":"SIAM J. Computing"},{"key":"2_CR29","unstructured":"Ibarra, O.H.: On the ambiguity, finite-valuedness, and lossiness problems in acceptors and transducers. In: Proc. of CIAA 2014 (to appear, 2014)"},{"key":"2_CR30","unstructured":"Ibarra, O.H.: On decidability and closure properties of language classes with respect to bio-operations. In: Proc. of DNA 20 (to appear)"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-44618-4_15","volume-title":"CONCUR 2000 - Concurrency Theory","author":"O.H. Ibarra","year":"2000","unstructured":"Ibarra, O.H., Bultan, T., Su, J.: Reachability analysis for some models of infinite-state transition systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 183\u2013198. Springer, Heidelberg (2000)"},{"issue":"1-3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1016\/j.tcs.2005.12.001","volume":"352","author":"O.H. Ibarra","year":"2006","unstructured":"Ibarra, O.H., Dang, Z.: On the solvability of a class of diophantine equations and applications. Theor. Comput. Sci.\u00a0352(1-3), 342\u2013346 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-45138-9_42","volume-title":"Mathematical Foundations of Computer Science 2003","author":"O.H. Ibarra","year":"2003","unstructured":"Ibarra, O.H., Dang, Z., Egecioglu, O., Saxena, G.: Characterizations of Catalytic Membrane Computing Systems. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 480\u2013489. Springer, Heidelberg (2003)"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Ibarra, O.H., Jiang, T., Tran, N., Wang, H.: New decidability results concerning two-way counter machines. SIAM J. Computing\u00a0(24), 123\u2013137 (1995)","DOI":"10.1137\/S0097539792240625"},{"key":"2_CR35","unstructured":"Ibarra, O.H., Seki, S.: Characterizations of bounded semilinear languages by one-way and two-way deterministic machines. In: Proc. 13th Int. Conf. on Automata and Formal Languages, pp. 211\u2013224 (2011)"},{"key":"2_CR36","unstructured":"Ibarra, O.H., Seki, S.: Semilinear sets and counter machines: a brief survey (submitted)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44612-5_38","volume-title":"Mathematical Foundations of Computer Science 2000","author":"O.H. Ibarra","year":"2000","unstructured":"Ibarra, O.H., Su, J., Dang, Z., Bultan, T., Kemmerer, R.A.: Counter machines: decidable properties and applications to verification problems. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 426\u2013435. Springer, Heidelberg (2000)"},{"key":"2_CR38","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/j.tcs.2011.12.034","volume":"429","author":"O.H. Ibarra","year":"2012","unstructured":"Ibarra, O.H., Yen, H.-C.: On the containment and equivalence problems for two-way transducers. Theor. Comput. Sci.\u00a0429, 155\u2013163 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Minsky, M.: Recursive unsolvability of Post\u2019s problem of Tag and other topics in the theory of Turing machines. Ann. of Math.\u00a0(74), 437\u2013455 (1961)","DOI":"10.2307\/1970290"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-540-70583-3_32","volume-title":"Automata, Languages and Programming","author":"J.-F. Raskin","year":"2008","unstructured":"Raskin, J.-F., Servais, F.: Visibly pushdown transducers. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 386\u2013397. Springer, Heidelberg (2008)"},{"key":"2_CR41","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/11532231_25","volume-title":"Automated Deduction \u2013 CADE-20","author":"K.N. Verma","year":"2005","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 337\u2013352. Springer, Heidelberg (2005)"},{"issue":"1","key":"2_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0022-0000(74)80018-8","volume":"8","author":"S.J. Walljasper","year":"1974","unstructured":"Walljasper, S.J.: Left-derivation bounded languages. J. Comput. and System Sci.\u00a08(1), 1\u20137 (1974)","journal-title":"J. Comput. and System Sci."},{"key":"2_CR43","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1137\/0222014","volume":"22","author":"A. Weber","year":"1993","unstructured":"Weber, A.: Decomposing finite-valued transducers and deciding their equivalence. SIAM. J. on Computing\u00a022, 175\u2013202 (1993)","journal-title":"SIAM. J. on Computing"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Wich, K.: Exponential ambiguity of context-free grammars. In: Proc. of 4th Int. Conf. on Developments in Language Theory, pp. 125\u2013138. World Scientific (1999)","DOI":"10.1142\/9789812792464_0011"},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/3-540-45061-0_53","volume-title":"Automata, Languages and Programming","author":"G. Xie","year":"2003","unstructured":"Xie, G., Dang, Z., Ibarra, O.H.: A Solvable class of quadratic diophantine equations with applications to verification of infinite-state systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 668\u2013680. Springer, Heidelberg (2003)"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-45069-6_8","volume-title":"Computer Aided Verification","author":"G. Xie","year":"2003","unstructured":"Xie, G., Dang, Z., Ibarra, O.H., Miltersen, P.B.: Dense counter machines and verification problems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 93\u2013105. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Descriptional Complexity of Formal Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09704-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T04:31:22Z","timestamp":1558931482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09704-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319097039","9783319097046"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09704-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}