A Distributed Fixed-Point Algorithm for Extended Dependency Graphs
A Distributed Fixed-Point Algorithm for Extended Dependency Graphs
复制标题
扩展依赖图的分布式定点算法
DOI：
10.3233/fi-2018-1707
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Jiri Srba
中科院分区：
文献类型：
--
作者：
Andreas Engelbredt Dalsgaard;Søren Enevoldsen;P. Fogh;Lasse S. Jensen;P. G. Jensen;T. S. Jepsen;Isabella Kaufmann;K. Larsen;Søren M. Nielsen;Mads Chr. Olesen;Samuel Pastva;Jiri Srba
等价性和模型检查问题可以被编码为计算依赖图上的不动点。依赖图通过超边表示图的节点之间的因果依赖关系。我们建议扩展模型的依赖图与所谓的否定边缘，以增加其适用性。图（以及验证问题）遭受状态空间爆炸问题。为了解决这个问题，我们设计了一个动态算法，有效地计算扩展依赖图上的不动点。我们的算法补充了以前的方法，在某些情况下，除了值1的标准反向传播之外，还可以反向传播域值0。最后，我们设计了一个分布式版本的算法，实现它在我们的开源工具TAPAAL，并证明了我们的一般方法的效率上的基准的Petri网模型和CTL查询从年度模型检查竞赛。
Equivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verifi- cation problems) suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate, in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design a distributed version of the algorithm, implement it in our open-source tool TAPAAL, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest.