{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T13:43:25Z","timestamp":1790343805292,"version":"4.1.0"},"reference-count":31,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"4","funder":[{"name":"Taiwan National Science and Technology Council","award":["109-2221-E-002-143-MY3"],"award-info":[{"award-number":["109-2221-E-002-143-MY3"]}]},{"DOI":"10.13039\/501100006477","name":"National Taiwan University","doi-asserted-by":"publisher","award":["109L891808"],"award-info":[{"award-number":["109L891808"]}],"id":[{"id":"10.13039\/501100006477","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T022124\/1"],"award-info":[{"award-number":["EP\/T022124\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Comput."],"published-print":{"date-parts":[[2024,8,31]]},"abstract":"<jats:p>Abstract.<\/jats:p>\n                  <jats:p>We consider the extension of [Formula: see text] with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence, i.e., the set of the sizes of its finite models, is definable in Presburger arithmetic. In the process we present several refinements to the \u201cbiregular graph method.\u201d In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.<\/jats:p>","DOI":"10.1137\/22m1504792","type":"journal-article","created":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T04:01:26Z","timestamp":1720411286000},"page":"884-968","source":"Crossref","is-referenced-by-count":1,"title":["Two Variable Logic with Ultimately Periodic Counting"],"prefix":"10.1137","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-0880","authenticated-orcid":true,"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, England."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Egor V.","family":"Kostylev","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tony","family":"Tan","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, England."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_3"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.09.028"},{"key":"ref3","doi-asserted-by":"crossref","unstructured":"B. Bednarczyk, F. Baader, and S. Rudolph, Satisfiability and query answering in description logics with global and local cardinality constraints, in 24th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2020, pp. 616\u2013623.","DOI":"10.3233\/FAIA200146"},{"key":"ref4","unstructured":"B. Bednarczyk, M. Orlowska, A. Pacanowska, and T. Tan, On classical decidable logics extended with percentage quantifiers and arithmetics, in 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs Leibniz Int. Proc. Inform. 213, Wadern, Germany, 2021, 36."},{"key":"ref5","unstructured":"M. Benedikt, E. Kostylev, and T. Tan, Two variable logice with ultimately periodic counting, in 47th International Colloquium on Automata, Languages, and Programming, LIPIcs Leibniz Int. Proc. Inform. 168, Wadern, Germany, 2020, 112."},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1976-0396605-3"},{"key":"ref7","first-page":"73","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Charatonik W.","year":"2013"},{"key":"ref8","volume":"12","author":"Charatonik W.","year":"2016","journal-title":"Log. Methods Comput. Sci."},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2983622"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2010.03.001"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.2178\/bsl.1804020"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.09.008"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1966.16.285"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"key":"ref15","doi-asserted-by":"crossref","unstructured":"E. Gr\u00e4del, M. Otto, and E. Rosen, Two-variable logic with counting is decidable, in 12th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Los Alamitos, CA, 1997, pp. 306\u2013317.","DOI":"10.1109\/LICS.1997.614957"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050130"},{"key":"ref17","doi-asserted-by":"crossref","unstructured":"Y. Gurevich and S. Shelah, Spectra of monadic second-order formulas with one unary function, in 12th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Los Alamitos, CA, 2003, pp. 291\u2013300.","DOI":"10.1109\/LICS.2003.1210069"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1137\/120900095"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1137\/130943625"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1996.12004747"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797323005"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-005-5791-1"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl034"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.02.004"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13824-9_4"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201400102"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780192867964.001.0001"},{"key":"ref31","volume":"27","author":"Scott D.","year":"1962","journal-title":"J. Symb. Log."}],"container-title":["SIAM Journal on Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/22M1504792","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T19:11:57Z","timestamp":1787339517000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/22M1504792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,8,31]]}},"alternative-id":["10.1137\/22M1504792"],"URL":"https:\/\/doi.org\/10.1137\/22m1504792","relation":{},"ISSN":["0097-5397","1095-7111"],"issn-type":[{"value":"0097-5397","type":"print"},{"value":"1095-7111","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,8]]}}}