GPU accelerated strong and branching bisimilarity checking

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

24 Citations (Scopus)

Abstract

Bisimilarity checking is an important operation to perform explicit-state model checking when the state space of a model under verification has already been generated. It can be applied in various ways: reduction of a state space w.r.t. a particular flavour of bisimilarity, or checking that two given state spaces are bisimilar. Bisimilarity checking is a computationally intensive task, and over the years, several algorithms have been presented, both sequential, i.e. single-threaded, and parallel, the latter either relying on shared memory or message-passing. In this work, we first present a novel way to check strong bisimilarity on general-purpose graphics processing units (GPUs), and show experimentally that an implementation of it for CUDA-enabled GPUs is competitive with other parallel techniques that run either on a GPU or use message-passing on a multi-core system. Building on this, we propose, to the best of our knowledge, the first many-core branching bisimilarity checking algorithm, an implementation of which shows speedups comparable to our strong bisimilarity checking approach.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
EditorsC. Baier, C. Tinelli
Place of PublicationBerlin
PublisherSpringer
Pages368-383
ISBN (Electronic)978-3-662-46681-0
ISBN (Print)978-3-662-46680-3
DOIs
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
Volume9035
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'GPU accelerated strong and branching bisimilarity checking'. Together they form a unique fingerprint.

Cite this