paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Counting and Sampling Traces in Regular Languages

正则语言中的迹计数与采样
POPL 10(POPL)2026匹配度 2/10 · 论文属于自动机与并发程序形式化验证中的迹计数与采样,涉及偏序归约和模型检测,但不涉及用户核心的 LLM/Agent 与静态分析交叉、浮点程序分析或贝叶斯程序分析。引用 1 inbox
Alexis de Colnet, Kuldeep S. Meel, Umang Mathur
crossref: 2026-09-10

AI 速览

一句话:研究正则语言中 Mazurkiewicz 迹的计数与近似均匀采样,给出 #P 复杂度结果及 FPRAS/FPAUS 算法。

本文研究正则语言所触及的 Mazurkiewicz 迹的计数与采样问题。给定字母表、独立关系、以 m 状态有限自动机表示的正则语言 L 以及一元编码的 n,计数问题是求与第 n 层 L_n=L∩Σ^n 相交的迹数;采样问题要求从这些迹上近似均匀分布中抽取一个迹。该问题服务于基于偏序归约的有界模型检测和并发程序随机测试。作者证明:即使给定 DFA,计数问题也是 #P-hard,这与 DFA 词计数可在多项式时间求解形成鲜明对比;对 NFA 与 DFA,且无论 L 是否迹封闭,计数问题仍属于 #P。主要贡献是 FPRAS 和 FPAUS,可高概率地在指定精度内估计计数并近似均匀采样。

问题
给定正则语言 L(由有限自动机表示)与独立关系,统计或采样与 L 的第 n 层相交的 Mazurkiewicz 迹,用于偏序归约模型检测与并发程序测试。
方法
将迹计数与采样问题置于自动机和计数复杂性框架下分析,证明其 #P 复杂度,并设计随机近似计数与近似均匀采样算法。
评估
通过理论证明给出 #P-hard 下界、#P 成员性,以及 FPRAS 与 FPAUS 的正确性和复杂度保证;未报告实验评估。
原文摘要(Abstract)

In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes the alphabet Σ and an independence relation 𝕀 ⊆ Σ × Σ . The computational problems we address take as input a regular language L over Σ, presented as a finite automaton with m states, together with a natural number n (presented in unary). For the counting problem, the output is the number of Mazurkiewicz traces (induced by 𝕀) that intersect the n th slice L n = L ∩ Σ n , i.e., traces that have at least one linearization in L 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 a priori 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. We first show that the counting problem is #P-hard even when the automaton accepting the language L 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 L is trace-closed. Finally, our main contributions are a fully polynomial-time randomized approximation scheme (FPRAS) that, with high probability, estimates the desired count within a specified accuracy parameter, and a fully polynomial-time almost uniform sampler (FPAUS) that generates traces while ensuring that the distribution induced on them is approximately uniform with high probability.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{ColnetMM26,
  title = {Counting and Sampling Traces in Regular Languages},
  author = {Alexis de Colnet and Kuldeep S. Meel and Umang Mathur},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776723}
}