GPUs for Model Checking and AI Planning


Talk by Stefan Edelkamp


There is no doubt that the success of state-space exploration is sensitive to the amount of computational resources available. It is not hard to predict that - due to economic pressure - parallel computing on an increased number of cores both in central processing units (CPUs) and in graphics processing units (GPUs) will be essential to solve challenging problems in the future.  The currently fastest computer (Tianhe-Ia) has more than 14000 (Intel Xeon X5670 6-core) CPUs and more than 7000 (Nvidia Tesla M2050) GPUs, while a combination of powerful multi-core CPUs and many-core GPUs is becoming standard technology also for the consumer market.


In this talk we show how model checking and AI planning can be parallelized by exploiting the processing power on the graphics card. The two exploration steps, namely selecting the actions to be applied and generating the successors, are performed on the GPU. Duplicate detection, however, is delayed to be executed on the central processing unit (CPU) or even further deferred to disk operations.  Multiple cores are employed to bypass main-memory latency, and - to increase processing speed for duplicate detection - hash tables are either approximate or lock-free.


The GPU model checker and the planner are able to deal with a considerable fraction of their respective benchmark input languages (DVE/PDDL), including numerical state variables, complex objective functions, and preferences. Experimental findings show visible performance gains especially for larger benchmark problems.