Hierarchical Decision Diagrams to Exploit Model Structure
Hierarchical Decision Diagrams to Exploit Model Structure
复制标题
利用模型结构的分层决策图
DOI：
10.1007/11562436_32
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Y. Thierry
中科院分区：
文献类型：
--
作者：
J. Couvreur;Y. Thierry
使用二进制决策图（BDD）进行符号模型检查可以表示非常大的状态空间。BDD为同步系统提供了良好的结果，特别是对于很好地适应状态二进制编码的电路。然而，在尝试处理全局异步和类型化规范时，操作定义机制（使用更多的BDD）和状态表示（从根到叶的纯线性遍历）都显示出它们的局限性。数据决策图（DDD）[7]是一种操纵（先验无界的）整数域变量的有向无环图结构，它通过归纳同态提供了灵活和组合的操作定义。
Symbolic model-checking using binary decision diagrams (BDD) can allow to represent very large state spaces. BDD give good results for synchronous systems, particularly for circuits that are well adapted to a binary encoding of a state. However both the operation definition mechanism (using more BDD) and the state representation (purely linear traversal from root to leaves) show their limits when trying to tackle globally asynchronous and typed specifications. Data Decision Diagrams (DDD) [7] are a directed acyclic graph structure that manipulates(a priori unbounded) integer domain variables, and which offers a flexible and compositional definition of operations through inductive homomorphisms.
We first introduce a new transitive closure unary operator for homomorphisms, that heavily reduces the intermediate peak size effect common to symbolic approaches. We then extend the DDD definition to introduce hierarchy in the data structure. We define Set Decision Diagrams, in which a variable’s domain is a set of values. Concretely, it means the arcs of an SDD may be labeled with an SDD (or a DDD), introducing the possibility of arbitrary depth nesting in the data structure. We show how this data structure and operation framework is particularly adapted to the computation and representation of structured state-spaces, and thus shows good potential for symbolic model-checking of software systems, a problem that is difficult for plain BDD representations.