Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F17%3A00094905" target="_blank" >RIV/00216224:14330/17:00094905 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-57861-3_10" target="_blank" >http://dx.doi.org/10.1007/978-3-319-57861-3_10</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-57861-3_10" target="_blank" >10.1007/978-3-319-57861-3_10</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GA15-11089S" target="_blank" >GA15-11089S: Získávání parametrů biologických modelů pomocí techniky ověřování modelů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Petri Nets 2017

ISBN

9783319578606

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

20

Strana od-do

139-158

Název nakladatele

Springer International Publishing

Místo vydání

Holandsko

Místo konání akce

Zaragoza, Spain

Datum konání akce

25. 6. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000430740600010