这个问题是关于如何为符号模型检查器生成符号状态空间。首先，我介绍了一些让我想为 MDD 做这件事的背景，然后我更详细地解释了这个问题。
Edmund M. Clarke（模型检查的创始人之一）的本次讲座介绍了符号模型检查。它说“工业强度”模型检查器使用布尔编码（二进制决策图，或 BDD）来处理状态爆炸问题。但是，它只允许比常规模型检查多一个数量级的状态。我跳过了常规的模型检查，它直接构建程序 b/c 的状态转换图，我可以想象这立即是不切实际的。
我看过一些描述优于 BDD 质量的论文，例如处理更多状态1（避免？！状态空间爆炸问题），一般加速2（有界模型检查），使用状态匹配技术来限制状态空间搜索（超出有界模型检查）3，并使用 MDD，其执行速度比现有 BDD[4][5] 快几个数量级。
BDD将平均支持的状态数从大约 10^6 提高到 10^20。那篇论文还说：
不幸的是，众所周知，符号技术不适用于异步系统，例如通信协议，这些系统尤其受到状态空间爆炸的影响。
因此，MDD 甚至 EDD 似乎是模型检查的更好选择。还有边值 BDD (EVBDD)。但是我的问题是，如何为 ~MDD（或任何一个最好的）构建符号状态空间。本文档介绍了它，但似乎没有解释如何实际生成它。他们说：
我们使用准约简、有序、非负边值、多值决策图。
想知道是否可以从高层次上解释 MDD 的状态空间生成算法，以及系统中涉及的数据结构是什么，例如node对象的属性是什么（如 C 结构）。我在想，如果我能看到数据结构的总体情况以及算法的大致工作原理，那将足以实现。
另外，我不确定初始程序和规范需要做什么。因此，如果解释可以快速描述/介绍如何生成任何中间对象，那将是有帮助的。添加这个是因为我在一篇论文中看到他们有 Petri 网形式的程序，然后他们将其转换为 MDD，我不确定如何将程序转换为 Petri 网，或者是否有必要。基本上，如何从源代码到高级别的 MDD。
我认为这张图片是状态空间生成的算法，但我一直难以理解它的细节。具体来说，涉及的数据结构，以及“状态”的来源，即这些是来自其他模型的布尔谓词还是什么。
这个似乎也很接近：
以下是同一篇论文的更多内容：
(1)在本文中，我们展示了布尔决策过程，如 Stalmarck 方法 [16] 或 Davis & Putnam 过程 [7]，如何替代 BDD。这种新技术避免了 BDD 的空间爆炸，更快地生成反例，有时还加快了验证速度。
(2)本文的主要结果是在检查有时间限制的直到公式的时间复杂度上提高了 O(N)，其中 N 是所考虑的 CTMC 中的状态数。
(3)我们在之前的工作的基础上提出了符号执行和模型检查的组合，用于分析具有复杂输入的程序 [14,19]。在这项工作中，我们限制了输入大小和（或）模型检查器的搜索深度。在这里，我们超越了有界模型检查，我们研究了状态匹配技术来限制状态空间搜索。我们提出了一种检查符号状态何时被另一个符号状态包含的技术。
(4)我们提出了一种使用多值决策图生成异步系统状态空间的新算法。与相关工作相比，我们将系统的下一个{状态函数编码为单个布尔函数，而是作为整数函数的叉积。这允许应用各种迭代策略来构建系统的状态空间。特别是，我们引入了一种新的优雅策略，称为饱和度，并在工具 SMART 中实现它。除了通常比现有的基于 BDD 的状态空间生成器快几个数量级之外，我们的算法所需的峰值内存通常接近存储整个状态空间所需的最终内存。
(5)基于二进制决策图 (BDD) 的符号技术被广泛用于推理硬件电路和同步控制器的时间特性。然而，它们在处理基于交错语义的巨大状态空间底层系统时，通常表现不佳，例如通信协议和分布式软件，它们由通过共享事件进行通信的独立行动子系统组成......本文展示了通过利用许多基于事件和基于组件的系统模型的交错语义，可以极大地改进使用决策图的状态空间探索技术。
越来越接近这个：
可达状态空间 X_reach 可以表征为不动点方程 X ⊆ X_init ∪ T(X) 的最小解。算法
Bfs正是实现了这种固定点计算，其中集合和关系分别使用 L 级和 2L 级 MDD 存储，即节点 p 编码具有特征函数 v_p 的集合 X_p 满足v_p(i_L,...,i_1) = 1 ⇔ (i_L,...,i_1) ∈ X_p。
集合的并集通过对它们的特征函数应用 Or 运算符来简单地实现，而一步可达状态的计算通过使用函数 RelProd 来实现（当然，如果使用 MDD，则必须使用这些函数的 MDD 版本而不是 BDD）。由于它执行广度优先的符号搜索，算法 Bfs 停止的迭代次数与任何可达状态与初始状态的最大距离一样多。
mdd Bfs(mdd Xinit) is
local mdd p;
p ← Xinit;
repeat
p ← Or(p, RelProd(p, T ));
until p does not change;
return p;
bdd Or(bdd a, bdd b) is
local bdd r, r0, r1;
local level k;
if a = 0 or b = 1 then return b;
if b = 0 or a = 1 then return a;
if a = b then return a;
if Cache contains entry hORcode, {a, b} : ri then return r;
if a.lvl < b.lvl then
k ← b.lvl;
r0 ← Or(a, b[0]);
r1 ← Or(a, b[1]);
else if a.lvl > b.lvl then
k ← a.lvl;
r0 ← Or(a[0], b);
r1 ← Or(a[1], b);
else • a.lvl = b.lvl
k ← a.lvl;
r0 ← Or(a[0], b[0]);
r1 ← Or(a[1], b[1]);
r ← UniqueTableInsert(k, r0, r1);
enter hORcode, {a, b} : ri in Cache;
return r;
bdd RelProd(bdd x, bdd2 t) is • quasi-reduced version
local bdd r, r0, r1;
if x = 0 or t = 0 then return 0;
if x = 1 and t = 1 then return 1;
if Cache contains entry hRELPRODcode, x, t : ri then return r;
r0 ← Or(RelProd(x[0], t[0][0]), RelProd(x[1], t[1][0]));
r1 ← Or(RelProd(x[0], t[0][1]), RelProd(x[1], t[1][1]));
r ← UniqueTableInsert(x.lvl, r0, r1);
enter hRELPRODcode, x, t : ri in Cache;
mdd Saturation(mdd Xinit) is
return Saturate(L, Xinit);
mdd Saturate(level k, mdd p) is
local mdd r, r0, ..., rnk−1;
if p = 0 then return 0;
if p = 1 then return 1;
if Cache contains entry hSATcode, p : ri then return r;
for i = to nk − 1 do
ri ← Saturate(k − 1, p[i]);
repeat
choose e ∈ Ek, i, j ∈ Xk, such that ri 6= 0 and Te[i][j] 6= 0;
rj ← Or(rj , RelProdSat(k − 1, ri, Te[i][j]));
until r0, ..., rnk−1 do not change;
r ← UniqueTableInsert(k, r0, ..., rnk−1);
enter hSATcode, p : ri in Cache;
return r;
mdd RelProdSat(level k, mdd q, mdd2 f) is
local mdd r, r0, ..., rnk−1;
if q = 0 or f = 0 then return 0;
if Cache contains entry hRELPRODSATcode, q, f : ri then return r;
for each i, j ∈ Xk such that q[i] 6= 0 and f[i][j] 6= 0 do
rj ← Or(rj , RelProdSat(k − 1, q[i], f[i][j]));
r ← Saturate(k, UniqueTableInsert(k, r0, ..., rnk−1));
enter hRELPRODSATcode, q, f : ri in Cache;
return r.