A Distributed Fixed-Point Algorithm for Extended Dependency Graphs
| Autoři | |
|---|---|
| Rok publikování | 2018 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Fundamenta Informaticae |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | |
| Doi | http://dx.doi.org/10.3233/FI-2018-1707 |
| Klíčová slova | extended dependency graph; fixed-point algorithm; petri nets |
| Popis | 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. |
| Související projekty: |