{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:15Z","timestamp":1751662875712,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,11,22]],"date-time":"2021-11-22T00:00:00Z","timestamp":1637539200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2022,1,31]]},"abstract":"<jats:p>\n            We study decidability problems for equivalence of probabilistic programs for a core probabilistic programming language over finite fields of fixed characteristic. The programming language supports uniform sampling, addition, multiplication, and conditionals and thus is sufficiently expressive to encode Boolean and arithmetic circuits. We consider two variants of equivalence: The first one considers an interpretation over the finite field\n            <jats:bold>F<\/jats:bold>\n            <jats:italic>\n              <jats:sub>q<\/jats:sub>\n            <\/jats:italic>\n            , while the second one, which we call universal equivalence, verifies equivalence over all extensions\n            <jats:bold>F<\/jats:bold>\n            <jats:italic>\n              <jats:sub>q<\/jats:sub>\n              <jats:sup>k<\/jats:sup>\n            <\/jats:italic>\n            of\n            <jats:bold>F<\/jats:bold>\n            <jats:italic>\n              <jats:sub>q<\/jats:sub>\n            <\/jats:italic>\n            . The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of\n            <jats:bold>F<\/jats:bold>\n            <jats:italic>\n              <jats:sub>2<\/jats:sub>\n              <jats:sup>k<\/jats:sup>\n            <\/jats:italic>\n            for any\n            <jats:italic>k<\/jats:italic>\n            . While the first problem is obviously decidable, we establish its exact complexity, which lies in the counting hierarchy. To show decidability and a doubly exponential upper bound of the universal variant, we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. We then devise a general way to draw links between the universal probabilistic problems and widely studied problems on linear recurrence sequences. Finally, we study several variants of the equivalence problem, including a problem we call majority, motivated by differential privacy. We also define and provide some insights about program indistinguishability, proving that it is decidable for programs always returning 0 or 1.\n          <\/jats:p>","DOI":"10.1145\/3487063","type":"journal-article","created":{"date-parts":[[2021,11,22]],"date-time":"2021-11-22T17:43:55Z","timestamp":1637603035000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Universal Equivalence and Majority of Probabilistic Programs over Finite Fields"],"prefix":"10.1145","volume":"23","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI-SP &amp; IMDEA Software Institute, Bochum, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charlie","family":"Jacomme","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[{"name":"LORIA, Inria Nancy-Grand Est &amp; CNRS &amp; Universit\u00e9 de Lorraine, Villers l\u00e9s Nancy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,11,22]]},"reference":[{"key":"e_1_3_3_2_2","series-title":"29th International Conference on Concurrency Theory (CONCUR\u201918)","first-page":"42:1\u201342:15","volume":"118","author":"Almagor Shaull","year":"2018","unstructured":"Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Jo\u00ebl Ouaknine, and James Worrell. 2018. Effective divergence analysis for linear recurrence sequences. In 29th International Conference on Concurrency Theory (CONCUR\u201918)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 118), Sven Schewe and Lijun Zhang (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 42:1\u201342:15. DOI: https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.42"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.2307\/1970573"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394796"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939145"},{"key":"e_1_3_3_6_2","first-page":"136","volume-title":"32nd IEEE Computer Security Foundations Symposium (CSF\u201919)","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, Charlie Jacomme, Steve Kremer, and Pierre-Yves Strub. 2019. Symbolic methods in computational cryptography proofs. In 32nd IEEE Computer Security Foundations Symposium (CSF\u201919). IEEE Computer Society, 136\u2013151."},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480894"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394746"},{"key":"e_1_3_3_9_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-319-89884-1_6","volume-title":"27th European Symposium on Programming (ESOP\u201918)","author":"Bichsel Benjamin","year":"2018","unstructured":"Benjamin Bichsel, Timon Gehr, and Martin Vechev. 2018. Fine-grained semantics for probabilistic programs. In 27th European Symposium on Programming (ESOP\u201918)(Lecture Notes in Computer Science, Vol. 10801). Springer, 145\u2013185."},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01609477"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53015-3_15"},{"key":"e_1_3_3_13_2","unstructured":"Antoine Chambert-Loir. 2006. Compter (rapidement) le nombre de solutions d\u2019\u00e9quations dans les corps finis. https:\/\/arxiv.org\/abs\/math\/0611584."},{"key":"e_1_3_3_14_2","unstructured":"Qi Cheng J. Maurice Rojas and Daqing Wan. 2020. Computing zeta functions of large polynomial systems over finite fields. arxiv:2007.13214 [math.NT]."},{"key":"e_1_3_3_15_2","volume-title":"30th International Conference on Concurrency Theory (CONCUR\u201919)","author":"Chistikov Dmitry","year":"2019","unstructured":"Dmitry Chistikov, Andrzej S. Murawski, and David Purser. 2019. Asymmetric distances for approximate differential privacy. In 30th International Conference on Concurrency Theory (CONCUR\u201919). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.55"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.2307\/2372974"},{"key":"e_1_3_3_18_2","unstructured":"Graham Everest Alf van der Poorten Igor Shparlinski and Thomas Ward. 2002. Exponential functions linear recurrence sequences and their applications. (2002). https:\/\/www.ams.org\/books\/surv\/104\/."},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603097"},{"key":"e_1_3_3_20_2","series-title":"47th International Colloquium on Automata, Languages, and Programming (ICALP\u201920)","first-page":"129:1\u2013129:17","volume":"168","author":"Gaboardi Marco","year":"2020","unstructured":"Marco Gaboardi, Kobbi Nissim, and David Purser. 2020. The complexity of verifying loop-free programs as differentially private. In 47th International Colloquium on Automata, Languages, and Programming (ICALP\u201920)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 168), Artur Czumaj, Anuj Dawar, and Emanuela Merelli (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 129:1\u2013129:17. DOI: https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2020.129"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1561\/0400000001"},{"key":"e_1_3_3_22_2","unstructured":"William Andrew Johnson. 2016. Fun with Fields . Ph.D. Dissertation. UC Berkeley."},{"key":"e_1_3_3_23_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/978-3-642-33167-1_33","volume-title":"17th European Symposium on Research in Computer Security (ESORICS\u201912)","author":"Jutla Charanjit S.","year":"2012","unstructured":"Charanjit S. Jutla and Arnab Roy. 2012. Decision procedures for simulatability. In 17th European Symposium on Research in Computer Security (ESORICS\u201912)(Lecture Notes in Computer Science, Vol. 7459). Springer, 573\u2013590."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1976-0422281-1"},{"key":"e_1_3_3_25_2","first-page":"579","volume-title":"Algorithmic Number Theory: Lattices, Number Fields, Curves and Cryptography","author":"Lauder Alan G. B.","year":"2008","unstructured":"Alan G. B. Lauder and Daqing Wan. 2008. Counting points on varieties over finite fields of small characteristic. In Algorithmic Number Theory: Lattices, Number Fields, Curves and Cryptography. Cambridge University Press, 579\u2013612."},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792752"},{"key":"e_1_3_3_27_2","volume-title":"Finite Fields","author":"Lidl Rudolf","year":"1983","unstructured":"Rudolf Lidl and Harald Niederreiter. 1983. Finite Fields. Addison-Wesley."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57048-8_6"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/1622797.1622798"},{"key":"e_1_3_3_30_2","first-page":"343","article-title":"Polynomial automorphisms over finite fields","volume":"27","author":"Maubach Stefan","year":"2001","unstructured":"Stefan Maubach. 2001. Polynomial automorphisms over finite fields. Serdica Math. J. 27 (2001), 343\u2013350.","journal-title":"Serdica Math. J."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2011.08.004"},{"issue":"349","key":"e_1_3_3_32_2","first-page":"63","article-title":"The distance between terms of an algebraic recurrence sequence","author":"Mignotte Maurice","year":"1984","unstructured":"Maurice Mignotte, Tarlok Nath Shorey, and Robert Tijdeman. 1984. The distance between terms of an algebraic recurrence sequence. J. F\u00fcr Die Reine Und Angewandte Mathematik349 (1984), 63\u201376.","journal-title":"J. F\u00fcr Die Reine Und Angewandte Mathematik"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/2555843"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_15"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/96559.96569"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/2406808.2406811"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/2634074.2634101"},{"key":"e_1_3_3_38_2","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1007\/978-3-662-43951-7_28","volume-title":"International Colloquium on Automata, Languages, and Programming","author":"Ouaknine Jo\u00ebl","year":"2014","unstructured":"Jo\u00ebl Ouaknine and James Worrell. 2014. Ultimate positivity is decidable for simple linear recurrence sequences. In International Colloquium on Automata, Languages, and Programming. Springer, 330\u2013341."},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/359168.359176"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/SCT.1988.5281"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/116825.116858"},{"issue":"2","key":"e_1_3_3_42_2","first-page":"609","article-title":"The problem of appearance of a zero in a linear recurrence sequence","volume":"38","author":"Vereshchagin N. K.","year":"1985","unstructured":"N. K. Vereshchagin. 1985. The problem of appearance of a zero in a linear recurrence sequence. Mat. Zametki 38, 2 (1985), 609\u2013615.","journal-title":"Mat. Zametki"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1949-09219-4"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487063","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3487063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:09Z","timestamp":1750183809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487063"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,22]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,1,31]]}},"alternative-id":["10.1145\/3487063"],"URL":"https:\/\/doi.org\/10.1145\/3487063","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,11,22]]},"assertion":[{"value":"2020-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}