A GPU-based MPG solver

Overview

The GPUMPG package contains a GPU-based implementations of several algorithms for solving mean-payoff games.

To use the tool, you need the corresponding OpenCL drivers for your device:

• Intel SDK for OpenCL Applications
• AMD APP SDK
• Nvidia CUDA Toolkit

The tool can be invoked by executing mpgsolver FILE, with FILE being a mean-payoff game. Several options can be specified, list them by executing mpgsolver --help. The benchmark results can be re-evaluated by running the Bash script bench/run_benchmarks.sh, with the options in bench/config adjusted to your system.

Source code, benchmarks and results

• Source code (71 KB, md5sum: 9e20b8c467e842880cf7c5052352256f).
• Precompiled Win64 executable (801 KB, md5sum: a83a7a4c80ba255e6bc8ef62619ff7d7).
• Games from the synthesis of controllers for hybrid systems (563 MB, md5sum: 22867970323da441f42e5d7765dace84).
• Games converted from parity games for equivalence checking problems (6.2 GB, md5sum: ac81d06d4cc684e414d57e1aa33041f7) (from here).
• Games converted from parity games for model checking problems (2.2 GB, md5sum: a509bf2e01bc6c6b12ec0fe83fe42f8e) (from here).
• Compiled results for the above benchmarks (6.2 KB, md5sum: 695ac092c8fe86c237e949ad53aa5327).
• Solutions from our solver for the above benchmarks (739 MB, md5sum: 1cde21047683970d95fe4fb06babfcac).

Compiling instructions

You need, in addition to one of the OpenCL toolkits given above:

• A C++ compiler. Compilation was tested with g++ 6.1 and the Visual Studio 2015 compiler (msvc-14.0)
• CMake
• Boost in the version 1.61 or higher. Extract boost to some location and set the environment variable BOOST_ROOT to that location. You also need to build the static boost libraries with the following commands in the boost folder (adjust toolset if you use another compiler):
  • .\boostrap
  • .\b2 -j8 variant=release toolset=msvc-14.0 address-model=64 link=static threading=multi

Then the build script build_windows.bat builds the project on Windows using Visual Studio 2015 in a 64-bit build. Other builds can be specified by editing the file or invoking CMake by hand.

Contact

• Philipp Meyer (Email: meyerphi@in.tum.de)
• Michael Luttenberger (Email: luttenbe@model.in.tum.de)