{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T22:24:47Z","timestamp":1742941487555,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319465197"},{"type":"electronic","value":"9783319465203"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46520-3_6","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T06:40:27Z","timestamp":1474440027000},"page":"89-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?"],"prefix":"10.1007","author":[{"given":"Radu","family":"Iosif","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090","volume-title":"Computational Complexity: A Modern Approach","author":"S Arora","year":"2009","unstructured":"Arora, S., Barak, B.: Computational Complexity: A Modern Approach. Cambridge University Press, Cambridge (2009)"},{"key":"6_CR2","unstructured":"Bardin, S., Finkel, A., Petrucci, J.L.L.: FAST: fast acceleration of symbolic transition systems. \n                      http:\/\/tapas.labri.fr\/trac\/wiki\/FASTer"},{"key":"6_CR3","unstructured":"Blondin, M., Finkel, A., G\u00f6ller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is PSPACE-complete. CoRR abs\/1412.4259 (2014). \n                      http:\/\/arxiv.org\/abs\/1412.4259"},{"key":"6_CR4","unstructured":"Boigelot, B.: Symbolic methods for exploring infinite state spaces. Ph.D., Univ. de Li\u00e8ge (1999)"},{"issue":"3","key":"6_CR5","first-page":"1","volume":"10","author":"M Bozga","year":"2014","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Deciding conditional termination. Log. Methods Comput. Sci. 10(3), 1\u201361 (2014)","journal-title":"Log. Methods Comput. Sci."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-48320-9_18","volume-title":"Concurrency Theory \u2013 CONCUR 1999","author":"H Comon","year":"1999","unstructured":"Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 242\u2013257. Springer, Heidelberg (1999)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-642-39212-2_17","volume-title":"Automata, Languages, and Programming","author":"S Demri","year":"2013","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: On the complexity of verifying regular properties on flat counter systems. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 162\u2013173. Springer, Heidelberg (2013)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-319-11439-2_7","volume-title":"Reachability Problems","author":"S Demri","year":"2014","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: Equivalence between model-checking flat counter systems and Presburger arithmetic. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 85\u201397. Springer, Heidelberg (2014)"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1016\/j.ic.2015.03.007","volume":"242","author":"S Demri","year":"2015","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: Taming past LTL and flat counter systems. Inf. Comput. 242, 306\u2013339 (2015)","journal-title":"Inf. Comput."},{"issue":"4","key":"6_CR11","doi-asserted-by":"publisher","first-page":"313","DOI":"10.3166\/jancl.20.313-344","volume":"20","author":"S Demri","year":"2010","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking CTL* over flat Presburger counter systems. J. Appl. Non-Class. Log. 20(4), 313\u2013344 (2010)","journal-title":"J. Appl. Non-Class. Log."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Gawlitza, T.M., Monniaux, D.: Invariant generation through strategy iteration in succinctly represented control flow graphs. Logical Methods Comput. Sci. 8(3) (2012)","DOI":"10.2168\/LMCS-8(3:29)2012"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-642-14162-1_48","volume-title":"Automata, Languages and Programming","author":"S G\u00f6ller","year":"2010","unstructured":"G\u00f6ller, S., Haase, C., Ouaknine, J., Worrell, J.: Model checking succinct and parametric one-counter automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 575\u2013586. Springer, Heidelberg (2010)"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/0022-0000(81)90028-3","volume":"22","author":"EM Gurari","year":"1981","unstructured":"Gurari, E.M., Ibarra, O.H.: The complexity of decision problems for finite-turn multicounter machines. J. Comput. Syst. Sci. 22, 220\u2013229 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Haase, C.: Subclasses of Presburger arithmetic and the weak EXP hierarchy. In: CSL-LICS 2014, pp. 47:1\u201347:10. ACM (2014)","DOI":"10.1145\/2603088.2603092"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 187\u2013202. Springer, Heidelberg (2012)"},{"key":"6_CR18","unstructured":"Iosif, R., Sangnier, A.: How hard is it to verify flat affine counter systems with the finite monoid property? CoRR abs\/1605.05836 (2016). \n                      http:\/\/arxiv.org\/abs\/1605.05836"},{"key":"6_CR19","unstructured":"Konecny, F., Iosif, R., Bozga, M.: FLATA: a verification toolset for counter machines (2009). \n                      http:\/\/nts.imag.fr\/index.php\/Flata"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-23217-6_28","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"L Kuhtz","year":"2011","unstructured":"Kuhtz, L., Finkbeiner, B.: Weak Kripke structures and LTL. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 419\u2013433. Springer, Heidelberg (2011)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-540-28644-8_26","volume-title":"CONCUR 2004 - Concurrency Theory","author":"J Leroux","year":"2004","unstructured":"Leroux, J., Sutre, G.: On flatness for 2-Dimensional vector addition systems with states. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 402\u2013416. Springer, Heidelberg (2004)"},{"key":"6_CR22","unstructured":"Lipton, R.J.: The reachability problem is exponential-space-hard. Technical report 62, Department of Computer Science, Yale University (1976)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-45187-7_17","volume-title":"CONCUR 2003 - Concurrency Theory","author":"N Markey","year":"2003","unstructured":"Markey, N., Schnoebelen, P.: Model checking a path. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 251\u2013265. Springer, Heidelberg (2003)"},{"key":"6_CR24","volume-title":"Computation: Finite and Infinite Machines","author":"M Minsky","year":"1967","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Upper Saddle River (1967)"},{"issue":"3","key":"6_CR25","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"6_CR26","unstructured":"Stockmeyer, L.J.: The complexity of decision problems in automata and logic. Ph.D. thesis, MIT (1974)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46520-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:13:06Z","timestamp":1558314786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46520-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465197","9783319465203"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46520-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"22 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chiba","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}