{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:20:15Z","timestamp":1760080815275,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308284"},{"type":"electronic","value":"9783031308291"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T00:00:00Z","timestamp":1682035200000},"content-version":"vor","delay-in-days":110,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents a similar approach for existential first-order characterizations of the languages recognizable by finite automata, by Parikh automata, and by multi-counter machines over the alphabet <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\left\\{ 0,1,...,k-1\\right\\} ^{n}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:msup>\n                  <mml:mfenced>\n                    <mml:mn>0<\/mml:mn>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mn>1<\/mml:mn>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mo>.<\/mml:mo>\n                    <mml:mo>.<\/mml:mo>\n                    <mml:mo>.<\/mml:mo>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>k<\/mml:mi>\n                    <mml:mo>-<\/mml:mo>\n                    <mml:mn>1<\/mml:mn>\n                  <\/mml:mfenced>\n                  <mml:mi>n<\/mml:mi>\n                <\/mml:msup>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula> for some <jats:inline-formula><jats:alternatives><jats:tex-math>$$k\\ge 2$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mi>k<\/mml:mi>\n                  <mml:mo>\u2265<\/mml:mo>\n                  <mml:mn>2<\/mml:mn>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. The set of <jats:italic>k<\/jats:italic>-FA-recognizable relations coincides with the set of relations, which are existentially definable in the structure \n\"Image missing\"\n, where \n\"Image missing\"\n corresponds to the bitwise minimum of base <jats:italic>k<\/jats:italic>. In order to obtain an existential first-order description of <jats:italic>k<\/jats:italic>-Parikh automata languages, we extend this structure with the predicate <jats:inline-formula><jats:alternatives><jats:tex-math>$$ EqNZB _{k}(x,y)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mi>E<\/mml:mi>\n                  <mml:mi>q<\/mml:mi>\n                  <mml:mi>N<\/mml:mi>\n                  <mml:mi>Z<\/mml:mi>\n                  <mml:msub>\n                    <mml:mi>B<\/mml:mi>\n                    <mml:mi>k<\/mml:mi>\n                  <\/mml:msub>\n                  <mml:mrow>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>x<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>y<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula> which is true if and only if <jats:italic>x<\/jats:italic> and <jats:italic>y<\/jats:italic> have the same number of non-zero bits in <jats:italic>k<\/jats:italic>-ary encoding. Using essentially the same ideas, we encode computations of <jats:italic>k<\/jats:italic>-multi-counter machines and thus show that every recursively enumerable relation over the natural numbers is existentially definable in the aforementioned structure supplemented with concatenation <jats:inline-formula><jats:alternatives><jats:tex-math>$$z=x\\smallfrown _{k} y\\rightleftharpoons z = x + k^{l_{k}(x)}y$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mi>z<\/mml:mi>\n                  <mml:mo>=<\/mml:mo>\n                  <mml:mi>x<\/mml:mi>\n                  <mml:msub>\n                    <mml:mo>\u2322<\/mml:mo>\n                    <mml:mi>k<\/mml:mi>\n                  <\/mml:msub>\n                  <mml:mi>y<\/mml:mi>\n                  <mml:mo>\u21cc<\/mml:mo>\n                  <mml:mi>z<\/mml:mi>\n                  <mml:mo>=<\/mml:mo>\n                  <mml:mi>x<\/mml:mi>\n                  <mml:mo>+<\/mml:mo>\n                  <mml:msup>\n                    <mml:mi>k<\/mml:mi>\n                    <mml:mrow>\n                      <mml:msub>\n                        <mml:mi>l<\/mml:mi>\n                        <mml:mi>k<\/mml:mi>\n                      <\/mml:msub>\n                      <mml:mrow>\n                        <mml:mo>(<\/mml:mo>\n                        <mml:mi>x<\/mml:mi>\n                        <mml:mo>)<\/mml:mo>\n                      <\/mml:mrow>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                  <mml:mi>y<\/mml:mi>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, where <jats:inline-formula><jats:alternatives><jats:tex-math>$$l_{k}(x)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:msub>\n                    <mml:mi>l<\/mml:mi>\n                    <mml:mi>k<\/mml:mi>\n                  <\/mml:msub>\n                  <mml:mrow>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>x<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is the bit-length of <jats:italic>x<\/jats:italic> in base <jats:italic>k<\/jats:italic>. This result gives us another proof of DPR-theorem.<\/jats:p>","DOI":"10.1007\/978-3-031-30829-1_9","type":"book-chapter","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:56:19Z","timestamp":1682020579000},"page":"176-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On the Existential Arithmetics with Addition and Bitwise Minimum"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2288-9483","authenticated-orcid":false,"given":"Mikhail R.","family":"Starchak","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,21]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"B\u00e8s, A.: Undecidable extensions of B\u00fcchi arithmetic and Cobham-Sem\u00ebnov theorem. Journal of Symbolic Logic 62(4), 1280\u20131296 (1997). https:\/\/doi.org\/10.2307\/2275643","DOI":"10.2307\/2275643"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"B\u00e8s, A.: Expansions of MSO by cardinality relations. Logical Methods in Computer Science 9(4) (2013). https:\/\/doi.org\/10.2168\/lmcs-9(4:18)2013","DOI":"10.2168\/lmcs-9(4:18)2013"},{"key":"9_CR3","unstructured":"Bruy\u00e8re V.: Entiers et automates finis. M\u00e9moire de fin d\u2019\u00e9tudes, University of Mons, Belgium (1985)"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Bruy\u00e8re V., Hansel G., Michaux C., Villemaire R.: Logic and $$p$$-recognizable sets of integers. Bulletin of the Belgian Mathematical Society - Simon Stevin 1(2), 191\u2013238 (1994). https:\/\/doi.org\/10.36045\/bbms\/1103408547","DOI":"10.36045\/bbms\/1103408547"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"B\u00fcchi R.J.: Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly 6(1-6), 66\u201392 (1960). https:\/\/doi.org\/10.1002\/malq.19600060105","DOI":"10.1002\/malq.19600060105"},{"key":"9_CR6","unstructured":"Cadilhac M., Finkel A., McKenzie P.: On the expressiveness of Parikh automata and related models. In: Proceedings of the Third Workshop on Non-Classical Models for Automata and Applications - NCMA 2011, pp. 103\u2013119. Milan, Italy (2011)"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Davis M.: Arithmetical problems and recursively enumerable predicates. Journal of Symbolic Logic 18(1), 33\u201341 (1953). https:\/\/doi.org\/10.2307\/2266325","DOI":"10.2307\/2266325"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Davis M., Putnam H., Robinson J.: The decision problem for exponential diophantine equations. Annals of Mathematics 74(3), 425\u2013436 (1961). https:\/\/doi.org\/10.2307\/1970289","DOI":"10.2307\/1970289"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Elgot C.C.: Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society 98(1), 21\u201351 (1961).https:\/\/doi.org\/10.1090\/s0002-9947-1961-0139530-9","DOI":"10.1090\/s0002-9947-1961-0139530-9"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Ginsburg S., Spanier E.: Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics 16(2), 285\u2013296 (1966). https:\/\/doi.org\/10.2140\/pjm.1966.16.285","DOI":"10.2140\/pjm.1966.16.285"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Haase C., R\u00f3\u017cycki J.: On the expressiveness of B\u00fcchi arithmetic. In: Kiefer, S., Tasson, C. (eds) FOSSACS 2021, Lecture Notes in Computer Science, vol. 12650, pp. 310\u2013323. Springer International Publishing (2021). https:\/\/doi.org\/10.1007\/978-3-030-71995-1_16","DOI":"10.1007\/978-3-030-71995-1_16"},{"key":"9_CR12","unstructured":"Hodgson B.R.: D\u00e9cidabilit\u00e9 par automate fini. Annales des sciences math\u00e9matiques du Qu\u00e9bec, 7(1), 39\u201357 (1983)."},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Ibarra O.H.: Reversal-bounded multicounter machines and their decision problems. Journal of the ACM 25(1), 116\u2013133 (1978). https:\/\/doi.org\/10.1145\/322047.322058","DOI":"10.1145\/322047.322058"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Jones J.P., Matijasevi\u010d Yu.V.: Register machine proof of the theorem on exponential diophantine representation of enumerable sets. Journal of Symbolic Logic 49(3), 818\u2013829 (1984). https:\/\/doi.org\/10.2307\/2274135","DOI":"10.2307\/2274135"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Klaedtke F., Rue\u00df H.: Parikh automata and monadic second-order logics with linear cardinality constraints. Tech. rep. 177, Universit\u00e4t Freiburg (2002)","DOI":"10.1007\/3-540-45061-0_54"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Klaedtke F., Rue\u00df H.: Monadic second-order logics with cardinalities. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds) ICALP 2003, Lecture Notes in Computer Science, vol. 2719, pp. 681\u2013696. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_54.","DOI":"10.1007\/3-540-45061-0_54."},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Kozen D.C.: Automata and Computability. Springer, New York (1997). https:\/\/doi.org\/10.1007\/978-1-4612-1844-9","DOI":"10.1007\/978-1-4612-1844-9"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Kummer E.E.: \u00dcber die Erg\u00e4nzungss\u00e4tze zu den allgemeinen Reciprocit\u00e4tsgesetzen. Journal f\u00fcr die reine und angewandte Mathematik, 44, 93\u2013146 (1852).https:\/\/doi.org\/10.1515\/crll.1852.44.93","DOI":"10.1515\/crll.1852.44.93"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Matiyasevich Yu.V.: A new proof of the theorem on exponential diophantine representation of enumerable sets (in Russian). Zapiski Nauchnykh Seminarov LOMI 60, 75\u201392 (1976). (English translation: Journal of Soviet Mathematics 14(5), 1475\u20131486 (1980) https:\/\/doi.org\/10.1007\/BF01693980)","DOI":"10.1007\/BF01693980"},{"key":"9_CR20","unstructured":"Matiyasevich Yu.V.: Hilbert\u2019s tenth problem. MIT Press, Massachusetts (1993)"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Parikh R.J.: On context-free languages. Journal of the ACM 13(4) 570\u2013581 (1966). https:\/\/doi.org\/10.1145\/321356.321364","DOI":"10.1145\/321356.321364"},{"key":"9_CR22","unstructured":"Trakhtenbrot B.A.: Finite automata and the logic of one-place predicates (in Russian). Sibirski\u012d Matematicheski\u012d Zhurnal 3, 103\u2013131 (1962)."},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Villemaire R.: Joining $$k$$- and $$l$$-recognizable sets of natural numbers. In: Finkel, A., Jantzen, M. (eds) STACS 1992, Lecture Notes in Computer Science, vol. 577, pp. 83\u201394. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55210-3_175","DOI":"10.1007\/3-540-55210-3_175"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Villemaire R.: The theory of $$\\left\\langle \\mathbb{N};+,V_{k},V_{l}\\right\\rangle $$ is undecidable. Theoretical Computer Science 106(2), 337\u2013349 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90256-f","DOI":"10.1016\/0304-3975(92)90256-f"}],"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-031-30829-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:57:48Z","timestamp":1682020668000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30829-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308284","9783031308291"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30829-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}