Abstract Dependency Graphs and Their Application to Model
Checking

D 2019

Abstract Dependency Graphs and Their Application to Model Checking

ENEVOLDSEN, Soeren, Kim G. LARSEN a Jiří SRBA

Základní údaje

Originální název

Abstract Dependency Graphs and Their Application to Model Checking

Autoři

ENEVOLDSEN, Soeren (208 Dánsko), Kim G. LARSEN (208 Dánsko) a Jiří SRBA (203 Česká republika, garant, domácí)

Vydání

The Netherlands, Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), od s. 316-333, 18 s. 2019

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

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"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00113640

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-17461-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-17462-0_18

UT WoS

000681166500018

Klíčová slova anglicky

dependency graph; on-the-fly algorithms; verification; model checking

Štítky

core_A, firank_A

Změněno: 16. 5. 2022 14:27, Mgr. Michal Petr

Anotace

V originále

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.

Citovat

ENEVOLDSEN, Soeren, Kim G. LARSEN a Jiří SRBA. Abstract Dependency Graphs and Their Application to Model Checking. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). The Netherlands: Springer, 2019, s. 316-333. ISBN 978-3-030-17461-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-17462-0_18.

@inproceedings{1646339,
   author = {Enevoldsen, Soeren and Larsen, Kim G. and Srba, Jiří},
   address = {The Netherlands},
   booktitle = {Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)},
   doi = {http://dx.doi.org/10.1007/978-3-030-17462-0_18},
   keywords = {dependency graph; on-the-fly algorithms; verification; model checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {The Netherlands},
   isbn = {978-3-030-17461-3},
   pages = {316-333},
   publisher = {Springer},
   title = {Abstract Dependency Graphs and Their Application to Model Checking},
   year = {2019}
}

TY  - JOUR
ID  - 1646339
AU  - Enevoldsen, Soeren - Larsen, Kim G. - Srba, Jiří
PY  - 2019
TI  - Abstract Dependency Graphs and Their Application to Model Checking
PB  - Springer
CY  - The Netherlands
SN  - 9783030174613
KW  - dependency graph
KW  - on-the-fly algorithms
KW  - verification
KW  - model checking
N2  - 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.
ER  -

ENEVOLDSEN, Soeren, Kim G. LARSEN a Jiří SRBA. Abstract Dependency Graphs and Their Application to Model Checking. In \textit{Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)}. The Netherlands: Springer, 2019, s.~316-333. ISBN~978-3-030-17461-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-17462-0\_{}18.

Podrobný výpis o publikaci