Sciweavers

Share
SPIN
2010
Springer

Efficient Explicit-State Model Checking on General Purpose Graphics Processors

8 years 8 months ago
Efficient Explicit-State Model Checking on General Purpose Graphics Processors
We accelerate state space exploration for explicit-state model checking by executing complex operations on the graphics processing unit (GPU). In contrast to existing approaches enhancing model checking through performing parallel matrix operations on the GPU, we parallelize the breadth-first layered construction of the state space graph. For efficient processing, the input model is translated to the reverse Polish notation, resulting in a representation as an integer vector. The proposed GPU exploration algorithm then divides into two parallel stages. In the first stage, each state is replaced with a Boolean vector to denote which transitions are enabled. In the second stage, pairs consisting of replicated states and enabled transition IDs are copied to the GPU then all transitions are applied in parallel to produce the successors. Bitstate hashing is used as a Bloom filter to remove duplicates from the set of successors in RAM. The experiments show speed-ups of about one order of mag...
Stefan Edelkamp, Damian Sulewski
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where SPIN
Authors Stefan Edelkamp, Damian Sulewski
Comments (0)
books