Model Verification Through Dependency Graphs

ENEVOLDSEN, Soeren; Kim G. LARSEN a Jiří SRBA. Model Verification Through Dependency Graphs. In Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19). The Nederlands: Springer, 2019, s. 1-19. ISBN 978-3-030-30922-0. Dostupné z: https://doi.org/10.1007/978-3-030-30923-7_1.

Základní údaje

Originální název

Model Verification Through Dependency Graphs

Autoři

ENEVOLDSEN, Soeren; Kim G. LARSEN a Jiří SRBA

Vydání

The Nederlands, Proceedings of the 26th International SPIN Symposium on Model Checking of Software (SPIN'19), od s. 1-19, 19 s. 2019

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/19:00113642

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-30922-0

ISSN

DOI

https://doi.org/10.1007/978-3-030-30923-7_1

UT WoS

000876678900001

EID Scopus

2-s2.0-85075546005

Klíčová slova anglicky

dependency graph; on-the-fly algorithms; model checking; verification

---

Anotace

V originále

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.