Name
Abstract | ||
|---|---|---|
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 magnitude. Compared to state-of-the-art in multi-core model checking software, still advances remain visible. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-16164-3_8 | SPIN |
Keywords | Field | DocType |
parallel stage,model checking,multi-core model checking software,boolean vector,parallel matrix operation,state space exploration,input model,general purpose graphics processor,efficient explicit-state model checking,state space graph,explicit-state model checking,proposed gpu exploration algorithm,state space,bloom filter | Graphics,Bloom filter,Abstraction model checking,Model checking,Reverse Polish notation,Computer science,Parallel computing,Hash function,Graphics processing unit,State space | Conference |
Volume | ISSN | ISBN |
6349 | 0302-9743 | 3-642-16163-4 |
Citations | PageRank | References |
13 | 0.61 | 25 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stefan Edelkamp | 1 | 1557 | 125.46 |
| Damian Sulewski | 2 | 87 | 6.45 |