TY - JOUR
T1 - Dependency graphs with applications to verification
AU - Enevoldsen, Søren
AU - Larsen, Kim G.
AU - Mariegaard, Anders
AU - Srba, Jiří
N1 - Funding Information:
We would like to thank to Hubert Garavel and Radu Mateescu for sharing the French history of on-the-fly model checking with us. The work of the second author has taken place in the context of the ERC Advanced Grant LASSO.
Publisher Copyright:
© 2020, Springer-Verlag GmbH Germany, part of Springer Nature.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2020/10/1
Y1 - 2020/10/1
N2 - Dependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original definition, assignments link each node with a Boolean value; however, in the recent work the assignment domains have been extended to more general setting, even including infinite domains. In this survey paper, we present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic, parameterized and timed systems.
AB - Dependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original definition, assignments link each node with a Boolean value; however, in the recent work the assignment domains have been extended to more general setting, even including infinite domains. In this survey paper, we present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic, parameterized and timed systems.
KW - Dependency graphs
KW - Fixed-point computation
KW - On-the-fly algorithms
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85086121913&partnerID=8YFLogxK
U2 - 10.1007/s10009-020-00578-9
DO - 10.1007/s10009-020-00578-9
M3 - Journal article
AN - SCOPUS:85086121913
VL - 22
SP - 635
EP - 654
JO - International Journal on Software Tools for Technology Transfer
JF - International Journal on Software Tools for Technology Transfer
SN - 1433-2779
IS - 5
ER -