A Distributed Fixed-Point Algorithm for Extended Dependency Graphs
| Authors | |
|---|---|
| Year of publication | 2018 |
| Type | Article in Periodical |
| Magazine / Source | Fundamenta Informaticae |
| MU Faculty or unit | |
| Citation | |
| Web | |
| Doi | http://dx.doi.org/10.3233/FI-2018-1707 |
| Keywords | extended dependency graph; fixed-point algorithm; petri nets |
| Description | 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. |
| Related projects: |