{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T22:01:02Z","timestamp":1726005662690},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030112448"},{"type":"electronic","value":"9783030112455"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_24","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T18:45:18Z","timestamp":1547145918000},"page":"513-534","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic"],"prefix":"10.1007","author":[{"given":"Normann","family":"Decker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Pirogov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"24_CR1","unstructured":"Abdulla, P.A., Atig, M.F., Meyer, R., Salehi, M.S.: What\u2019s decidable about availability languages? In: FSTTCS. LIPIcs, vol. 45, pp. 192\u2013205 (2015)"},{"key":"24_CR2","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. 3707, pp. 474\u2013488. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562948_35"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300\u2013309. ACM (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"24_CR4","unstructured":"Biere, A.: Bounded model checking. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457\u2013481. IOS Press (2009)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bollig, B., Decker, N., Leucker, M.: Frequency linear-time temporal logic. In: TASE, pp. 85\u201392. IEEE (2012)","DOI":"10.1109\/TASE.2012.43"},{"issue":"2","key":"24_CR7","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1090\/S0002-9939-1976-0396605-3","volume":"55","author":"I Borosh","year":"1976","unstructured":"Borosh, I., Treybig, L.B.: Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc. 55(2), 299\u2013304 (1976)","journal-title":"Proc. Am. Math. Soc."},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS, pp. 123\u2013133. IEEE (1995)","DOI":"10.1109\/LICS.1995.523250"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-78800-3_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Caniart","year":"2008","unstructured":"Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 428\u2013442. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_32"},{"issue":"1","key":"24_CR10","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s10817-015-9328-2","volume":"55","author":"DR Cok","year":"2015","unstructured":"Cok, D.R., Stump, A., Weber, T.: The 2013 evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55(1), 61\u201390 (2015)","journal-title":"J. Autom. Reason."},{"key":"24_CR11","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. 1862, pp. 262\u2013276. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44622-2_17"},{"key":"24_CR12","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 counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268\u2013279. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028751"},{"key":"24_CR13","unstructured":"Decker, N., Habermehl, P., Leucker, M., Sangnier, A., Thoma, D.: Model-checking counting temporal logics on flat structures. In: CONCUR. LIPIcs, vol. 85, pp. 29:1\u201329:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_7"},{"key":"24_CR15","doi-asserted-by":"crossref","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":"3","key":"24_CR16","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"key":"24_CR17","unstructured":"Dhar, A.K.: Algorithms for model-checking flat counter systems. Ph.D. thesis, Universit\u00e9 Paris Diderot (2014)"},{"key":"24_CR18","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: Abiteboul, S., Shamir, E. (eds.) ICALP 1994. LNCS, vol. 820, pp. 35\u201346. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58201-0_56"},{"issue":"11","key":"24_CR19","doi-asserted-by":"crossref","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","volume":"30","author":"ER Gansner","year":"2000","unstructured":"Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Softw. Pract. Exp. 30(11), 1203\u20131233 (2000)","journal-title":"Softw. Pract. Exp."},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-15375-4_32","volume-title":"CONCUR 2010 - Concurrency Theory","author":"J Hoenicke","year":"2010","unstructured":"Hoenicke, J., Meyer, R., Olderog, E.-R.: Kleene, Rabin, and Scott are available. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 462\u2013477. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_32"},{"key":"24_CR21","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, pp. 187\u2013202. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16"},{"issue":"5","key":"24_CR22","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/s10009-014-0337-y","volume":"16","author":"F Howar","year":"2014","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems - the RERS challenges 2012 and 2013. STTT 16(5), 457\u2013464 (2014)","journal-title":"STTT"},{"issue":"2","key":"24_CR23","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s00165-009-0110-2","volume":"22","author":"D Kroening","year":"2010","unstructured":"Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2), 105\u2013128 (2010)","journal-title":"Formal Asp. Comput."},{"key":"24_CR24","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). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_28"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In: TIME, pp. 51\u201358. IEEE (2010)","DOI":"10.1109\/TIME.2010.20"},{"issue":"1","key":"24_CR26","first-page":"1","volume":"9","author":"F Laroussinie","year":"2012","unstructured":"Laroussinie, F., Meyer, A., Petonnet, E.: Counting CTL. Log. Methods Comput. Sci. 9(1), 1\u201334 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"24_CR27","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). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_26"},{"key":"24_CR28","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Upper Saddle River (1967)"},{"key":"24_CR29","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"24_CR31","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":"3","key":"24_CR32","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T03:17:45Z","timestamp":1573701465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}