Multi-core SCC-Based LTL Model Checking

Vincent Bloemen; Jan Cornelis van de Pol

doi:10.1007/978-3-319-49052-6_2

Multi-core SCC-Based LTL Model Checking

Vincent Bloemen, Jan Cornelis van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

13 Citations (Scopus)

114 Downloads (Pure)

Abstract

We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel. To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.

Original language	Undefined
Title of host publication	Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016
Editors	Roderick Bloem, Eli Arbel
Place of Publication	Cham
Publisher	Springer
Pages	18-33
Number of pages	16
ISBN (Print)	978-3-319-49051-9
DOIs	https://doi.org/10.1007/978-3-319-49052-6_2
Publication status	Published - Nov 2016
Event	12th International Haifa Verification Conference, HVC 2016: Hardware and Software: Verification and Testing - Haifa, Israel Duration: 14 Nov 2016 → 17 Nov 2016 Conference number: 12

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	10028
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Haifa Verification Conference, HVC 2016
Abbreviated title	HVC 2016
Country/Territory	Israel
City	Haifa
Period	14/11/16 → 17/11/16

Keywords

METIS-320900
IR-102924
Model Checking
Multi-Core
SCC
accepting cycle
LTL
strongly connected component
EWI-27453

Access to Document

10.1007/978-3-319-49052-6_2

HVC16_-_Multi-core_SCC-Based_LTL_Model_Checking

http://dx.doi.org/10.1007/978-3-319-49052-6_2

13 Citations
1 PhD Thesis - Research UT, graduation UT

Strong Connectivity and Shortest Paths for Checking Models
Bloemen, V., 10 Jul 2019, Enschede: University of Twente. 264 p.
Research output: Thesis › PhD Thesis - Research UT, graduation UT

Open Access
File
634 Downloads (Pure)

Cite this

@inproceedings{e3a5a85fff114958b3f21fbca474da2e,

title = "Multi-core SCC-Based LTL Model Checking",

abstract = "We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel. To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.",

keywords = "METIS-320900, IR-102924, Model Checking, Multi-Core, SCC, accepting cycle, LTL, strongly connected component, EWI-27453",

author = "Vincent Bloemen and \{van de Pol\}, \{Jan Cornelis\}",

note = "10.1007/978-3-319-49052-6\_2 ; 12th International Haifa Verification Conference, HVC 2016 ; Conference date: 14-11-2016 Through 17-11-2016",

year = "2016",

month = nov,

doi = "10.1007/978-3-319-49052-6\_2",

language = "Undefined",

isbn = "978-3-319-49051-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "18--33",

editor = "Roderick Bloem and Eli Arbel",

booktitle = "Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016",

address = "Germany",

}

Bloemen, V & van de Pol, JC 2016, Multi-core SCC-Based LTL Model Checking. in R Bloem & E Arbel (eds), Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016. Lecture Notes in Computer Science, vol. 10028, Springer, Cham, pp. 18-33, 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, 14/11/16. https://doi.org/10.1007/978-3-319-49052-6_2

Multi-core SCC-Based LTL Model Checking. / Bloemen, Vincent; van de Pol, Jan Cornelis.
Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016. ed. / Roderick Bloem; Eli Arbel. Cham: Springer, 2016. p. 18-33 (Lecture Notes in Computer Science; Vol. 10028).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Multi-core SCC-Based LTL Model Checking

AU - Bloemen, Vincent

AU - van de Pol, Jan Cornelis

N1 - Conference code: 12

PY - 2016/11

Y1 - 2016/11

N2 - We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel. To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.

AB - We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel. To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.

KW - METIS-320900

KW - IR-102924

KW - Model Checking

KW - Multi-Core

KW - SCC

KW - accepting cycle

KW - LTL

KW - strongly connected component

KW - EWI-27453

U2 - 10.1007/978-3-319-49052-6_2

DO - 10.1007/978-3-319-49052-6_2

M3 - Conference contribution

SN - 978-3-319-49051-9

T3 - Lecture Notes in Computer Science

SP - 18

EP - 33

BT - Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016

A2 - Bloem, Roderick

A2 - Arbel, Eli

PB - Springer

CY - Cham

T2 - 12th International Haifa Verification Conference, HVC 2016

Y2 - 14 November 2016 through 17 November 2016

ER -

Multi-core SCC-Based LTL Model Checking

Abstract

Publication series

Conference

Keywords

Access to Document

Research output

Strong Connectivity and Shortest Paths for Checking Models

Cite this