{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:18:19Z","timestamp":1781893099867,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544570","type":"print"},{"value":"9783662544587","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54458-7_12","type":"book-chapter","created":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T09:22:57Z","timestamp":1489569777000},"page":"196-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Logics of Repeating Values on Data Trees and Branching Counter Systems"],"prefix":"10.1007","author":[{"given":"Sergio","family":"Abriola","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Diego","family":"Figueira","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Figueira","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,16]]},"reference":[{"key":"12_CR1","unstructured":"Baelde, D., Lunel, S., Schmitz, S.: A sequent calculus for a modal logic on finite data trees. In: 25th EACSL Annual Conference on Computer Science Logic, CSL 29, 1 September 2016, Marseille, France, pp. 32:1\u201332:16, August 2016"},{"issue":"3","key":"12_CR2","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1516512.1516515","volume":"56","author":"M Boja\u0144czyk","year":"2009","unstructured":"Boja\u0144czyk, M., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and XML reasoning. JACM 56(3), 13 (2009)","journal-title":"JACM"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4) 2010","DOI":"10.1145\/1970398.1970403"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-28729-9_26","volume-title":"Foundations of Software Science and Computational Structures","author":"B Bollig","year":"2012","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Narayan Kumar, K.: Model checking languages of data words. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 391\u2013405. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28729-9_26"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-540-72734-7_13","volume-title":"Logical Foundations of Computer Science","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D., Gascon, R.: A decidable temporal logic of repeating values. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 180\u2013194. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-72734-7_13"},{"issue":"5","key":"12_CR6","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.1093\/logcom\/exr013","volume":"22","author":"S Demri","year":"2012","unstructured":"Demri, S., D\u2019Souza, D., Gascon, R.: Temporal logics of repeating values. J. Log. Comput. 22(5), 1059\u20131096 (2012)","journal-title":"J. Log. Comput."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Demri, S., Figueira, D., Praveen, M.: Reasoning about data repetitions with counter systems. In: LICS, pp. 33\u201342. IEEE Press (2013)","DOI":"10.1109\/LICS.2013.8"},{"issue":"1","key":"12_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.jcss.2012.04.002","volume":"79","author":"S Demri","year":"2013","unstructured":"Demri, S., Jurdzi\u0144ski, M., Lachish, O., Lazi\u0107, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79(1), 23\u201338 (2013)","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)","DOI":"10.1145\/1507244.1507246"},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. JACM 33(1), 151\u2013178 (1986)","journal-title":"JACM"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Figueira, D.: Forward-XPath and extended register automata on data-trees. In: ICDT. ACM (2010)","DOI":"10.1145\/1804669.1804699"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Figueira, D.: Alternating register automata on finite data words and trees. Log. Methods Comput. Sci. 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:22)2012"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Figueira, D.: Decidability of downward XPath. ACM Trans. Comput. Log. 13(4) (2012)","DOI":"10.1145\/2362355.2362362"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Figueira, D.: On XPath with transitive axes and data tests. In: PODS, pp. 249\u2013260. ACM (2013)","DOI":"10.1145\/2463664.2463675"},{"key":"12_CR15","unstructured":"Figueira, D., Figueira, S., Areces, C.: Basic model theory of XPath on data trees. In: ICDT, pp. 50\u201360. ACM (2014)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Figueira, D., Libkin, L.: Pattern logics and auxiliary relations. In: CSL-LICS, pp. 40:1\u201340:10 (2014)","DOI":"10.1145\/2603088.2603136"},{"key":"12_CR17","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. 5734, pp. 331\u2013343. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03816-7_29"},{"key":"12_CR18","unstructured":"Figueira, D., Segoufin, L.: Bottom-up automata on data trees and vertical XPath. In: STACS, vol. 9 of LIPIcs, pp. 93\u2013104. LZI (2011)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Jacquemard, F., Segoufin, L., Dimino, J.: $$\\text{FO2}(< +1, \\sim )$$ on data trees, data tree automata and branching vector addition systems. Log. Methods Comput. Sci. 12(2) (2016)","DOI":"10.2168\/LMCS-12(2:3)2016"},{"issue":"3","key":"12_CR20","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/1929954.1929956","volume":"12","author":"M Jurdzi\u0144ski","year":"2011","unstructured":"Jurdzi\u0144ski, M., Lazi\u0107, R.: Alternating automata on data trees and XPath satisfiability. ACM Trans. Comput. Log. 12(3), 19 (2011)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR21","unstructured":"Kara, A., Schwentick, T., Zeume, T.: Temporal logics on words with multiple data values. In: FST & TCS (2010)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Memoryful branching-time logic. In: LICS, pp. 265\u2013274. IEEE Press (2006)","DOI":"10.1109\/LICS.2006.34"},{"issue":"3","key":"12_CR23","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/2733375","volume":"16","author":"R Lazi\u0107","year":"2015","unstructured":"Lazi\u0107, R., Sylvain, S.: Nonelementary complexities for branching VASS, MELL, and extensions. ACM Trans. Comput. Log. 16(3), 20 (2015)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Lisitsa, A., Potapov, I.: Temporal logic with predicate $$\\lambda $$-abstraction. In: TIME, pp. 147\u2013155. IEEE Press (2005)","DOI":"10.1109\/TIME.2005.34"},{"issue":"3","key":"12_CR25","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"12_CR27","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoret. Comput. Sci. 6(2), 223\u2013231 (1978)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/11874683_3","volume-title":"Computer Science Logic","author":"L Segoufin","year":"2006","unstructured":"Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41\u201357. Springer, Heidelberg (2006). doi:10.1007\/11874683_3"},{"issue":"1","key":"12_CR29","first-page":"217","volume":"7","author":"KN Verma","year":"2005","unstructured":"Verma, K.N., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Discrete Math. Theor. Comput. Sci. 7(1), 217\u2013230 (2005)","journal-title":"Discrete Math. Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54458-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:22:38Z","timestamp":1750108958000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544570","9783662544587"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54458-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2017","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":"fossacs2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}