2017
Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation
DALSGAARD, Andreas E., Søren ENEVOLDSEN, Peter FOGH, Lasse S. JENSEN, Tobias S. JEPSEN et. al.Základní údaje
Originální název
Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation
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), 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í
Holandsko, Petri Nets 2017, od s. 139-158, 20 s. 2017
Nakladatel
Springer International Publishing
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10200 1.2 Computer and information sciences
Stát vydavatele
Nizozemské království
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Odkazy
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/17:00094905
Organizační jednotka
Fakulta informatiky
ISBN
978-3-319-57860-6
ISSN
UT WoS
000430740600010
Klíčová slova anglicky
CTL model checking; Petri Nets; distributed algorithms; on-the-fly state-space search; parallelism
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 18. 5. 2018 12:14, 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 verification 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 an open-source tool, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the Model Checking Contest 2016.
Návaznosti
GA15-11089S, projekt VaV |
|