BFS-based model checking of linear-time properties with an application on GPUs

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

13 Citations (Scopus)

Abstract

Efficient algorithms have been developed to model check liveness properties, such as the well-known Nested Depth-First Search, which uses a depth-first search (DFS) strategy. However, in some settings, DFS is not a suitable option. For instance, when considering distributed model checking on a cluster, or many-core model checking using a Graphics Processing Unit (GPU), Breadth-First Search (BFS) is a more natural choice, at least for basic reachability analysis. Liveness property checking, however, requires the detection of (accepting) cycles, and BFS is not very suitable to detect these on-the-fly. In this paper, we consider how a model checker that completely runs on a GPU can be extended to efficiently verify whether finite-state concurrent systems satisfy liveness properties. We exploit the fact that the state space is the product of the behaviour of several parallel automata. The result of this work is the very first GPU-based model checker that can check liveness properties.

Original languageEnglish
Title of host publicationComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
PublisherSpringer
Pages472-493
Number of pages22
Volume9780
ISBN (Print)9783319415390
DOIs
Publication statusPublished - 2016
Event28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada
Duration: 17 Jul 201623 Jul 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9780
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference28th International Conference on Computer Aided Verification, CAV 2016
CountryCanada
CityToronto
Period17/07/1623/07/16

Fingerprint

Dive into the research topics of 'BFS-based model checking of linear-time properties with an application on GPUs'. Together they form a unique fingerprint.

Cite this