{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:57:09Z","timestamp":1742993829233,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319114385"},{"type":"electronic","value":"9783319114392"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11439-2_7","type":"book-chapter","created":{"date-parts":[[2014,9,15]],"date-time":"2014-09-15T01:30:11Z","timestamp":1410744611000},"page":"85-97","source":"Crossref","is-referenced-by-count":2,"title":["Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amit Kumar","family":"Dhar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L. Berman","year":"1980","unstructured":"Berman, L.: The complexity of logical theories. TCS\u00a011, 71\u201378 (1980)","journal-title":"TCS"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-24364-6_6","volume-title":"Frontiers of Combining Systems","author":"M. Bersani","year":"2011","unstructured":"Bersani, M., Demri, S.: The complexity of reversal-bounded model-checking. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol.\u00a06989, pp. 71\u201386. Springer, Heidelberg (2011)"},{"key":"7_CR3","unstructured":"Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-54013-4_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Bozga","year":"2014","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Safety problems are NP-complete for flat integer programs with octagonal loops. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol.\u00a08318, pp. 242\u2013261. Springer, Heidelberg (2014)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/3-540-36494-3_60","volume-title":"STACS 2003","author":"V. Bruy\u00e8re","year":"2003","unstructured":"Bruy\u00e8re, V., Dall\u2019Olio, E., Raskin, J.: Durations, parametric model-checking in timed automata with presburger arithmetic. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 687\u2013698. Springer, Heidelberg (2003)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counter automata, safety analysis and Presburger Arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"7_CR7","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. de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-31365-3_16","volume-title":"Automated Reasoning","author":"S. Demri","year":"2012","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: Taming past LTL and flat counter systems. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 179\u2013193. Springer, Heidelberg (2012)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a07966, pp. 162\u2013173. Springer, Heidelberg (2013)"},{"issue":"4","key":"7_CR10","first-page":"313","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. JANCL\u00a020(4), 313\u2013344 (2010)","journal-title":"JANCL"},{"key":"7_CR11","unstructured":"Dhar, A.K.: Applying Satisfiability Modulo Theories Techniques to the Verification of Infinite-State Systems. PhD thesis, Universit\u00e9 Paris VII-Denis Diderot (2014)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"A. Emerson","year":"1986","unstructured":"Emerson, A., Halpern, J.: \u2018sometimes\u2018 and \u2019not never\u2019 revisited: on branching versus linear time temporal logic. JACM\u00a033, 151\u2013178 (1986)","journal-title":"JACM"},{"issue":"3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program.\u00a08(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28729-9_27","volume-title":"Foundations of Software Science and Computational Structures","author":"S. G\u00f6ller","year":"2012","unstructured":"G\u00f6ller, S., Haase, C., Ouaknine, J., Worrell, J.: Branching-time model checking of parametric one-counter automata. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol.\u00a07213, pp. 406\u2013420. Springer, Heidelberg (2012)"},{"issue":"3","key":"7_CR16","doi-asserted-by":"publisher","first-page":"884","DOI":"10.1137\/120876435","volume":"42","author":"S. G\u00f6ller","year":"2013","unstructured":"G\u00f6ller, S., Lohrey, M.: Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput.\u00a042(3), 884\u2013923 (2013)","journal-title":"SIAM J. Comput."},{"key":"7_CR17","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":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45315-6_21","volume-title":"Foundations of Software Science and Computation Structures","author":"F. Laroussinie","year":"2001","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking CTL\u2009+\u2009 and FCTL is hard. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 318\u2013331. Springer, Heidelberg (2001)"},{"key":"7_CR19","unstructured":"Leroux, J.: Presburger counter machines. Habilitation thesis, U. of Bordeaux (2012)"},{"key":"7_CR20","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":"7_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.\u00a03170, pp. 402\u2013416. Springer, Heidelberg (2004)"},{"key":"7_CR22","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)"},{"key":"7_CR23","volume-title":"Computation, Finite and Infinite Machines","author":"M. Minsky","year":"1967","unstructured":"Minsky, M.: Computation, Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"7_CR24","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 (1929)"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11439-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,21]],"date-time":"2023-01-21T02:45:50Z","timestamp":1674269150000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-11439-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319114385","9783319114392"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11439-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}