{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:38:37Z","timestamp":1725748717103},"publisher-location":"Berlin, Heidelberg","reference-count":96,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642408847"},{"type":"electronic","value":"9783642408854"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_9","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T07:20:19Z","timestamp":1378884019000},"page":"120-150","source":"Crossref","is-referenced-by-count":1,"title":["Witness Runs for Counter Machines"],"prefix":"10.1007","author":[{"given":"Clark","family":"Barrett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"9_CR1","first-page":"783","volume":"22","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Habermehl, P.: On Yen\u2019s path logic for Petri nets. IJFCS\u00a022(4), 783\u2013799 (2011)","journal-title":"IJFCS"},{"issue":"2","key":"9_CR2","first-page":"91","volume":"127","author":"P. Abdulla","year":"1996","unstructured":"Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels. I & C\u00a0127(2), 91\u2013101 (1996)","journal-title":"I & C"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists Are Counter Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/S0065-2458(03)58003-2","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":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"9_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-24364-6_6","volume-title":"Frontiers of Combining Systems","author":"M.M. Bersani","year":"2011","unstructured":"Bersani, M.M., Demri, S.: The complexity of reversal-bounded model-checking. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol.\u00a06989, pp. 71\u201386. Springer, Heidelberg (2011)"},{"key":"9_CR7","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.-F.: 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":"9_CR8","unstructured":"Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS 1995, pp. 123\u2013133 (1995)"},{"key":"9_CR9","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":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bardin","year":"2005","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 474\u2013488. Springer, Heidelberg (2005)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Bersani, M.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 (2010)","DOI":"10.1109\/TIME.2010.21"},{"key":"9_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/11916277_14","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Bozzelli","year":"2006","unstructured":"Bozzelli, L., Gascon, R.: Branching-time temporal logic extended with qualitative Presburger constraints. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 197\u2013211. Springer, Heidelberg (2006)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-00768-2_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., G\u00eerlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 337\u2013351. Springer, Heidelberg (2009)"},{"key":"9_CR14","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.\u00a06174, pp. 227\u2013242. Springer, Heidelberg (2010)"},{"issue":"2","key":"9_CR15","doi-asserted-by":"crossref","first-page":"275","DOI":"10.3233\/FI-2009-0044","volume":"91","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. FI\u00a091(2), 275\u2013303 (2009)","journal-title":"FI"},{"key":"9_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45744-5_50","volume-title":"Automated Reasoning","author":"B. Boigelot","year":"2001","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 611\u2013625. Springer, Heidelberg (2001)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/3-540-61648-9_56","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M. Biehl","year":"1996","unstructured":"Biehl, M., Klarlund, N., Rauhe, T.: MONA: Decidable arithmetic in practice. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol.\u00a01135, pp. 459\u2013462. Springer, Heidelberg (1996)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., Lasota, S.: An extension of data automata that captures XPath. In: LICS 2010, pp. 243\u2013252. IEEE (2010)","DOI":"10.1109\/LICS.2010.33"},{"key":"9_CR19","unstructured":"Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1999)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27940-9_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Bozzelli","year":"2012","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 88\u2013103. Springer, Heidelberg (2012)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-22993-0_13","volume-title":"Mathematical Foundations of Computer Science 2011","author":"M. Blockelet","year":"2011","unstructured":"Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol.\u00a06907, pp. 108\u2013119. Springer, Heidelberg (2011)"},{"key":"9_CR22","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, ch. 26, pp. 825\u2013885. IOS Press (2008)"},{"key":"9_CR23","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0 (September 2012), http:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.0-r12.09.09.pdf"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1994","unstructured":"Boigelot, B., Wolper, P.: Verification with Periodic Sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 55\u201367. Springer, Heidelberg (1994)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1998","unstructured":"Boigelot, B., Wolper, P.: Verifying systems with infinite but regular state spaces. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-44622-2_17","volume-title":"Computer Science Logic","author":"H. Comon","year":"2000","unstructured":"Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 262\u2013276. Springer, Heidelberg (2000)"},{"key":"9_CR27","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press (2000)"},{"key":"9_CR28","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":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-40184-8_32","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"C. Carapelle","year":"2013","unstructured":"Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of CTL* with constraints. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol.\u00a08052, pp. 455\u2013469. Springer, Heidelberg (2013)"},{"key":"9_CR30","unstructured":"Conchon, S.: SMT Techniques and their Applications: from Alt-Ergo to Cubicle. Habilitation \u00e0 Diriger des Recherches, Universit\u00e9 Paris-Sud (2012)"},{"key":"9_CR31","first-page":"91","volume":"7","author":"D. Cooper","year":"1972","unstructured":"Cooper, D.: Theorem proving in arithmetic without multiplication. Machine Learning\u00a07, 91\u201399 (1972)","journal-title":"Machine Learning"},{"issue":"3","key":"9_CR32","first-page":"380","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. I & C\u00a0205(3), 380\u2013415 (2007)","journal-title":"I & C"},{"key":"9_CR33","series-title":"LNAI","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 (LNAI), vol.\u00a07364, pp. 179\u2013193. Springer, Heidelberg (2012)"},{"key":"9_CR34","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":"9_CR35","first-page":"313","volume":"20","author":"S. Demri","year":"2010","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking $\\textsf{CTL}^{*}$ over flat Presburger counter systems. JANCL\u00a020(4), 313\u2013344 (2010)","journal-title":"JANCL"},{"issue":"1","key":"9_CR36","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.tcs.2008.07.023","volume":"409","author":"S. Demri","year":"2008","unstructured":"Demri, S., Gascon, R.: Verification of qualitative Z constraints. TCS\u00a0409(1), 24\u201340 (2008)","journal-title":"TCS"},{"issue":"6","key":"9_CR37","first-page":"1541","volume":"19","author":"S. Demri","year":"2009","unstructured":"Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. JLC\u00a019(6), 1541\u20131575 (2009)","journal-title":"JLC"},{"issue":"1","key":"9_CR38","first-page":"2","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri, S., Lazi\u0107, R., Nowak, D.: On the freeze quantifier in constraint LTL: decidability and complexity. I & C\u00a0205(1), 2\u201324 (2007)","journal-title":"I & C"},{"issue":"22-24","key":"9_CR39","doi-asserted-by":"publisher","first-page":"2298","DOI":"10.1016\/j.tcs.2010.02.021","volume":"411","author":"S. Demri","year":"2010","unstructured":"Demri, S., Lazi\u0107, R., Sangnier, A.: Model checking memoryful linear-time logics over one-counter automata. TCS\u00a0411(22-24), 2298\u20132316 (2010)","journal-title":"TCS"},{"key":"9_CR40","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\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":"9_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BFb0017477","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"J. Esparza","year":"1994","unstructured":"Esparza, J.: On the decidability of model checking for several \u03bc-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 115\u2013129. Springer, Heidelberg (1994)"},{"issue":"6","key":"9_CR42","first-page":"1017","volume":"12","author":"M. Fitting","year":"2002","unstructured":"Fitting, M.: Modal logic between propositional and first-order. JLC\u00a012(6), 1017\u20131026 (2002)","journal-title":"JLC"},{"key":"9_CR43","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. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"9_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-63141-0_15","volume-title":"CONCUR\u201997: Concurrency Theory","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Ols\u00e9n, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 213\u2013227. Springer, Heidelberg (1997)"},{"key":"9_CR45","unstructured":"Fischer, M., Rabin, M.: Super-exponential complexity of Presburger arithmetic. In: Complexity of Computation. SIAM-AMS proceedings, vol.\u00a07, pp. 27\u201342. AMS (1974)"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"Ferrante, J., Rackoff, C.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol.\u00a0718. Springer (1979)","DOI":"10.1007\/BFb0062837"},{"key":"9_CR47","unstructured":"Fribourg, L.: Petri nets, flat languages and linear arithmetic. In: 9th Workshop on Functional and Logic Programming (WFLP), pp. 344\u2013365 (2000)"},{"issue":"1-2","key":"9_CR48","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transitions systems everywhere! TCS\u00a0256(1-2), 63\u201392 (2001)","journal-title":"TCS"},{"key":"9_CR49","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":"9_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-03816-7_29","volume-title":"Mathematical Foundations of Computer Science 2009","author":"D. Figueira","year":"2009","unstructured":"Figueira, D., Segoufin, L.: Future-looking logics on data words and trees. In: Kr\u00e1lovi\u010d, R., Niwi\u0144ski, D. (eds.) MFCS 2009. LNCS, vol.\u00a05734, pp. 331\u2013343. Springer, Heidelberg (2009)"},{"key":"9_CR51","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":"9_CR52","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-540-73595-3_25","volume-title":"Automated Deduction \u2013 CADE-21","author":"S. Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 362\u2013378. Springer, Heidelberg (2007)"},{"key":"9_CR53","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BFb0013985","volume-title":"Temporal Logic","author":"V. Goranko","year":"1994","unstructured":"Goranko, V.: Temporal logic with reference pointers. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS (LNAI), vol.\u00a0827, pp. 133\u2013148. Springer, Heidelberg (1994)"},{"key":"9_CR54","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(88)90136-3","volume":"56","author":"E. Gr\u00e4del","year":"1988","unstructured":"Gr\u00e4del, E.: Subclasses of Presburger arithmetic and the polynomial-time hierarchy. TCS\u00a056, 289\u2013301 (1988)","journal-title":"TCS"},{"issue":"3","key":"9_CR55","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. German","year":"1992","unstructured":"German, S., Sistla, P.: Reasoning about systems with many processes. JACM\u00a039(3), 675\u2013735 (1992)","journal-title":"JACM"},{"key":"9_CR56","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":"9_CR57","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: Half-order modal logic: how to prove real-time properties. In: PODC 1990, pp. 281\u2013296. ACM Press (1990)","DOI":"10.1145\/93385.93429"},{"key":"9_CR58","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)"},{"key":"9_CR59","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. TCS\u00a08, 135\u2013159 (1979)","journal-title":"TCS"},{"issue":"1","key":"9_CR60","first-page":"55","volume":"34","author":"R.R. Howell","year":"1987","unstructured":"Howell, R.R., Rosier, L.E.: An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. JCSS\u00a034(1), 55\u201374 (1987)","journal-title":"JCSS"},{"key":"9_CR61","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0304-3975(89)90053-4","volume":"64","author":"R.R. Howell","year":"1989","unstructured":"Howell, R.R., Rosier, L.E.: Problems concerning fairness and temporal logic for conflict-free petri nets. TCS\u00a064, 305\u2013329 (1989)","journal-title":"TCS"},{"key":"9_CR62","first-page":"222","volume":"12","author":"H. Hunt","year":"1976","unstructured":"Hunt, H., Rosenkrantz, D., Szymanski, T.: On the equivalence, containment, and covering problems for the regular and context-free languages. JCSS\u00a012, 222\u2013268 (1976)","journal-title":"JCSS"},{"issue":"1","key":"9_CR63","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. Ibarra","year":"1978","unstructured":"Ibarra, O.: Reversal-bounded multicounter machines and their decision problems. JACM\u00a025(1), 116\u2013133 (1978)","journal-title":"JACM"},{"issue":"1","key":"9_CR64","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(90)90006-4","volume":"74","author":"P. Jan\u010dar","year":"1990","unstructured":"Jan\u010dar, P.: Decidability of a temporal logic problem for Petri nets. TCS\u00a074(1), 71\u201393 (1990)","journal-title":"TCS"},{"issue":"2","key":"9_CR65","first-page":"147","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. JCSS\u00a03(2), 147\u2013195 (1969)","journal-title":"JCSS"},{"key":"9_CR66","doi-asserted-by":"crossref","unstructured":"Kosaraju, R.: Decidability of reachability in vector addition systems. In: STOC 1982, pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"key":"9_CR67","unstructured":"Leroux, J.: Algorithmique de la v\u00e9rification des syst\u00e8mes \u00e0 compteurs. Approximation et acc\u00e9l\u00e9ration. Impl\u00e9mentation de l\u2019outil FAST. PhD thesis, ENS de Cachan, France (2003)"},{"key":"9_CR68","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LICS 2009, pp. 4\u201313. IEEE (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"9_CR69","unstructured":"Leroux, J.: Presburger counter machines. Habilitation \u00e0 Diriger des Recherches, Universit\u00e9 Bordeaux (2012)"},{"key":"9_CR70","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Presburger Vector Addition Systems. In: LICS 2013, pp. 23\u201332. IEEE (2013)","DOI":"10.1109\/LICS.2013.7"},{"key":"9_CR71","unstructured":"Lipton, R.J.: The reachability problem requires exponential space. Technical Report\u00a062, Department of Computer Science, Yale University (1976)"},{"key":"9_CR72","unstructured":"Lisitsa, A., Potapov, I.: Temporal logic with predicate \u03bb-abstraction. In: TIME 2005, pp. 147\u2013155. IEEE (2005)"},{"key":"9_CR73","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":"9_CR74","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":"9_CR75","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"},{"issue":"3","key":"9_CR76","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E. Mayr","year":"1984","unstructured":"Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM Journal of Computing\u00a013(3), 441\u2013460 (1984)","journal-title":"SIAM Journal of Computing"},{"issue":"1-3","key":"9_CR77","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0304-3975(02)00646-1","volume":"297","author":"R. Mayr","year":"2003","unstructured":"Mayr, R.: Undecidable problems in unreliable computations. TCS\u00a0297(1-3), 337\u2013354 (2003)","journal-title":"TCS"},{"issue":"3","key":"9_CR78","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M. Minsky","year":"1961","unstructured":"Minsky, M.: Recursive unsolvability of Post\u2019s problems of \u2018tag\u2019 and other topics in theory of Turing machines. Annals of Mathematics\u00a074(3), 437\u2013455 (1961)","journal-title":"Annals of Mathematics"},{"key":"9_CR79","unstructured":"Minsky, M.: Computation, Finite and Infinite Machines. Prentice Hall (1967)"},{"key":"9_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 585\u2013599. Springer, Heidelberg (2010)"},{"key":"9_CR81","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"9_CR82","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reative systems: safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"2","key":"9_CR83","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(77)90001-9","volume":"5","author":"A. Mandel","year":"1977","unstructured":"Mandel, A., Simon, I.: On finite semigroups of matrices. TCS\u00a05(2), 101\u2013111 (1977)","journal-title":"TCS"},{"issue":"3","key":"9_CR84","first-page":"323","volume":"16","author":"D. Oppen","year":"1978","unstructured":"Oppen, D.: A $2^{2^{2pn}}$ upper bound on the complexity of Presburger arithmetic. JCSS\u00a016(3), 323\u2013332 (1978)","journal-title":"JCSS"},{"key":"9_CR85","unstructured":"Ouaknine, J., Worrell, J.: On the Decidability of Metric Temporal Logic. In: LICS 2005, pp. 188\u2013197. IEEE (2005)"},{"key":"9_CR86","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9_CR87","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)"},{"issue":"8","key":"9_CR88","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: A practical algorithm for exact array dependence analysis. Communications of the ACM\u00a035(8), 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"key":"9_CR89","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)"},{"key":"9_CR90","unstructured":"Reutenauer, C.: The mathematics of Petri nets. Masson and Prentice (1990)"},{"key":"9_CR91","doi-asserted-by":"crossref","unstructured":"Reddy, C., Loveland, W.: Presburger arithmetic with bounded quantifier alternation. In: STOC 1978, pp. 320\u2013325. ACM Press (1978)","DOI":"10.1145\/800133.804361"},{"key":"9_CR92","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"P. Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. IPL\u00a083, 251\u2013261 (2002)","journal-title":"IPL"},{"key":"9_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-642-15155-2_54","volume-title":"Mathematical Foundations of Computer Science 2010","author":"P. Schnoebelen","year":"2010","unstructured":"Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 616\u2013628. Springer, Heidelberg (2010)"},{"issue":"2","key":"9_CR94","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. Shostak","year":"1979","unstructured":"Shostak, R.: A practical decision procedure for arithmetic with function symbols. JACM\u00a026(2), 351\u2013360 (1979)","journal-title":"JACM"},{"issue":"1","key":"9_CR95","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":"9_CR96","unstructured":"Segoufin, L., Torunczyk, S.: Automata based verification over linearly ordered data domains. In: STACS 2011, pp. 81\u201392 (2011)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40885-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T16:19:32Z","timestamp":1596471572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":96,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}