We study the estimation problem for concurrent programs: given a bounded program $P$, estimate the number of Mazurkiewicz trace-equivalence classes induced by its interleavings. This quantity informs two practical questions for enumeration-based model checking: how long a model checking run is likely to take, and what fraction of the search space has been covered so far. We first show the counting problem is #P-hard even for restricted programs and, unless $P=NP$, inapproximable within any subexponential factor, ruling out efficient exact or randomized approximation algorithms. We give a Monte Carlo approach to obtain a poly-time unbiased estimator: we convert a stateless optimal DPOR algorithm into an unbiased estimator by viewing its exploration as a bounded-depth, bounded-width tree whose leaves are the maximal Mazurkiewicz traces. A classical estimator by Knuth, when run on this tree, yields an unbiased estimate. To control the variance, we apply stochastic enumeration by maintaining a small population of partial paths per depth whose evolution is coupled. We have implemented our estimator in the JMC model checker and evaluated it on shared-memory benchmarks. With modest budgets, our estimator yields stable estimates, typically within a 20% band, within a few hundred trials, even when the state space has $10^5$--$10^6$ classes. We also show how the same machinery estimates model-checking cost by weighting all explored graphs, not only complete traces. Our algorithms provide the first provable poly-time unbiased estimators for counting traces, a problem of considerable importance when allocating model checking resources.

翻译：我们研究并发程序的估计问题：给定一个有界程序 $P$，估计由其交错执行产生的Mazurkiewicz迹等价类数量。该数量为基于枚举的模型检查提供了两个实际问题的信息：模型检查运行可能持续的时间，以及当前已覆盖搜索空间的百分比。我们首先证明，即使对于受限程序，该计数问题也是#P-hard的，并且除非 $P=NP$，否则无法在次指数因子内近似，从而排除了高效的精确或随机近似算法。我们提出一种蒙特卡洛方法以获得多项式时间的无偏估计量：将无状态最优DPOR算法转化为无偏估计量，方法是将探索过程视为一棵有界深度、有界宽度的树，其叶子节点为最大Mazurkiewicz迹。在此树上应用Knuth的经典估计量可得到无偏估计。为控制方差，我们采用随机枚举，在每个深度维护一个规模较小的部分路径种群，并使其演化过程耦合。我们已在JMC模型检查器中实现了该估计量，并在共享内存基准测试上进行评估。即便状态空间包含$10^5$--$10^6$个等价类，在适度预算下，该估计量在数百次试验内可获得稳定估计，通常偏差在20%以内。我们还展示了相同机制如何通过对所有探索图（而非仅完整迹）进行加权来估计模型检查成本。我们的算法首次提供了可证明的多项式时间无偏迹计数估计量，这对分配模型检查资源具有重要实践意义。