Saturation Unbound
Saturation Unbound
复制标题
饱和度无限制
DOI：
10.1007/3-540-36577-x_27
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Radu I. Siminiceanu
中科院分区：
文献类型：
--
作者：
Gianfranco Ciardo;Robert M. Marmorstein;Radu I. Siminiceanu
在以前的工作中，我们提出了一个“饱和”算法的符号状态空间生成的特点是使用多值决策图，布尔Kronecker算子，事件局部性，和一个特殊的迭代策略。这种方法优于传统的基于BDD的技术在空间和时间上的几个数量级，但像他们一样，假设每个子模型的状态空间的先验知识。我们引入了一个新的算法，合并显式的局部状态空间发现与符号的全局状态空间生成。这使建模者不必担心孤立的子模型的行为。
In previous work, we proposed a "saturation" algorithm for symbolic state-space generation characterized by the use of multivalued decision diagrams, boolean Kronecker operators, event locality, and a special iteration strategy. This approach outperforms traditional BDD-based techniques by several orders of magnitude in both space and time but, like them, assumes a priori knowledge of each submodel's state space. We introduce a new algorithm that merges explicit local state-space discovery with symbolic global state-space generation. This relieves the modeler from worrying about the behavior of submodels in isolation.