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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

13 Citaten (Scopus)

Samenvatting

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.

Originele taal-2Engels
TitelComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
UitgeverijSpringer
Pagina's472-493
Aantal pagina's22
Volume9780
ISBN van geprinte versie9783319415390
DOI's
StatusGepubliceerd - 2016
Evenement28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada
Duur: 17 jul 201623 jul 2016

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9780
ISSN van geprinte versie03029743
ISSN van elektronische versie16113349

Congres

Congres28th International Conference on Computer Aided Verification, CAV 2016
Land/RegioCanada
StadToronto
Periode17/07/1623/07/16

Vingerafdruk

Duik in de onderzoeksthema's van 'BFS-based model checking of linear-time properties with an application on GPUs'. Samen vormen ze een unieke vingerafdruk.

Citeer dit