Abstract Dependency Graphs and Their Application to Model Checking

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2 Citations (Scopus)
1 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)
EditorsLijun Zhang, Tomáš Vojnar
Number of pages18
PublisherSpringer
Publication date2019
Pages316-333
ISBN (Print)978-3-030-17461-3
ISBN (Electronic)978-3-030-17462-0
DOIs
Publication statusPublished - 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
CountryCzech Republic
CityPrague
Period06/04/201911/04/2019
SeriesLecture Notes in Computer Science
Volume11427
ISSN0302-9743

Fingerprint

Model checking
Concretes

Keywords

  • dependency graphs, model checking, logic

Cite this

Enevoldsen, S., Larsen, K. G., & Srba, J. (2019). Abstract Dependency Graphs and Their Application to Model Checking. In L. Zhang, & T. Vojnar (Eds.), Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19) (pp. 316-333). Springer. Lecture Notes in Computer Science, Vol.. 11427 https://doi.org/10.1007/978-3-030-17462-0_18
Enevoldsen, Søren ; Larsen, Kim Guldstrand ; Srba, Jiri. / Abstract Dependency Graphs and Their Application to Model Checking. Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). editor / Lijun Zhang ; Tomáš Vojnar. Springer, 2019. pp. 316-333 (Lecture Notes in Computer Science, Vol. 11427).
@inproceedings{8aceb746c233466382c0cb469847df88,
title = "Abstract Dependency Graphs and Their Application to Model Checking",
abstract = "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.",
keywords = "dependency graphs, model checking, logic",
author = "S{\o}ren Enevoldsen and Larsen, {Kim Guldstrand} and Jiri Srba",
year = "2019",
doi = "10.1007/978-3-030-17462-0_18",
language = "English",
isbn = "978-3-030-17461-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "316--333",
editor = "Lijun Zhang and Tom{\'a}š Vojnar",
booktitle = "Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)",
address = "Germany",
note = "25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",

}

Enevoldsen, S, Larsen, KG & Srba, J 2019, Abstract Dependency Graphs and Their Application to Model Checking. in L Zhang & T Vojnar (eds), Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). Springer, Lecture Notes in Computer Science, vol. 11427, pp. 316-333, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 06/04/2019. https://doi.org/10.1007/978-3-030-17462-0_18

Abstract Dependency Graphs and Their Application to Model Checking. / Enevoldsen, Søren; Larsen, Kim Guldstrand; Srba, Jiri.

Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). ed. / Lijun Zhang; Tomáš Vojnar. Springer, 2019. p. 316-333 (Lecture Notes in Computer Science, Vol. 11427).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

TY - GEN

T1 - Abstract Dependency Graphs and Their Application to Model Checking

AU - Enevoldsen, Søren

AU - Larsen, Kim Guldstrand

AU - Srba, Jiri

PY - 2019

Y1 - 2019

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.

AB - 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.

KW - dependency graphs, model checking, logic

UR - https://link.springer.com/chapter/10.1007%2F978-3-030-17462-0_18

U2 - 10.1007/978-3-030-17462-0_18

DO - 10.1007/978-3-030-17462-0_18

M3 - Article in proceeding

SN - 978-3-030-17461-3

T3 - Lecture Notes in Computer Science

SP - 316

EP - 333

BT - Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)

A2 - Zhang, Lijun

A2 - Vojnar, Tomáš

PB - Springer

T2 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Y2 - 6 April 2019 through 11 April 2019

ER -

Enevoldsen S, Larsen KG, Srba J. Abstract Dependency Graphs and Their Application to Model Checking. In Zhang L, Vojnar T, editors, Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). Springer. 2019. p. 316-333. (Lecture Notes in Computer Science, Vol. 11427). https://doi.org/10.1007/978-3-030-17462-0_18