Abstract Dependency Graphs and Their Application to Model Checking

ENEVOLDSEN, Soeren, Kim G. LARSEN and Jiří SRBA. Abstract Dependency Graphs and Their Application to Model Checking. Online. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). The Netherlands: Springer, 2019. p. 316-333. ISBN 978-3-030-17461-3. Available from: https://dx.doi.org/10.1007/978-3-030-17462-0_18. [citováno 2024-04-24]

Basic information

• Original name: Abstract Dependency Graphs and Their Application to Model Checking
• Authors: ENEVOLDSEN, Soeren (208 Denmark), Kim G. LARSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution)
• Edition: The Netherlands, Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), p. 316-333, 18 pp. 2019.
• Publisher: Springer

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: printed version "print"
• Impact factor: Impact factor: 0.402 in 2005
• RIV identification code: RIV/00216224:14330/19:00113640
• Organization unit: Faculty of Informatics
• ISBN: 978-3-030-17461-3
• ISSN: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-030-17462-0_18
• UT WoS: 000681166500018
• Keywords in English: dependency graph; on-the-fly algorithms; verification; model checking
• Tags: core_A, firank_A

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.