Abstract Dependency Graphs and Their Application to Model Checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00113640" target="_blank" >RIV/00216224:14330/19:00113640 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-17462-0_18" target="_blank" >http://dx.doi.org/10.1007/978-3-030-17462-0_18</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-17462-0_18" target="_blank" >10.1007/978-3-030-17462-0_18</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Abstract Dependency Graphs and Their Application to Model Checking

Popis výsledku v původním jazyce

Dependency graphs, invented by Liu and Smolka in 1998, are oriented graphs with hyperedges that represent dependencies among the values of the vertices. Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex assignment. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general domains in order to speed up the fixed-point computation or to apply the formalism to a more general setting of e.g. weighted logics. All these extensions require separate correctness proofs of the fixed-point algorithm as well as a one-purpose implementation. We suggest the notion of abstract dependency graphs where the vertex assignment is defined over an abstract algebraic structure of Noetherian partial orders with the least element. We show that existing approaches are concrete instances of our general framework and provide an open-source C++ library that implements the abstract algorithm. We demonstrate that the performance of our generic implementation is comparable to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the literature.

Název v anglickém jazyce

Abstract Dependency Graphs and Their Application to Model Checking

Popis výsledku anglicky

Dependency graphs, invented by Liu and Smolka in 1998, are oriented graphs with hyperedges that represent dependencies among the values of the vertices. Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex assignment. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general domains in order to speed up the fixed-point computation or to apply the formalism to a more general setting of e.g. weighted logics. All these extensions require separate correctness proofs of the fixed-point algorithm as well as a one-purpose implementation. We suggest the notion of abstract dependency graphs where the vertex assignment is defined over an abstract algebraic structure of Noetherian partial orders with the least element. We show that existing approaches are concrete instances of our general framework and provide an open-source C++ library that implements the abstract algorithm. We demonstrate that the performance of our generic implementation is comparable to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the literature.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2019

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 the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)

ISBN

9783030174613

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

316-333

Název nakladatele

Springer

Místo vydání

The Netherlands

Místo konání akce

Praha

Datum konání akce

1. 1. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000681166500018