AI 中文总结
本文研究关联加权模型计数（WMC）与概率模型检测（PMC）的形式关系，提出无环参数马尔可夫链到算术电路的映射及反向映射，实现二者间优化技术的迁移。
AI 中文摘要
加权模型计数（WMC）和概率模型检测（PMC）是两个成熟的框架，前者用于概率推理，后者传统上用于概率验证，不过近来也被应用于推理领域。然而，这两个框架之间的形式关联在很大程度上仍未被探索。本文为二者的关联奠定了基础：我们提出了（1）一种从无环参数马尔可夫链（pMCs）到算术电路（ACs）的映射，使得这类pMC中的可达性概率计算可以归约为对应AC上的加权模型计数问题；（2）一种从具有概率语义的算术电路子类映射回参数马尔可夫链的方法。我们详细阐述了WMC和PMC实体之间的对应关系，并讨论了我们的映射如何实现互模拟极小化等优化技术在两个框架间的迁移。
英文摘要
Weighted model counting (WMC) and probabilistic model checking (PMC) are two well- established frameworks that are independently developed, the former for probabilistic inference, the latter traditionally for probabilistic verification, though recently also applied to inference. The formal relationship between the two frameworks, however, remains largely unexplored. In this paper, we lay the foundations for how they relate: we present (1) a mapping from cycle- free parametric Markov chains (pMCs) to arithmetic circuits (ACs), enabling the reduction of reachability probability computations in such pMCs to a weighted model counting problem on the corresponding ACs, and (2) a mapping from a subclass of arithmetic circuits -- with probabilistic semantics -- back to parametric Markov chains. We propose a detailed correspondence between the entities of WMC and PMC, and discuss how our mappings enable transferring optimization techniques such as bisimulation minimization across the frameworks.
