{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:13:03Z","timestamp":1725549183351},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120312"},{"type":"electronic","value":"9783642120329"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-12032-9_13","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:07:56Z","timestamp":1268010476000},"page":"176-190","source":"Crossref","is-referenced-by-count":10,"title":["When Model-Checking Freeze LTL over Counter Machines Becomes Decidable"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.: A really temporal logic. JACM\u00a041(1), 181\u2013204 (1994)","journal-title":"JACM"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/3-540-48168-0_22","volume-title":"Computer Science Logic","author":"C. Areces","year":"1999","unstructured":"Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 307\u2013321. Springer, Heidelberg (1999)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"862","DOI":"10.1007\/978-3-540-73420-8_74","volume-title":"Automata, Languages and Programming","author":"H. Bj\u00f6rklund","year":"2007","unstructured":"Bj\u00f6rklund, H., Boja\u0144czyk, M.: Bounded depth data trees. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol.\u00a04596, pp. 862\u2013874. Springer, Heidelberg (2007)"},{"key":"13_CR4","unstructured":"Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"13_CR5","first-page":"7","volume-title":"LICS 2006","author":"M. Boja\u0144czyk","year":"2006","unstructured":"Boja\u0144czyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS 2006, pp. 7\u201316. IEEE, Los Alamitos (2006)"},{"key":"13_CR6","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":"13_CR7","first-page":"109","volume-title":"LICS 2007","author":"P. Bouyer","year":"2007","unstructured":"Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: LICS 2007, pp. 109\u2013118. IEEE, Los Alamitos (2007)"},{"issue":"2","key":"13_CR8","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. Fundamenta Informaticae\u00a091(2), 275\u2013303 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"13_CR9","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":"13_CR10","first-page":"82","volume-title":"TIME 2007","author":"U. Lago Dal","year":"2007","unstructured":"Dal Lago, U., Montanari, A., Puppis, G.: On the equivalence of automaton-based representations of time granularities. In: TIME 2007, pp. 82\u201393. IEEE, Los Alamitos (2007)"},{"key":"13_CR11","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":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/11901914_36","volume-title":"Automated Technology for Verification and Analysis","author":"S. Demri","year":"2006","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Towards a model-checker for counter systems. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 493\u2013507. Springer, Heidelberg (2006)"},{"issue":"6","key":"13_CR13","doi-asserted-by":"publisher","first-page":"1541","DOI":"10.1093\/logcom\/exp037","volume":"19","author":"S. Demri","year":"2009","unstructured":"Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. Journal of Logic and Computation\u00a019(6), 1541\u20131575 (2009)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"13_CR14","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"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-540-78499-9_34","volume-title":"Foundations of Software Science and Computational Structures","author":"S. Demri","year":"2008","unstructured":"Demri, S., Lazi\u0107, R., Sangnier, A.: Model checking freeze LTL over one-counter automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 490\u2013504. Springer, Heidelberg (2008)"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Demri, S., Sangnier, A.: When Model-Checking Freeze LTL over Counter Machines Becomes Decidable. Research report, LSV, ENS Cachan (2010)","DOI":"10.1007\/978-3-642-12032-9_13"},{"key":"13_CR17","first-page":"352","volume-title":"LICS 1999","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359. IEEE, Los Alamitos (1999)"},{"key":"13_CR18","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","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger accelerations: Applications to broadcast protocols. In: FST&TCS 2002. LNCS, vol.\u00a02256, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"13_CR19","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)"},{"issue":"2","key":"13_CR20","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics\u00a016(2), 285\u2013296 (1966)","journal-title":"Pacific Journal of Mathematics"},{"key":"13_CR21","first-page":"235","volume-title":"LICS 2009","author":"S. G\u00f6ller","year":"2009","unstructured":"G\u00f6ller, S., Mayr, R., To, A.: On the computational complexity of verifying one-counter processes. In: LICS 2009, pp. 235\u2013244. IEEE, Los Alamitos (2009)"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00215625","volume":"5","author":"V. Goranko","year":"1996","unstructured":"Goranko, V.: Hierarchies of modal and temporal logics with references pointers. Journal of Logic, Language, and Information\u00a05, 1\u201324 (1996)","journal-title":"Journal of Logic, Language, and Information"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-04081-8_25","volume-title":"CONCUR 2009 - Concurrency Theory","author":"C. Haase","year":"2009","unstructured":"Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in succinct and parametric one-counter automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol.\u00a05710, pp. 369\u2013383. Springer, Heidelberg (2009)"},{"issue":"2","key":"13_CR24","first-page":"253","volume":"106","author":"R. Howell","year":"1993","unstructured":"Howell, R., Jan\u010dar, P., Rosier, L.: Completeness results for single-path Petri nets. I&C\u00a0106(2), 253\u2013265 (1993)","journal-title":"I&C"},{"issue":"1","key":"13_CR25","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":"181","key":"13_CR26","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BF01744294","volume":"13","author":"O. Ibarra","year":"1979","unstructured":"Ibarra, O.: Restricted one-counter machines with undecidable universe problems. Mathematical Systems Theory\u00a013(181), 181\u2013186 (1979)","journal-title":"Mathematical Systems Theory"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-45678-3_22","volume-title":"Algorithms and Computation","author":"O. Ibarra","year":"2001","unstructured":"Ibarra, O., Dang, Z.: On removing the stack from reachability constructions. In: Eades, P., Takaoka, T. (eds.) ISAAC 2001. LNCS, vol.\u00a02223, pp. 244\u2013256. Springer, Heidelberg (2001)"},{"issue":"1","key":"13_CR28","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":"13_CR29","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"},{"key":"13_CR30","first-page":"147","volume-title":"TIME 2005","author":"A. Lisitsa","year":"2005","unstructured":"Lisitsa, A., Potapov, I.: Temporal logic with predicate \u03bb-abstraction. In: TIME 2005, pp. 147\u2013155. IEEE, Los Alamitos (2005)"},{"key":"13_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, Warsaw, pp. 92\u2013101 (1929)"},{"key":"13_CR32","unstructured":"Reutenauer, C.: The Mathematics of Petri nets. Masson and Prentice (1990)"},{"key":"13_CR33","unstructured":"Sangnier, A.: V\u00e9rification de syst\u00e8mes avec compteurs et pointeurs. Th\u00e8se de doctorat, LSV, ENS Cachan, France (2008)"},{"issue":"3","key":"13_CR34","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. JACM\u00a032(3), 733\u2013749 (1985)","journal-title":"JACM"},{"key":"13_CR35","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","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12032-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,28]],"date-time":"2020-05-28T23:38:21Z","timestamp":1590709101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12032-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120312","9783642120329"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12032-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}