给定状态空间上的静态偏序降阶
给定状态空间上的静态偏序降阶
提问于 2017-05-07 02:19:54
大多数关于偏序降阶的文献都假设要分析的系统是由一组带有合成算子的过程给出的。这很有意义，因为您不想先计算状态空间，然后使用偏序缩减来减少它。
但是，假设您已经给出了一个扁平的状态空间，那么您仍然可以使用偏序缩减来减少它吗？我在想，这应该可以使用一个修改过的DFS。可以在本地检查某些属性，并且可以使用堆栈上有关状态的信息来考虑循环条件。
是否有任何论文或其他参考文献中提出了这样的算法？
回答 1
Stack Overflow用户
发布于 2017-06-05 23:09:22
是的，这是可能的。正如您所描述的，该算法与传统方法非常相似。唯一的区别是收集有关操作独立性的信息的方式不同。从概念上讲，这一切都非常简单。因此，我不认为有任何关于这样的算法的论文。
对于您的用例，互模拟最小化更有用。Baier和Katoen在他们的书“模型检查的原理”中做了很好的介绍。在用于强互模拟的"Paige和Tarjan -三个分区细化算法“和用于分支互模拟的"Groote和Wijs -用于卡顿等价和分支互模拟的O(m log n)算法”中描述了最新技术。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/43823900
复制相关文章
相似问题
腾讯云开发者
