2018
A Distributed Fixed-Point Algorithm for Extended Dependency Graphs
DALSGAARD, Andreas E., Søren ENEVOLDSEN, Peter FOGH, Lasse S. JENSEN, Peter G. JENSEN et. al.Základní údaje
Originální název
A Distributed Fixed-Point Algorithm for Extended Dependency Graphs
Autoři
DALSGAARD, Andreas E. (208 Dánsko), Søren ENEVOLDSEN (208 Dánsko), Peter FOGH (208 Dánsko), Lasse S. JENSEN (208 Dánsko), Peter G. JENSEN (208 Dánsko), Tobias S. JEPSEN (208 Dánsko), Isabella KAUFMANN (208 Dánsko), Kim G. LARSEN (208 Dánsko), Søren M. NIELSEN (208 Dánsko), Mads Chr. OLESEN (208 Dánsko), Samuel PASTVA (703 Slovensko, domácí) a Jiří SRBA (203 Česká republika, garant, domácí)
Vydání
Fundamenta Informaticae, 2018, 0169-2968
Další údaje
Jazyk
angličtina
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Polsko
Utajení
není předmětem státního či obchodního tajemství
Impakt faktor
Impact factor: 1.204
Kód RIV
RIV/00216224:14330/18:00105266
Organizační jednotka
Fakulta informatiky
UT WoS
000437739500003
Klíčová slova anglicky
extended dependency graph; fixed-point algorithm; petri nets
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2019 17:28, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
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.
Návaznosti
MUNI/A/0854/2017, interní kód MU |
|