{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:25:33Z","timestamp":1743128733642,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243639"},{"type":"electronic","value":"9783642243646"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24364-6_6","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T01:22:21Z","timestamp":1317259341000},"page":"71-86","source":"Crossref","is-referenced-by-count":5,"title":["The Complexity of Reversal-Bounded Model-Checking"],"prefix":"10.1007","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","first-page":"164","volume-title":"FOCS 1989","author":"R. Alur","year":"1989","unstructured":"Alur, R., Henzinger, T.: A really temporal logic. In: FOCS 1989, pp. 164\u2013169. IEEE, Los Alamitos (1989)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-73368-3_36","volume-title":"Computer Aided Verification","author":"B. Becker","year":"2007","unstructured":"Becker, B., Dax, C., Eisinger, J., Klaedtke, F.: LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 307\u2013310. Springer, Heidelberg (2007)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Bersani, M., Demri, S.: The complexity of reversal-bounded model checking. Tech. Rep. LSV-11-10, LSV, ENS Cachan, France (May 2011)","DOI":"10.1007\/978-3-642-24364-6_6"},{"key":"6_CR5","first-page":"43","volume-title":"TIME 2010","author":"M. Bersani","year":"2010","unstructured":"Bersani, M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: TIME 2010, pp. 43\u201350. IEEE, Los Alamitos (2010)"},{"key":"6_CR6","first-page":"118","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 118\u2013149 (2003)","journal-title":"Advances in Computers"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1090\/S0002-9939-1976-0396605-3","volume":"55","author":"I. Borosh","year":"1976","unstructured":"Borosh, I., Treybig, L.: Bounds on positive integral solutions of linear diophantine equations. Proocedings of The American Mathematical Society\u00a055, 299\u2013304 (1976)","journal-title":"Proocedings of The American Mathematical Society"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS 1995, pp. 123\u2013133 (1995)","DOI":"10.1109\/LICS.1995.523250"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-58201-0_56","volume-title":"Automata, Languages, and Programming","author":"K. \u010cer\u0101ns","year":"1994","unstructured":"\u010cer\u0101ns, K.: Deciding properties of integral relational automata. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol.\u00a0820, pp. 35\u201346. Springer, Heidelberg (1994)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-45294-X_12","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"Z. Dang","year":"2001","unstructured":"Dang, Z., Ibarra, O., San Pietro, P.: 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)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Demri, S.: On Selective Unboundedness of VASS. In: INFINITY 2010. EPTCS, vol.\u00a039, pp. 1\u201315 (2010)","DOI":"10.4204\/EPTCS.39.1"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: Basic Models","author":"J. Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and complexity of Petri net problems \u2014 an introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol.\u00a01491, pp. 374\u2013428. Springer, Heidelberg (1998)"},{"key":"6_CR13","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":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-10843-2_39","volume-title":"Automata, Languages and Programming","author":"E. Gurari","year":"1981","unstructured":"Gurari, E., Ibarra, O.: The complexity of decision problems for finite-turn multicounter machines. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol.\u00a0115, pp. 495\u2013505. Springer, Heidelberg (1981)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/3-540-63139-9_32","volume-title":"Application and Theory of Petri Nets 1997","author":"P. Habermehl","year":"1997","unstructured":"Habermehl, P.: On the complexity of the linear-time mu-calculus for Petri nets. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol.\u00a01248, pp. 102\u2013116. Springer, Heidelberg (1997)"},{"key":"6_CR16","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":"1","key":"6_CR17","first-page":"55","volume":"34","author":"R. Howell","year":"1987","unstructured":"Howell, R., Rosier, L.: An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. JCSS\u00a034(1), 55\u201374 (1987)","journal-title":"JCSS"},{"key":"6_CR18","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","key":"6_CR19","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0304-3975(01)00268-7","volume":"289","author":"O. Ibarra","year":"2002","unstructured":"Ibarra, O., Su, J., Dang, Z., Bultan, T., Kemmerer, R.: Counter Machines and Verification Problems. TCS\u00a0289(1), 165\u2013189 (2002)","journal-title":"TCS"},{"issue":"1","key":"6_CR20","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. JACM\u00a025(1), 116\u2013133 (1978)","journal-title":"JACM"},{"key":"6_CR21","first-page":"80","volume-title":"LICS 2010","author":"E. Kopczynski","year":"2010","unstructured":"Kopczynski, E., To, A.: Parikh Images of Grammars: Complexity and Applications. In: LICS 2010, pp. 80\u201389. IEEE, Los Alamitos (2010)"},{"key":"6_CR22","first-page":"51","volume-title":"TIME 2010","author":"F. Laroussinie","year":"2010","unstructured":"Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In: TIME 2010, pp. 51\u201358. IEEE, Los Alamitos (2010)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-00768-2_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Leroux","year":"2009","unstructured":"Leroux, J., Point, G.: TaPAS: The Talence Presburger Arithmetic Suite. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 182\u2013185. Springer, Heidelberg (2009)"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J. Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"issue":"4","key":"6_CR25","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1145\/1024922.1024925","volume":"5","author":"C. Lutz","year":"2004","unstructured":"Lutz, C.: NEXPTIME-complete description logics with concrete domains. ACM ToCL\u00a05(4), 669\u2013705 (2004)","journal-title":"ACM ToCL"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f6rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"4","key":"6_CR27","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.: On the complexity of integer programming. JACM\u00a028(4), 765\u2013768 (1981)","journal-title":"JACM"},{"key":"6_CR28","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier congr\u00e8s de math\u00e9maticiens des Pays Slaves, Warszawa, pp. 92\u2013101 (1930)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"issue":"2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS\u00a06(2), 223\u2013231 (1978)","journal-title":"TCS"},{"issue":"1","key":"6_CR31","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N. Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.: Verification Decidability of Presburger Array Programs. JACM\u00a027(1), 191\u2013205 (1980)","journal-title":"JACM"},{"key":"6_CR32","unstructured":"To, A.: Model Checking Infinite-State Systems: Generic and Specific Approaches. Ph.D. thesis, School of Informatics, University of Edinburgh (2010)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-12032-9_16","volume-title":"Foundations of Software Science and Computational Structures","author":"A. To","year":"2010","unstructured":"To, A., Libkin, L.: Algorithmic metatheorems for decidable LTL model checking over infinite systems. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 221\u2013236. Springer, Heidelberg (2010)"},{"key":"6_CR34","first-page":"1","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115, 1\u201337 (1994)","journal-title":"I&C"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24364-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T14:00:11Z","timestamp":1560693611000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24364-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243639","9783642243646"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24364-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}