{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:53:30Z","timestamp":1767920010138,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes the alphabet \u03a3 and an independence relation I \u2286 \u03a3 \u00d7 \u03a3. The computational problems we address take as input a regular language\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    over \u03a3, presented as a finite automaton with\n                    <jats:italic toggle=\"yes\">m<\/jats:italic>\n                    states, together with a natural number\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    (presented in unary). For the counting problem, the output is the number of Mazurkiewicz\n                    <jats:italic toggle=\"yes\">traces<\/jats:italic>\n                    (induced by I) that intersect the\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <jats:sup>\n                      <jats:italic toggle=\"yes\">th<\/jats:italic>\n                    <\/jats:sup>\n                    slice\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    <jats:sub>\n                      <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <\/jats:sub>\n                    =\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    \u2229 \u03a3\n                    <jats:sup>\n                      <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <\/jats:sup>\n                    of\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    , i.e., traces that have at least one linearization in\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    <jats:sub>\n                      <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <\/jats:sub>\n                    . For the sampling problem, the output is a trace drawn from a distribution that is approximately uniform over all such traces. These problems are motivated by applications such as bounded model checking based on partial-order reduction, where an\n                    <jats:italic toggle=\"yes\">a priori<\/jats:italic>\n                    estimate of the size of the state space can significantly improve usability, as well as testing approaches for concurrent programs that use partial-order-aware random sampling, where uniform exploration is desirable for effective bug detection.\n                  <\/jats:p>\n                  <jats:p>\n                    We first show that the counting problem is #P-hard even when the automaton accepting the language\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    is deterministic, which is in sharp contrast to the corresponding problem for counting the words of a DFA, which is solvable in polynomial time. We then show that the counting problem remains in the class #P for both NFAs and DFAs, independent of whether\n                    <jats:italic toggle=\"yes\">L<\/jats:italic>\n                    is trace-closed. Finally, our main contributions are a\n                    <jats:italic toggle=\"yes\">fully polynomial-time randomized approximation scheme<\/jats:italic>\n                    (FPRAS) that, with high probability, estimates the desired count within a specified accuracy parameter, and a\n                    <jats:italic toggle=\"yes\">fully polynomial-time almost uniform sampler<\/jats:italic>\n                    (FPAUS) that generates traces while ensuring that the distribution induced on them is approximately uniform with high probability.\n                  <\/jats:p>","DOI":"10.1145\/3776723","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2352-2379","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Counting and Sampling Traces in Regular Languages"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7517-6735","authenticated-orcid":false,"given":"Alexis","family":"de Colnet","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9423-5270","authenticated-orcid":false,"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the ACM on Programming Languages, 8, POPL","author":"Ang Zhendong","year":"2024","unstructured":"Zhendong Ang and Umang Mathur. 2024. Predictive Monitoring against Pattern Regular Languages. Proceedings of the ACM on Programming Languages, 8, POPL (2024), 2191\u20132225."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3294052.3319704"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477045"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90051-5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213042"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_2_1_10_1","unstructured":"Alexis de Colnet Kuldeep S. Meel and Umang Mathur. 2025. Counting and Sampling Traces in Regular Languages. arxiv:2512.00314. arxiv:2512.00314"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Volker Diekert and Grzegorz Rozenberg. 1995. The book of traces. World scientific.","DOI":"10.1142\/9789814261456"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632873"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90174-X"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_4"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616268"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_5"},{"key":"e_1_2_1_22_1","volume-title":"Advances in Petri Nets","author":"Mazurkiewicz A","year":"1986","unstructured":"A Mazurkiewicz. 1987. Trace Theory. In Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency. Springer-Verlag New York, Inc., 279\u2013324."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3651613"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICDT.2025.30"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3725253"},{"key":"e_1_2_1_26_1","volume-title":"Introduction to Choreographies","author":"Montesi Fabrizio","unstructured":"Fabrizio Montesi. 2023. Introduction to Choreographies. Cambridge University Press."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360606"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510227"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321679"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640389"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707214"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90252-O"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776723","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:02:37Z","timestamp":1767898957000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776723"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776723"],"URL":"https:\/\/doi.org\/10.1145\/3776723","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}