时间戳

首页 > 解决方案 > CUDD：ZDD 的量化

model-checking - CUDD：ZDD 的量化

问题描述

我正在使用 CUDD ( https://github.com/ivmai/cudd ) 使用 bdd 和 zdd 功能进行模型检查，我想知道如何量化 zdds。

对于 bdd，有 bddExistAbstract 和 bddUnivAbstract 函数（参见http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddAllDet.html#Cudd_bddUnivAbstract）。

该手册说，这些函数普遍地和存在地从 bdd 中抽象出给定的变量（以封面形式）。我不太清楚“抽象出来”是什么意思，因此我坚持弄清楚量化如何改变 zdds。

你们能帮忙吗？谢谢。

标签： model-checkingquantifiersbinary-decision-diagramcudd

解决方案

Python 包dd实现了到 CUDD 的 Cython 接口，该接口通过量化扩展了 CUDD 的 ZDD 功能。例如，要在 ZDD 上使用存在量化：

from dd import cudd_zdd

zdd = cudd_zdd.ZDD()  # create a ZDD manager
zdd.declare('x', 'y')  # add variables to the manager
u = zdd.add_expr(r'x /\ y')  # create a BDD `u` for the expression x /\ y
v = zdd.exist(['y'], u)  # quantify over variable y, i.e., compute \E y:  x /\ y
>>> zdd.to_expr(v)  # convert to an expression as string
'x'

ZDD 量化的实现可以在以下位置找到：

https://github.com/tulip-control/dd/blob/24ec9eba335c173e1fe0367a9ac25ec201dee1b5/dd/cudd_zdd.pyx#L1999-L2172

并且出于开发目的还存在许多 Python 级别的实现：

https://github.com/tulip-control/dd/blob/24ec9eba335c173e1fe0367a9ac25ec201dee1b5/dd/cudd_zdd.pyx#L1387-L1544

该软件包dd可以从PyPI安装，带有pip install dd. 这将在 Linux 上安装 CUDD 绑定。在 macOS 上，与 CUDD 的绑定需要从 的源代码编译dd，因此 macOS 的安装变为：

pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd --cudd_zdd

如文件README.md中所述。

推荐阅读