Extended abstract dependency graphs

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

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2022-02, Vol.24 (1), p.49-65
Main Authors: Enevoldsen, Søren, Larsen, Kim Guldstrand, Srba, Jiří
Format: Article
Language:English
Subjects:
Algorithms
Apexes
Boolean
Boolean algebra
Computation
Computer Science
Domains
Fixed points (mathematics)
Graphs
Software Engineering
Software Engineering/Programming and Operating Systems
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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, for example, 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 extended abstract dependency graphs where the vertex assignment is defined over an abstract algebraic structure of Noetherian partial orders with the least element, and where we allow both monotonic and non-monotonic functions. 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.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-021-00638-8