Abstract Dependency Graphs and Their Application to Model Checking

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

4 Citationer (Scopus)
18 Downloads (Pure)

Abstrakt

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.
OriginalsprogEngelsk
TitelProceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)
RedaktørerLijun Zhang, Tomáš Vojnar
Antal sider18
ForlagSpringer
Publikationsdato2019
Sider316-333
ISBN (Trykt)978-3-030-17461-3
ISBN (Elektronisk)978-3-030-17462-0
DOI
StatusUdgivet - 2019
Begivenhed25th 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, Tjekkiet
Varighed: 6 apr. 201911 apr. 2019

Konference

Konference25th 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
LandTjekkiet
ByPrague
Periode06/04/201911/04/2019
NavnLecture Notes in Computer Science
Vol/bind11427
ISSN0302-9743

Fingeraftryk Dyk ned i forskningsemnerne om 'Abstract Dependency Graphs and Their Application to Model Checking'. Sammen danner de et unikt fingeraftryk.

Citationsformater