Model Verification Through Dependency Graphs

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearch

Abstract

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. We present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic and timed systems.
Original languageEnglish
Title of host publicationProceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19)
EditorsFabrizio Biondi, Thomas Given-Wilson, Axel Legay
Number of pages19
PublisherSpringer
Publication date2019
Pages1-19
ISBN (Print)978-3-030-30922-0
ISBN (Electronic)978-3-030-30923-7
DOIs
Publication statusPublished - 2019
EventInternational Symposium on Model Checking Software - Beijing, China
Duration: 15 Jul 201919 Jul 2019

Conference

ConferenceInternational Symposium on Model Checking Software
CountryChina
CityBeijing
Period15/07/201919/07/2019
SeriesLecture Notes in Computer Science
Volume11636
ISSN0302-9743

Keywords

  • Dependency graphs
  • Fixed-point computation
  • On-the-fly algorithms
  • Verification

Cite this

Enevoldsen, S., Larsen, K. G., & Srba, J. (2019). Model Verification Through Dependency Graphs. In F. Biondi, T. Given-Wilson, & A. Legay (Eds.), Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19) (pp. 1-19). Springer. Lecture Notes in Computer Science, Vol.. 11636 https://doi.org/10.1007/978-3-030-30923-7_1
Enevoldsen, Søren ; Larsen, Kim Guldstrand ; Srba, Jiri. / Model Verification Through Dependency Graphs. Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19). editor / Fabrizio Biondi ; Thomas Given-Wilson ; Axel Legay. Springer, 2019. pp. 1-19 (Lecture Notes in Computer Science, Vol. 11636).
@inproceedings{c6becba94b7b4f7aacec54d86f051017,
title = "Model Verification Through Dependency Graphs",
abstract = "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. We present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic and timed systems.",
keywords = "Dependency graphs, Fixed-point computation, On-the-fly algorithms, Verification",
author = "S{\o}ren Enevoldsen and Larsen, {Kim Guldstrand} and Jiri Srba",
year = "2019",
doi = "10.1007/978-3-030-30923-7_1",
language = "English",
isbn = "978-3-030-30922-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--19",
editor = "Fabrizio Biondi and Thomas Given-Wilson and Axel Legay",
booktitle = "Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19)",
address = "Germany",

}

Enevoldsen, S, Larsen, KG & Srba, J 2019, Model Verification Through Dependency Graphs. in F Biondi, T Given-Wilson & A Legay (eds), Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19). Springer, Lecture Notes in Computer Science, vol. 11636, pp. 1-19, International Symposium on Model Checking Software, Beijing, China, 15/07/2019. https://doi.org/10.1007/978-3-030-30923-7_1

Model Verification Through Dependency Graphs. / Enevoldsen, Søren; Larsen, Kim Guldstrand; Srba, Jiri.

Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19). ed. / Fabrizio Biondi; Thomas Given-Wilson; Axel Legay. Springer, 2019. p. 1-19 (Lecture Notes in Computer Science, Vol. 11636).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearch

TY - GEN

T1 - Model Verification Through Dependency Graphs

AU - Enevoldsen, Søren

AU - Larsen, Kim Guldstrand

AU - Srba, Jiri

PY - 2019

Y1 - 2019

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. We present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic 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. We present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic 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=85075546005&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-30923-7_1

DO - 10.1007/978-3-030-30923-7_1

M3 - Article in proceeding

SN - 978-3-030-30922-0

T3 - Lecture Notes in Computer Science

SP - 1

EP - 19

BT - Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19)

A2 - Biondi, Fabrizio

A2 - Given-Wilson, Thomas

A2 - Legay, Axel

PB - Springer

ER -

Enevoldsen S, Larsen KG, Srba J. Model Verification Through Dependency Graphs. In Biondi F, Given-Wilson T, Legay A, editors, Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19). Springer. 2019. p. 1-19. (Lecture Notes in Computer Science, Vol. 11636). https://doi.org/10.1007/978-3-030-30923-7_1