Model Verification Through Dependency Graphs

ENEVOLDSEN, Soeren, Kim G. LARSEN and 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, p. 1-19. ISBN 978-3-030-30922-0. Available from: https://dx.doi.org/10.1007/978-3-030-30923-7_1.

Basic information

Original name

Model Verification Through Dependency Graphs

Authors

ENEVOLDSEN, Soeren (208 Denmark), Kim G. LARSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00113642

Organization unit

Faculty of Informatics

ISBN

978-3-030-30922-0

ISSN

DOI

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

UT WoS

000876678900001

Keywords in English

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

Tags

firank_B

---

Abstract

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.