D 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

Štítky

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
Název: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů