GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data.

Anton Wijs, Muhammad Osama

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

1 Citation (Scopus)


GPUexplore 3.0 is an explicit state space exploration tool that runs entirely on a graphics processing unit (GPU), and supports models of concurrent systems with data variables. We discuss its workflow and modelling language, present several design decisions regarding work distribution and retrieval, and experimentally evaluate the impact of those decisions. Our tool achieves acceleration up to 115 × and 28 × compared to single- and four-core LTSmin, respectively. It currently checks for deadlocks, with verification of temporal logic formulae planned for the near future.

Original languageEnglish
Title of host publicationModel Checking Software - 29th International Symposium, SPIN 2023, Proceedings
EditorsGeorgiana Caltais, Christian Schilling
Number of pages10
Publication statusPublished - 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13872 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Explicit state space exploration
  • GPU
  • finite-state machines


Dive into the research topics of 'GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data.'. Together they form a unique fingerprint.

Cite this