PGSolver is a collection of tools for generating, manipulating and - most of all - solving parity games. It features implementations of (almost) all known algorithms for parity games as well as heuristics for pre-processing and speeding up the solving process.

PGSolver is being developed and maintained at the chair for theoretical computer science of the University of Munich, Germany.

The latest version is 3.1, released on February 27th, 2012. No warranty can be given. Source code can be downloaded below. It is distributed under the BSD license.
The program is written in OCaml. You will therefore need an OCaml compiler to produce the executables. We recommend version ≥ 3.09, but smaller versions may also suffice. If you want to have support for the reductions to SAT you will also need a SAT solver. Please consult the documentation for a description of which SAT solvers are currently supported or how to embed a new one.

• Version 3.1, released February, 27th, 2012
  • new solver: genetic solver
  • new solver: smt-based solving
  • new generators: generator for all policy iteration lower bound constructions
• Version 3, released January, 21st, 2010
  • new solver: strategy iteration by reduction to discounted payoff games
  • new solver: randomized algorithm by Vorobyov et al.
  • new solver: another randomized algorithm by Vorobyov et al.
  • new solver: local strategy improvement by ourselves
  • solver improved: local mu-calculus model checker
  • solver improved: small progress measures algorithm
  • new feature: PGSolver as a linkable library
  • new feature: local solving
  • new feature: generators can be linked in
  • new feature: printing and parsing of solutions and strategies
  • new tool: conversion between min-parity and max-parity games
  • new generator: towers of Hanoi (reachability game)
  • new generator: fairness verification of an elevator system
• Version 2, released January, 30th, 2009
• Version 1, released ... uh, well, a long time ago. And who cares about this anyway?

Click on the download button below to obtain a tar.gz archive with PGSolver's source code. It also contains guidelines on how to compile and run it.

If you want to be notified whenever a newer version is available please provide your details. Otherwise leave the following fields blank. Do not enter fake email addresses or keywords like "test". That just messes up our statistics file. You really do not need to enter anything. We will give you the implementation even if you don't give us your details. Believe me. If you enter nonsense into the fields think twice before you press the download button. If you are extremely lucky we have a nice day and let you get away with it. Equally, we may not.

Name:
Email:
Affiliation:

For installation instructions see the included documentation. It is also available here in PDF format: Documentation.

Please direct and questions, enquiries, suggestions, etc. to Oliver Friedmann or Martin Lange.