Distributed Computation of Fixed Points on Dependency Graphs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00094045" target="_blank" >RIV/00216224:14330/16:00094045 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007/978-3-319-47677-3_13" target="_blank" >http://link.springer.com/chapter/10.1007/978-3-319-47677-3_13</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Distributed Computation of Fixed Points on Dependency Graphs

Popis výsledku v původním jazyce

Dependency graph is an abstract mathematical structure for representing complex causal dependencies among its vertices. Several equivalence and model checking questions, boolean equation systems and other problems can be reduced to fixed-point computations on dependency graphs. We develop a novel distributed algorithm for computing such fixed points, prove its correctness and provide an efficient, open-source implementation of the algorithm. The algorithm works in an on-the-fly manner, eliminating the need to generate a priori the entire dependency graph. We evaluate the applicability of our approach by a number of experiments that verify weak simulation/bisimulation equivalences between CCS processes and we compare the performance with the well-known CWB tool. Even though the fixed-point computation, being a P-complete problem, is difficult to parallelize in theory, we achieve significant speed-ups in the performance as demonstrated on a Linux cluster with several hundreds of cores.

Název v anglickém jazyce

Distributed Computation of Fixed Points on Dependency Graphs

Popis výsledku anglicky

Dependency graph is an abstract mathematical structure for representing complex causal dependencies among its vertices. Several equivalence and model checking questions, boolean equation systems and other problems can be reduced to fixed-point computations on dependency graphs. We develop a novel distributed algorithm for computing such fixed points, prove its correctness and provide an efficient, open-source implementation of the algorithm. The algorithm works in an on-the-fly manner, eliminating the need to generate a priori the entire dependency graph. We evaluate the applicability of our approach by a number of experiments that verify weak simulation/bisimulation equivalences between CCS processes and we compare the performance with the well-known CWB tool. Even though the fixed-point computation, being a P-complete problem, is difficult to parallelize in theory, we achieve significant speed-ups in the performance as demonstrated on a Linux cluster with several hundreds of cores.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2016

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

Proceedings of Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'16)

ISBN

9783319476766

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

16

Strana od-do

197-212

Název nakladatele

Springer

Místo vydání

Netherlands

Místo konání akce

China

Datum konání akce

1. 1. 2016

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

WRD - Celosvětová akce

Kód UT WoS článku

000389932000013